let W be Universe; :: thesis: for phi being Ordinal-Sequence of W st phi is increasing & phi is continuous & omega in W holds
ex A being Ordinal st
( A in dom phi & phi . A = A )
let phi be Ordinal-Sequence of W; :: thesis: ( phi is increasing & phi is continuous & omega in W implies ex A being Ordinal st
( A in dom phi & phi . A = A ) )
assume that
A1: phi is increasing and
A2: phi is continuous and
A3: omega in W ; :: thesis: ex A being Ordinal st
( A in dom phi & phi . A = A )
assume A4: for A being Ordinal holds
( not A in dom phi or not phi . A = A ) ; :: thesis: contradiction
reconsider N = phi . (0-element_of W) as Ordinal ;
deffunc H₁( set , set ) -> set = phi . $2;
deffunc H₂( set , set ) -> set = {} ;
consider L being T-Sequence such that
A5: dom L = omega and
A6: ( {} in omega implies L . {} = N ) and
A7: for A being Ordinal st succ A in omega holds
L . (succ A) = H₁(A,L . A) and
for A being Ordinal st A in omega & A <> {} & A is limit_ordinal holds
L . A = H₂(A,L | A) from ORDINAL2:sch 5();
defpred S₁[ Ordinal] means ( $1 in dom L implies L . $1 is Ordinal of W );
A8: S₁[ {} ] by A5, A6;
A9: for A being Ordinal st S₁[A] holds
S₁[ succ A]

proof

let A be Ordinal; :: thesis: ( S₁[A] implies S₁[ succ A] )
assume that
A10: ( A in dom L implies L . A is Ordinal of W ) and
A11: succ A in dom L ; :: thesis: L . (succ A) is Ordinal of W
A in succ A by ORDINAL1:10;
then reconsider x = L . A as Ordinal of W by A10, A11, ORDINAL1:19;
L . (succ A) = phi . x by A5, A7, A11;
hence L . (succ A) is Ordinal of W ; :: thesis: verum

end;

A12: for A being Ordinal st A <> {} & A is limit_ordinal & ( for B being Ordinal st B in A holds
S₁[B] ) holds
S₁[A]

proof

let A be Ordinal; :: thesis: ( A <> {} & A is limit_ordinal & ( for B being Ordinal st B in A holds
S₁[B] ) implies S₁[A] )
assume that
A13: ( A <> {} & A is limit_ordinal ) and
for B being Ordinal st B in A & B in dom L holds
L . B is Ordinal of W and
A14: A in dom L ; :: thesis: L . A is Ordinal of W
{} in A by A13, ORDINAL3:10;
then omega c= A by A13, ORDINAL1:def 12;
hence L . A is Ordinal of W by A5, A14, ORDINAL1:7; :: thesis: verum

end;

A15: for A being Ordinal holds S₁[A] from ORDINAL2:sch 1(A8, A9, A12);
rng L c= sup (rng L)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng L or x in sup (rng L) )
assume A16: x in rng L ; :: thesis: x in sup (rng L)
then consider y being set such that
A17: ( y in dom L & x = L . y ) by FUNCT_1:def 5;
reconsider y = y as Ordinal by A17;
reconsider A = L . y as Ordinal of W by A15, A17;
A in sup (rng L) by A16, A17, ORDINAL2:27;
hence x in sup (rng L) by A17; :: thesis: verum

end;

then reconsider L = L as Ordinal-Sequence by ORDINAL2:def 8;

A18: now

let A1 be Ordinal of W; :: thesis: A1 in phi . A1
A1 in dom phi by Th36;
then ( A1 c= phi . A1 & A1 <> phi . A1 ) by A1, A4, Th10;
then A1 c< phi . A1 by XBOOLE_0:def 8;
hence A1 in phi . A1 by ORDINAL1:21; :: thesis: verum

end;

A19: L is increasing

proof

let A be Ordinal; :: according to ORDINAL2:def 16 :: thesis: for b₁ being set holds
( not A in b₁ or not b₁ in dom L or L . A in L . b₁ )
let B be Ordinal; :: thesis: ( not A in B or not B in dom L or L . A in L . B )
assume A20: ( A in B & B in dom L ) ; :: thesis: L . A in L . B
then A21: ex C being Ordinal st
( B = A +^ C & C <> {} ) by ORDINAL3:31;
defpred S₂[ Ordinal] means ( A +^ $1 in omega & $1 <> {} implies L . A in L . (A +^ $1) );
A22: S₂[ {} ] ;
A23: for C being Ordinal st S₂[C] holds
S₂[ succ C]

proof

let C be Ordinal; :: thesis: ( S₂[C] implies S₂[ succ C] )
assume that
A24: ( A +^ C in omega & C <> {} implies L . A in L . (A +^ C) ) and
A25: ( A +^ (succ C) in omega & succ C <> {} ) ; :: thesis: L . A in L . (A +^ (succ C))
A26: ( A +^ C in succ (A +^ C) & A +^ (succ C) = succ (A +^ C) ) by ORDINAL1:10, ORDINAL2:45;
then reconsider D = L . (A +^ C) as Ordinal of W by A5, A15, A25, ORDINAL1:19;
( L . (A +^ (succ C)) = phi . D & D in phi . D & A +^ {} = A ) by A7, A18, A25, A26, ORDINAL2:44;
hence L . A in L . (A +^ (succ C)) by A24, A25, A26, ORDINAL1:19; :: thesis: verum

