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 H_{1}( Ordinal, set ) -> Element of W = 0-element_of W;

deffunc H_{2}( 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) = H_{2}(a,nu . a)
and

for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal holds

nu . a = H_{1}(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

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 )

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

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 H

deffunc H

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

for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal holds

nu . a = H

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

then A32:
a is limit_ordinal
by A9, Lm2, ORDINAL4:16;
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 (nu | omega) or (nu | omega) . A in (nu | omega) . b_{1} )

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

S_{2}[C] ) holds

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

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

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

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 S

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

S

S

proof

A20:
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

A17: B <> 0 and

A18: B is limit_ordinal ; :: thesis: ( ex C being Ordinal st

( C in B & not S_{2}[C] ) or S_{2}[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 S_{2}[C] ) or S_{2}[B] )
by A9, A19, ORDINAL1:5; :: thesis: verum

end;S

assume that

A17: B <> 0 and

A18: B is limit_ordinal ; :: thesis: ( ex C being Ordinal st

( C in B & not S

{} 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 S

S

proof

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

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;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)) )

A29:
( succ ac = asc & nu . ac in dom phi )
by ORDINAL2:28, ORDINAL4:34;
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;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

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

A31: for C being Ordinal holds S

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

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

thus
a c= phi . a
by A2, A10, ORDINAL4:10; :: thesis: a is_cofinal_with omega
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;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

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

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
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;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