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 H_{1}( 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 H_{2}( 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) = H_{2}(A,L . A)
and

for A being Ordinal st A in omega & A <> 0 & A is limit_ordinal holds

L . A = H_{1}(A,L | A)
from ORDINAL2:sch 5();

defpred S_{1}[ Ordinal] means ( $1 in dom L implies L . $1 is Ordinal of W );

A7: for A being Ordinal st S_{1}[A] holds

S_{1}[ succ A]

S_{1}[B] ) holds

S_{1}[A]
_{1}[ 0 ]
by A4, A5;

A15: for A being Ordinal holds S_{1}[A]
from ORDINAL2:sch 1(A14, A7, A10);

rng L c= sup (rng L)

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

A40: rng L c= W

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

.= phi . (sup L) by A45, ORDINAL2:def 10 ;

then not S in phi . S by A47, ORDINAL1:5;

hence contradiction by A21; :: thesis: verum

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 H

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 H

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) = H

for A being Ordinal st A in omega & A <> 0 & A is limit_ordinal holds

L . A = H

defpred S

A7: for A being Ordinal st S

S

proof

A10:
for A being Ordinal st A <> 0 & A is limit_ordinal & ( for B being Ordinal st B in A holds
let A be Ordinal; :: thesis: ( S_{1}[A] implies S_{1}[ 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;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

S

S

proof

A14:
S
let A be Ordinal; :: thesis: ( A <> 0 & A is limit_ordinal & ( for B being Ordinal st B in A holds

S_{1}[B] ) implies S_{1}[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;S

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

A15: for A being Ordinal holds S

rng L c= sup (rng L)

proof

then reconsider L = L as Ordinal-Sequence by ORDINAL2:def 4;
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;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

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

L is increasing
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;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

proof

then A39:
sup L is limit_ordinal
by A4, Lm2, Th16;
let A be Ordinal; :: according to ORDINAL2:def 12 :: thesis: for b_{1} being set holds

( not A in b_{1} or not b_{1} in dom L or L . A in L . b_{1} )

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 S_{2}[ 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

S_{2}[C] ) holds

S_{2}[B]
_{2}[C] holds

S_{2}[ succ C]
_{2}[ 0 ]
;

A38: for C being Ordinal holds S_{2}[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;( not A in b

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 S

A25: for B being Ordinal st B <> 0 & B is limit_ordinal & ( for C being Ordinal st C in B holds

S

S

proof

A31:
for C being Ordinal st S
let B be Ordinal; :: thesis: ( B <> 0 & B is limit_ordinal & ( for C being Ordinal st C in B holds

S_{2}[C] ) implies S_{2}[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;S

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

S

proof

A37:
S
let C be Ordinal; :: thesis: ( S_{2}[C] implies S_{2}[ 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;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

A38: for C being Ordinal holds S

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

A40: rng L c= W

proof

then reconsider S = sup L as Ordinal of W by A3, A4, Th35;
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;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

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

phi | (sup L) is increasing
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;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

proof

then sup (phi | (sup L)) =
lim (phi | (sup L))
by A43, A39, A46, Th8
A61:
dom (phi | (sup L)) c= dom phi
by RELAT_1:60;

let A be Ordinal; :: according to ORDINAL2:def 12 :: thesis: for b_{1} being set holds

( not A in b_{1} or not b_{1} in dom (phi | (sup L)) or (phi | (sup L)) . A in (phi | (sup L)) . b_{1} )

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;let A be Ordinal; :: according to ORDINAL2:def 12 :: thesis: for b

( not A in 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 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

.= phi . (sup L) by A45, ORDINAL2:def 10 ;

then not S in phi . S by A47, ORDINAL1:5;

hence contradiction by A21; :: thesis: verum