end;

A27: for B being Ordinal st B <> {} & B is limit_ordinal & ( for C being Ordinal st C in B holds
S₂[C] ) holds
S₂[B]

proof

let B be Ordinal; :: thesis: ( B <> {} & B is limit_ordinal & ( for C being Ordinal st C in B holds
S₂[C] ) implies S₂[B] )
assume that
A28: ( B <> {} & B is limit_ordinal ) and
for C being Ordinal st C in B & A +^ C in omega & C <> {} holds
L . A in L . (A +^ C) and
A29: ( A +^ B in omega & B <> {} ) ; :: thesis: L . A in L . (A +^ B)
A +^ B <> {} by A29, ORDINAL3:29;
then ( A +^ B is limit_ordinal & {} in A +^ B ) by A28, ORDINAL3:10, ORDINAL3:32;
then omega c= A +^ B by ORDINAL1:def 12;
hence L . A in L . (A +^ B) by A29, ORDINAL1:7; :: thesis: verum

end;

for C being Ordinal holds S₂[C] from ORDINAL2:sch 1(A22, A23, A27);
hence L . A in L . B by A5, A20, A21; :: thesis: verum

end;

set fi = phi | (sup L);
( N in rng L & sup (rng L) = sup L ) by A5, A6, Lm1, FUNCT_1:def 5;
then A30: ( sup L <> {} & sup L is limit_ordinal ) by A5, A19, Lm2, Th16, ORDINAL2:27;
A31: rng L c= W

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng L or x in W )
assume x in rng L ; :: thesis: x in W
then consider y being set such that
A32: ( y in dom L & x = L . y ) by FUNCT_1:def 5;
reconsider y = y as Ordinal by A32;
L . y is Ordinal of W by A15, A32;
hence x in W by A32, Def2; :: thesis: verum

end;

then A33: sup L in W by A3, A5, Th37;
then reconsider S = sup L as Ordinal of W by Def2;
A34: ( S in On W & dom phi = On W ) by A33, Def3, ORDINAL1:def 10;
then A35: phi . S is_limes_of phi | (sup L) by A2, A30, ORDINAL2:def 17;
S c= dom phi by A34, ORDINAL1:def 2;
then A36: dom (phi | (sup L)) = S by RELAT_1:91;
phi | (sup L) is increasing

proof

let A be Ordinal; :: according to ORDINAL2:def 16 :: thesis: for b₁ being set holds
( not A in b₁ or not b₁ in dom (phi | (sup L)) or (phi | (sup L)) . A in (phi | (sup L)) . b₁ )
let B be Ordinal; :: thesis: ( not A in B or not B in dom (phi | (sup L)) or (phi | (sup L)) . A in (phi | (sup L)) . B )
assume A37: ( A in B & B in dom (phi | (sup L)) ) ; :: thesis: (phi | (sup L)) . A in (phi | (sup L)) . B
then ( A in dom (phi | (sup L)) & dom (phi | (sup L)) c= dom phi ) by ORDINAL1:19, RELAT_1:89;
then ( (phi | (sup L)) . A = phi . A & (phi | (sup L)) . B = phi . B & B in dom phi ) by A37, FUNCT_1:70;
hence (phi | (sup L)) . A in (phi | (sup L)) . B by A1, A37, ORDINAL2:def 16; :: thesis: verum

end;

then A38: sup (phi | (sup L)) = lim (phi | (sup L)) by A30, A36, Th8
.= phi . (sup L) by A35, ORDINAL2:def 14 ;
sup (phi | (sup L)) c= sup L

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in sup (phi | (sup L)) or x in sup L )
assume A39: x in sup (phi | (sup L)) ; :: thesis: x in sup L
then reconsider A = x as Ordinal ;
consider B being Ordinal such that
A40: ( B in rng (phi | (sup L)) & A c= B ) by A39, ORDINAL2:29;
consider y being set such that
A41: ( y in dom (phi | (sup L)) & B = (phi | (sup L)) . y ) by A40, FUNCT_1:def 5;
reconsider y = y as Ordinal by A41;
consider C being Ordinal such that
A42: ( C in rng L & y c= C ) by A36, A41, ORDINAL2:29;
consider z being set such that
A43: ( z in dom L & C = L . z ) by A42, FUNCT_1:def 5;
reconsider z = z as Ordinal by A43;
succ z in omega by A5, A43, Lm2, ORDINAL1:41;
then A44: ( L . (succ z) = phi . C & L . (succ z) in rng L & B = phi . y ) by A5, A7, A41, A43, FUNCT_1:70, FUNCT_1:def 5;
reconsider C1 = C as Ordinal of W by A31, A42, Def2;
( y c< C1 iff ( y c= C1 & y <> C1 ) ) by XBOOLE_0:def 8;
then ( ( y in C1 & C1 in dom phi ) or y = C ) by A31, A34, A42, ORDINAL1:21, ORDINAL1:def 10;
then ( phi . y in phi . C1 or y = C1 ) by A1, ORDINAL2:def 16;
then ( B c= phi . C1 & phi . C1 in sup L ) by A44, ORDINAL1:def 2, ORDINAL2:27;
then B in sup L by ORDINAL1:22;
hence x in sup L by A40, ORDINAL1:22; :: thesis: verum

end;

then not S in phi . S by A38, ORDINAL1:7;
hence contradiction by A18; :: thesis: verum