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 9;
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: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 A1, A9, Th11, ZF_REFLE:19;
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 A17, ORDINAL3:8;
then A19: omega c= B by A18, ORDINAL1:def 11;
B c= A +^ B by ORDINAL3:24;
hence ( ex C being Ordinal st
( C in B & not S2[C] ) or S2[B] ) by A9, A19, ORDINAL1:5; :: 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:10;
then reconsider asc = A +^ (succ C) as Ordinal of W by ZF_REFLE:7;
A24: A +^ C in asc by ORDINAL1:6, ORDINAL2:32;
then A +^ C in On W by A23, ORDINAL1:10;
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 A2, ORDINAL4:10;
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 A22, A24, FUNCT_1:47, ORDINAL1:10;
hence (nu | omega) . A in (nu | omega) . (A +^ (succ C)) by A28, A27, A26, ORDINAL1:6, ORDINAL1:12; :: thesis: verum
end;
A29: ( succ ac = asc & nu . ac in dom phi ) by ORDINAL2:28, ORDINAL4:34;
A +^ C in dom (nu | omega) by A22, A24, ORDINAL1:10;
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:47, ORDINAL1:6, 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:47, ORDINAL1:12;
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 ORDINAL2:sch 1(A30, A20, A16);
 ex C being Ordinal st
( B = A +^ C & C <> {} ) by A14, ORDINAL3:28;
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:34;
then A33: b in rng (nu | omega) by A5, Lm1, FUNCT_1:50;
hence b in a by ORDINAL2:19; :: thesis: ( phi . a = a & a is_cofinal_with omega )
A34: a <> {} by A33, ORDINAL2:19;
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 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 10;
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:21;
consider e being object such that
A39: e in a and
A40: B = (phi | a) . e by A12, A37, FUNCT_1:def 3;
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:21;
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 A9, A41, FUNCT_1:def 3;
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:34;
C in a by A41, ORDINAL2:19;
then ( e = C or ( e in C & C in dom phi ) ) by A11, A42, A43, ORDINAL1:11;
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 A44, Lm2, ORDINAL1:28;
then nu . (succ u) in rng (nu | omega) by A46, FUNCT_1:50;
then A49: nu . (succ u) in a by ORDINAL2:19;
C = nu . u by A9, A44, A45, FUNCT_1:47;
then A50: phi . e c= phi . (nu . u) by A47, ORDINAL1:def 2;
phi . e = B by A12, A39, A40, FUNCT_1:47;
then B in nu . (succ u) by A48, A50, ORDINAL1:6, ORDINAL1:12;
then B in a by A49, ORDINAL1:10;
hence A in a by A38, ORDINAL1:12; :: 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 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 A51, A52, ORDINAL2:19; :: thesis: verum
end;
hence ( dom (nu | omega) = omega & rng (nu | omega) c= a & nu | omega is increasing & a = sup (nu | omega) ) by A8, A13, RELAT_1:62; :: thesis: verum