let W be Universe; :: thesis: for b being Ordinal of W
for phi being Ordinal-Sequence of W st omega in W & phi is increasing & phi is continuous holds
ex a being Ordinal of W st
( b in a & phi . a = a & a is_cofinal_with omega )

let b be Ordinal of W; :: thesis: for phi being Ordinal-Sequence of W st omega in W & phi is increasing & phi is continuous holds
ex a being Ordinal of W st
( b in a & phi . a = a & a is_cofinal_with omega )

let phi be Ordinal-Sequence of W; :: thesis: ( omega in W & phi is increasing & phi is continuous implies ex a being Ordinal of W st
( b in a & phi . a = a & a is_cofinal_with omega ) )

assume that
A1: omega in W and
A2: phi is increasing and
A3: phi is continuous ; :: thesis: ex a being Ordinal of W st
( b in a & phi . a = a & a is_cofinal_with omega )

A4: omega in On W by ;
deffunc H1( Ordinal, set ) -> Element of W = 0-element_of W;
deffunc H2( Ordinal, Ordinal of W) -> Element of W = succ (phi . \$2);
consider nu being Ordinal-Sequence of W such that
A5: nu . () = b and
A6: for a being Ordinal of W holds nu . (succ a) = H2(a,nu . a) and
for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal holds
nu . a = H1(a,nu | a) from set xi = nu | omega;
set a = sup (nu | omega);
A7: On W c= W by ORDINAL2:7;
dom nu = On W by FUNCT_2:def 1;
then A8: omega c= dom nu by A4;
then A9: dom (nu | omega) = omega by RELAT_1:62;
( rng (nu | omega) c= rng nu & rng nu c= On W ) by RELAT_1:def 19;
then rng (nu | omega) c= On W ;
then rng (nu | omega) c= W by A7;
then reconsider a = sup (nu | omega) as Ordinal of W by ;
A10: a in dom phi by ORDINAL4:34;
then A11: a c= dom phi by ORDINAL1:def 2;
then A12: dom (phi | a) = a by RELAT_1:62;
A13: nu | omega is increasing
proof
let A be Ordinal; :: according to ORDINAL2:def 12 :: thesis: for b1 being set holds
( not A in b1 or not b1 in dom (nu | omega) or (nu | omega) . A in (nu | omega) . b1 )

let B be Ordinal; :: thesis: ( not A in B or not B in dom (nu | omega) or (nu | omega) . A in (nu | omega) . B )
assume that
A14: A in B and
A15: B in dom (nu | omega) ; :: thesis: (nu | omega) . A in (nu | omega) . B
defpred S2[ Ordinal] means ( A +^ \$1 in dom (nu | omega) & \$1 <> {} implies (nu | omega) . A in (nu | omega) . (A +^ \$1) );
A16: for B being Ordinal st B <> 0 & B is limit_ordinal & ( for C being Ordinal st C in B holds
S2[C] ) holds
S2[B]
proof
let B be Ordinal; :: thesis: ( B <> 0 & B is limit_ordinal & ( for C being Ordinal st C in B holds
S2[C] ) implies S2[B] )

assume that
A17: B <> 0 and
A18: B is limit_ordinal ; :: thesis: ( ex C being Ordinal st
( C in B & not S2[C] ) or S2[B] )

