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 A1, ORDINAL1:def 10;
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 . (0-element_of W) = 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 ZF_REFLE:sch 3();
 set xi = nu | omega ;
set a = sup (nu | omega );
A7: On W c= W by ORDINAL2:9;
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:91;
( rng (nu | omega ) c= rng nu & rng nu c= On W ) by RELAT_1:def 19;
then rng (nu | omega ) c= On W by XBOOLE_1:1;
then rng (nu | omega ) c= W by A7, XBOOLE_1:1;
then reconsider a = sup (nu | omega ) as Ordinal of W by A1, A9, Th12, ZF_REFLE:28;
A10: a in dom phi by ORDINAL4:36;
then A11: a c= dom phi by ORDINAL1:def 2;
then A12: dom (phi | a) = a by RELAT_1:91;
A13: nu | omega is increasing
proof
let A be Ordinal; :: according to ORDINAL2:def 16 :: thesis: for b1 being set holds
( not A in b1 or not b1 in proj1 (nu | omega ) or (nu | omega ) . A in (nu | omega ) . b1 )
let B be Ordinal; :: thesis: ( not A in B or not B in proj1 (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 <> {} & 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 <> {} & B is limit_ordinal & ( for C being Ordinal st C in B holds
S2[C] ) implies S2[B] )
assume that
A17: B <> {} and
A18: B is limit_ordinal ; :: thesis: ( ex C being Ordinal st
( C in B & not S2[C] ) or S2[B] )
{} in B by A17, ORDINAL3:10;
then A19: omega c= B by A18, ORDINAL1:def 12;
B c= A +^ B by ORDINAL3:27;
hence ( ex C being Ordinal st
( C in B & not S2[C] ) or S2[B] ) by A9, A19, ORDINAL1:7; :: 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 A4, A9, A22, ORDINAL1:19;
then reconsider asc = A +^ (succ C) as Ordinal of W by ZF_REFLE:8;
A24: A +^ C in asc by ORDINAL1:10, ORDINAL2:49;
then A +^ C in On W by A23, ORDINAL1:19;
then reconsider ac = A +^ C as Ordinal of W by ZF_REFLE:8;
A25: now
nu . ac in dom phi by ORDINAL4:36;
then A26: nu . ac c= phi . (nu . ac) by A2, ORDINAL4:10;
asc = succ ac by ORDINAL2:45;
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:44;
( (nu | omega ) . ac = nu . ac & (nu | omega ) . asc = nu . asc ) by A22, A24, FUNCT_1:70, ORDINAL1:19;
hence (nu | omega ) . A in (nu | omega ) . (A +^ (succ C)) by A28, A27, A26, ORDINAL1:10, ORDINAL1:22; :: thesis: verum
end;
A29: ( succ ac = asc & nu . ac in dom phi ) by ORDINAL2:45, ORDINAL4:36;
A +^ C in dom (nu | omega ) by A22, A24, ORDINAL1:19;
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 A2, A6, A21, A29, FUNCT_1:70, ORDINAL1:10, ORDINAL4:10;
then ( ( (nu | omega ) . A in nu . ac & nu . ac in nu . asc & nu . asc = (nu | omega ) . asc ) or C = {} ) by A22, FUNCT_1:70, ORDINAL1:22;
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[ {} ] ;
A31: for C being Ordinal holds S2[C] from ORDINAL2:sch 1(A30, A20, A16);
 ex C being Ordinal st
( B = A +^ C & C <> {} ) by A14, ORDINAL3:31;
hence (nu | omega ) . A in (nu | omega ) . B by A15, A31; :: thesis: verum
end;
then A32: a is limit_ordinal by A9, Lm2, ORDINAL4:16;
take a ; :: thesis: ( b in a & phi . a = a & a is_cofinal_with omega )
0-element_of W in dom nu by ORDINAL4:36;
then A33: b in rng (nu | omega ) by A5, Lm1, FUNCT_1:73;
hence b in a by ORDINAL2:27; :: thesis: ( phi . a = a & a is_cofinal_with omega )
A34: a <> {} by A33, ORDINAL2:27;
a in dom phi by ORDINAL4:36;
then A35: phi . a is_limes_of phi | a by A3, A32, A34, ORDINAL2:def 17;
phi | a is increasing by A2, ORDINAL4:15;
then sup (phi | a) = lim (phi | a) by A32, A34, A12, ORDINAL4:8;
then A36: phi . a = sup (rng (phi | a)) by A35, ORDINAL2:def 14;
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 A36, ORDINAL2:29;
consider e being set such that
A39: e in a and
A40: B = (phi | a) . e by A12, A37, FUNCT_1:def 5;
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 A39, ORDINAL2:29;
A43: ( e c< C iff ( e c= C & e <> C ) ) by XBOOLE_0:def 8;
consider u being set such that
A44: u in omega and
A45: C = (nu | omega ) . u by A9, A41, FUNCT_1:def 5;
reconsider u = u as Ordinal by A44;
u c= omega by A44, ORDINAL1:def 2;
then reconsider u = u as Ordinal of W by A1, CLASSES1:def 1;
A46: succ u in dom nu by ORDINAL4:36;
C in a by A41, ORDINAL2:27;
then ( e = C or ( e in C & C in dom phi ) ) by A11, A42, A43, ORDINAL1:21;
then A47: ( phi . e = phi . C or phi . e in phi . C ) by A2, ORDINAL2:def 16;
A48: nu . (succ u) = succ (phi . (nu . u)) by A6;
succ u in omega by A44, Lm2, ORDINAL1:41;
then nu . (succ u) in rng (nu | omega ) by A46, FUNCT_1:73;
then A49: nu . (succ u) in a by ORDINAL2:27;
C = nu . u by A9, A44, A45, FUNCT_1:70;
then A50: phi . e c= phi . (nu . u) by A47, ORDINAL1:def 2;
phi . e = B by A12, A39, A40, FUNCT_1:70;
then B in nu . (succ u) by A48, A50, ORDINAL1:10, ORDINAL1:22;
then B in a by A49, ORDINAL1:19;
hence A in a by A38, ORDINAL1:22; :: thesis: verum
end;
thus a c= phi . a by A2, A10, ORDINAL4:10; :: thesis: a is_cofinal_with omega
take nu | omega ; :: according to ORDINAL2:def 21 :: thesis: ( proj1 (nu | omega ) = omega & proj2 (nu | omega ) c= a & nu | omega is increasing & a = sup (nu | omega ) )
rng (nu | omega ) c= a
proof
let e be set ; :: 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 set such that
A52: u in dom (nu | omega ) and
A53: e = (nu | omega ) . u by FUNCT_1:def 5;
thus e in a by A51, A52, A53, ORDINAL2:27; :: thesis: verum
reconsider u = u as Ordinal by A52;
end;
hence ( proj1 (nu | omega ) = omega & proj2 (nu | omega ) c= a & nu | omega is increasing & a = sup (nu | omega ) ) by A8, A13, RELAT_1:91; :: thesis: verum