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 ) )
deffunc H1( set , set ) -> set = {} ;
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 )
deffunc H2( set , set ) -> set = phi . $2;
reconsider N = phi . (0-element_of W) as Ordinal ;
consider L being Sequence such that
A4: dom L = omega and
A5: ( 0 in omega implies L . 0 = N ) and
A6: for A being Ordinal st succ A in omega holds
L . (succ A) = H2(A,L . A) and
for A being Ordinal st A in omega & A <> 0 & A is limit_ordinal holds
L . A = H1(A,L | A) from ORDINAL2:sch 5();
 defpred S1[ Ordinal] means ( $1 in dom L implies L . $1 is Ordinal of W );
A7: for A being Ordinal st S1[A] holds
S1[ succ A]
proof
let A be Ordinal; :: thesis: ( S1[A] implies S1[ succ A] )
assume that
A8: ( A in dom L implies L . A is Ordinal of W ) and
A9: succ A in dom L ; :: thesis: L . (succ A) is Ordinal of W
A in succ A by ORDINAL1:6;
then reconsider x = L . A as Ordinal of W by A8, A9, ORDINAL1:10;
L . (succ A) = phi . x by A4, A6, A9;
hence L . (succ A) is Ordinal of W ; :: thesis: verum
end;
A10: for A being Ordinal st A <> 0 & A is limit_ordinal & ( for B being Ordinal st B in A holds
S1[B] ) holds
S1[A]
proof
let A be Ordinal; :: thesis: ( A <> 0 & A is limit_ordinal & ( for B being Ordinal st B in A holds
S1[B] ) implies S1[A] )
assume that
A11: A <> 0 and
A12: 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
A13: A in dom L ; :: thesis: L . A is Ordinal of W
{} in A by A11, ORDINAL3:8;
then omega c= A by A12, ORDINAL1:def 11;
hence L . A is Ordinal of W by A4, A13, ORDINAL1:5; :: thesis: verum
end;
A14: S1[ 0 ] by A4, A5;
A15: for A being Ordinal holds S1[A] from ORDINAL2:sch 1(A14, A7, A10);
 rng L c= sup (rng L)
proof
let x be object ; :: 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 object such that
A17: y in dom L and
A18: x = L . y by FUNCT_1:def 3;
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, A18, ORDINAL2:19;
hence x in sup (rng L) by A18; :: thesis: verum
end;
then reconsider L = L as Ordinal-Sequence by ORDINAL2:def 4;
A19: dom phi = On W by FUNCT_2:def 1;
assume A20: for A being Ordinal holds
( not A in dom phi or not phi . A = A ) ; :: thesis: contradiction
A21: now :: thesis: for A1 being Ordinal of W holds A1 in phi . A1
let A1 be Ordinal of W; :: thesis: A1 in phi . A1
A1 in dom phi by Th34;
then A22: A1 c= phi . A1 by A1, Th10;
A1 <> phi . A1 by A20, Th34;
then A1 c< phi . A1 by A22;
hence A1 in phi . A1 by ORDINAL1:11; :: thesis: verum
end;
L 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 L or L . A in L . b1 )
let B be Ordinal; :: thesis: ( not A in B or not B in dom L or L . A in L . B )
assume that
A23: A in B and
A24: B in dom L ; :: thesis: L . A in L . B
defpred S2[ Ordinal] means ( A +^ $1 in omega & $1 <> {} implies L . A in L . (A +^ $1) );
A25: 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
A26: B <> 0 and
A27: 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
A28: A +^ B in omega and
A29: B <> {} ; :: thesis: L . A in L . (A +^ B)
A +^ B <> {} by A29, ORDINAL3:26;
then A30: {} in A +^ B by ORDINAL3:8;
A +^ B is limit_ordinal by A26, A27, ORDINAL3:29;
then omega c= A +^ B by A30, ORDINAL1:def 11;
hence L . A in L . (A +^ B) by A28, ORDINAL1:5; :: thesis: verum
end;
A31: 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
A32: ( A +^ C in omega & C <> {} implies L . A in L . (A +^ C) ) and
A33: A +^ (succ C) in omega and
succ C <> {} ; :: thesis: L . A in L . (A +^ (succ C))
A34: A +^ (succ C) = succ (A +^ C) by ORDINAL2:28;
A35: A +^ C in succ (A +^ C) by ORDINAL1:6;
then reconsider D = L . (A +^ C) as Ordinal of W by A4, A15, A33, A34, ORDINAL1:10;
A36: D in phi . D by A21;
L . (A +^ (succ C)) = phi . D by A6, A33, A34;
hence L . A in L . (A +^ (succ C)) by A32, A33, A35, A34, A36, ORDINAL1:10, ORDINAL2:27; :: thesis: verum
end;
A37: S2[ 0 ] ;
A38: for C being Ordinal holds S2[C] from ORDINAL2:sch 1(A37, A31, A25);
 ex C being Ordinal st