{} in B by ;
then A19: omega c= B by ;
B c= A +^ B by ORDINAL3:24;
hence ( ex C being Ordinal st
( C in B & not S2[C] ) or S2[B] ) by ; :: thesis: verum
end;
A20: for C being Ordinal st S2[C] holds
S2[ succ C]
proof
let C be Ordinal; :: thesis: ( S2[C] implies S2[ succ C] )
assume that
A21: ( A +^ C in dom (nu | omega) & C <> {} implies (nu | omega) . A in (nu | omega) . (A +^ C) ) and
A22: A +^ (succ C) in dom (nu | omega) and
succ C <> {} ; :: thesis: (nu | omega) . A in (nu | omega) . (A +^ (succ C))
A23: A +^ (succ C) in On W by ;
then reconsider asc = A +^ (succ C) as Ordinal of W by ZF_REFLE:7;
A24: A +^ C in asc by ;
then A +^ C in On W by ;
then reconsider ac = A +^ C as Ordinal of W by ZF_REFLE:7;
A25: now :: thesis: ( C = {} implies (nu | omega) . A in (nu | omega) . (A +^ (succ C)) )
nu . ac in dom phi by ORDINAL4:34;
then A26: nu . ac c= phi . (nu . ac) by ;
asc = succ ac by ORDINAL2:28;
then A27: nu . asc = succ (phi . (nu . ac)) by A6;
assume C = {} ; :: thesis: (nu | omega) . A in (nu | omega) . (A +^ (succ C))
then A28: ac = A by ORDINAL2:27;
( (nu | omega) . ac = nu . ac & (nu | omega) . asc = nu . asc ) by ;
hence (nu | omega) . A in (nu | omega) . (A +^ (succ C)) by ; :: thesis: verum
end;
A29: ( succ ac = asc & nu . ac in dom phi ) by ;
A +^ C in dom (nu | omega) by ;
then ( ( (nu | omega) . A in (nu | omega) . ac & nu . asc = succ (phi . (nu . ac)) & nu . ac = (nu | omega) . ac & phi . (nu . ac) in succ (phi . (nu . ac)) & nu . ac c= phi . (nu . ac) ) or C = {} ) by ;
then ( ( (nu | omega) . A in nu . ac & nu . ac in nu . asc & nu . asc = (nu | omega) . asc ) or C = {} ) by ;
then ( ( (nu | omega) . A in nu . ac & nu . ac c= (nu | omega) . asc ) or C = {} ) by ORDINAL1:def 2;
hence (nu | omega) . A in (nu | omega) . (A +^ (succ C)) by A25; :: thesis: verum
end;
A30: S2[ 0 ] ;
A31: for C being Ordinal holds S2[C] from ex C being Ordinal st
( B = A +^ C & C <> {} ) by ;
hence (nu | omega) . A in (nu | omega) . B by ; :: thesis: verum
end;
then A32: a is limit_ordinal by ;
take a ; :: thesis: ( b in a & phi . a = a & a is_cofinal_with omega )
0-element_of W in dom nu by ORDINAL4:34;
then A33: b in rng (nu | omega) by ;
hence b in a by ORDINAL2:19; :: thesis: ( phi . a = a & a is_cofinal_with omega )
A34: a <> {} by ;
a in dom phi by ORDINAL4:34;
then A35: phi . a is_limes_of phi | a by A3, A32, A34;
phi | a is increasing by ;
then sup (phi | a) = lim (phi | a) by ;
then A36: phi . a = sup (rng (phi | a)) by ;
thus phi . a c= a :: according to XBOOLE_0:def 10 :: thesis: ( a c= phi . a & a is_cofinal_with omega )
proof
let A be Ordinal; :: according to ORDINAL1:def 5 :: thesis: ( not A in phi . a or A in a )
assume A in phi . a ; :: thesis: A in a
then consider B being Ordinal such that
A37: B in rng (phi | a) and
A38: A c= B by ;
consider e being object such that
A39: e in a and
A40: B = (phi | a) . e by ;
reconsider e = e as Ordinal by A39;
consider C being Ordinal such that
A41: C in rng (nu | omega) and
A42: e c= C by ;
A43: ( e c< C iff ( e c= C & e <> C ) ) ;
consider u being object such that
A44: u in omega and
A45: C = (nu | omega) . u by ;
reconsider u = u as Ordinal by A44;
u c= omega by ;
then reconsider u = u as Ordinal of W by ;
A46: succ u in dom nu by ORDINAL4:34;
C in a by ;
then ( e = C or ( e in C & C in dom phi ) ) by ;
then A47: ( phi . e = phi . C or phi . e in phi . C ) by A2;
A48: nu . (succ u) = succ (phi . (nu . u)) by A6;
succ u in omega by ;
then nu . (succ u) in rng (nu | omega) by ;
then A49: nu . (succ u) in a by ORDINAL2:19;
C = nu . u by ;
then A50: phi . e c= phi . (nu . u) by ;
phi . e = B by ;
then B in nu . (succ u) by ;
then B in a by ;
hence A in a by ; :: thesis: verum
end;
thus a c= phi . a by ; :: thesis:
take nu | omega ; :: according to ORDINAL2:def 17 :: thesis: ( dom (nu | omega) = omega & rng (nu | omega) c= a & nu | omega is increasing & a = sup (nu | omega) )
rng (nu | omega) c= a
proof
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in rng (nu | omega) or e in a )
assume A51: e in rng (nu | omega) ; :: thesis: e in a
then consider u being object such that
u in dom (nu | omega) and
A52: e = (nu | omega) . u by FUNCT_1:def 3;
thus e in a by ; :: thesis: verum
end;
hence ( dom (nu | omega) = omega & rng (nu | omega) c= a & nu | omega is increasing & a = sup (nu | omega) ) by ; :: thesis: verum