( B = A +^ C & C <> {} ) by A23, ORDINAL3:28;
hence L . A in L . B by A4, A24, A38; :: thesis: verum
end;
then A39: sup L is limit_ordinal by A4, Lm2, Th16;
A40: rng L c= W
proof
let x be object ; :: 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 object such that
A41: y in dom L and
A42: x = L . y by FUNCT_1:def 3;
reconsider y = y as Ordinal by A41;
L . y is Ordinal of W by A15, A41;
hence x in W by A42; :: thesis: verum
end;
then reconsider S = sup L as Ordinal of W by A3, A4, Th35;
set fi = phi | (sup L);
N in rng L by A4, A5, Lm1, FUNCT_1:def 3;
then A43: sup L <> {} by ORDINAL2:19;
A44: S in On W by ORDINAL1:def 9;
then A45: phi . S is_limes_of phi | (sup L) by A2, A43, A39, A19;
S c= dom phi by A44, A19, ORDINAL1:def 2;
then A46: dom (phi | (sup L)) = S by RELAT_1:62;
A47: sup (phi | (sup L)) c= sup L
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in sup (phi | (sup L)) or x in sup L )
assume A48: x in sup (phi | (sup L)) ; :: thesis: x in sup L
then reconsider A = x as Ordinal ;
consider B being Ordinal such that
A49: B in rng (phi | (sup L)) and
A50: A c= B by A48, ORDINAL2:21;
consider y being object such that
A51: y in dom (phi | (sup L)) and
A52: B = (phi | (sup L)) . y by A49, FUNCT_1:def 3;
reconsider y = y as Ordinal by A51;
consider C being Ordinal such that
A53: C in rng L and
A54: y c= C by A46, A51, ORDINAL2:21;
reconsider C1 = C as Ordinal of W by A40, A53;
( y c< C1 iff ( y c= C1 & y <> C1 ) ) ;
then ( ( y in C1 & C1 in dom phi ) or y = C ) by A19, A54, ORDINAL1:11, ORDINAL1:def 9;
then A55: ( phi . y in phi . C1 or y = C1 ) by A1;
B = phi . y by A51, A52, FUNCT_1:47;
then A56: B c= phi . C1 by A55, ORDINAL1:def 2;
consider z being object such that
A57: z in dom L and
A58: C = L . z by A53, FUNCT_1:def 3;
reconsider z = z as Ordinal by A57;
A59: succ z in omega by A4, A57, Lm2, ORDINAL1:28;
then A60: L . (succ z) in rng L by A4, FUNCT_1:def 3;
L . (succ z) = phi . C by A6, A58, A59;
then phi . C1 in sup L by A60, ORDINAL2:19;
then B in sup L by A56, ORDINAL1:12;
hence x in sup L by A50, ORDINAL1:12; :: thesis: verum
end;
phi | (sup L) is increasing
proof
A61: dom (phi | (sup L)) c= dom phi by RELAT_1:60;
let A be Ordinal; :: according to ORDINAL2:def 12 :: thesis: for b1 being set holds
( not A in b1 or not b1 in dom (phi | (sup L)) or (phi | (sup L)) . A in (phi | (sup L)) . b1 )
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 that
A62: A in B and
A63: B in dom (phi | (sup L)) ; :: thesis: (phi | (sup L)) . A in (phi | (sup L)) . B
A64: (phi | (sup L)) . B = phi . B by A63, FUNCT_1:47;
(phi | (sup L)) . A = phi . A by A62, A63, FUNCT_1:47, ORDINAL1:10;
hence (phi | (sup L)) . A in (phi | (sup L)) . B by A1, A62, A63, A61, A64; :: thesis: verum
end;
then sup (phi | (sup L)) = lim (phi | (sup L)) by A43, A39, A46, Th8
.= phi . (sup L) by A45, ORDINAL2:def 10 ;
then not S in phi . S by A47, ORDINAL1:5;
hence contradiction by A21; :: thesis: verum