A3: now :: thesis: for A being Ordinal holds not S_{1}[A]

deffunc Hdefpred S_{1}[ Ordinal] means not $1 c= F_{1}($1);

assume A4: ex A being Ordinal st S_{1}[A]
; :: thesis: contradiction

consider A being Ordinal such that

A5: S_{1}[A]
and

A6: for B being Ordinal st S_{1}[B] holds

A c= B from ORDINAL1:sch 1(A4);

F_{1}(F_{1}(A)) in F_{1}(A)
by A1, A5, ORDINAL1:16;

then not F_{1}(A) c= F_{1}(F_{1}(A))
by ORDINAL1:5;

hence contradiction by A5, A6; :: thesis: verum

end;assume A4: ex A being Ordinal st S

consider A being Ordinal such that

A5: S

A6: for B being Ordinal st S

A c= B from ORDINAL1:sch 1(A4);

F

then not F

hence contradiction by A5, A6; :: thesis: verum

deffunc H

consider phi being Ordinal-Sequence such that

A7: dom phi = omega and

A8: ( 0 in omega implies phi . 0 = F

A9: for A being Ordinal st succ A in omega holds

phi . (succ A) = H

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

phi . A = H

assume A10: for A being Ordinal holds not F

A11: now :: thesis: for A being Ordinal holds A in F_{1}(A)

A13:
phi is increasing
let A be Ordinal; :: thesis: A in F_{1}(A)

A12: A <> F_{1}(A)
by A10;

A c= F_{1}(A)
by A3;

then A c< F_{1}(A)
by A12;

hence A in F_{1}(A)
by ORDINAL1:11; :: thesis: verum

end;A12: A <> F

A c= F

then A c< F

hence A in F

proof

deffunc H
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 or phi . A in phi . b_{1} )

let B be Ordinal; :: thesis: ( not A in B or not B in dom phi or phi . A in phi . B )

assume that

A14: A in B and

A15: B in dom phi ; :: thesis: phi . A in phi . B

defpred S_{1}[ Ordinal] means ( A +^ $1 in omega & $1 <> {} implies phi . A in phi . (A +^ $1) );

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

S_{1}[C] ) holds

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

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

A29: for C being Ordinal holds S_{1}[C]
from ORDINAL2:sch 1(A28, A22, A16);

ex C being Ordinal st

( B = A +^ C & C <> {} ) by A14, ORDINAL3:28;

hence phi . A in phi . B by A7, A15, A29; :: thesis: verum

end;( not A in b

let B be Ordinal; :: thesis: ( not A in B or not B in dom phi or phi . A in phi . B )

assume that

A14: A in B and

A15: B in dom phi ; :: thesis: phi . A in phi . 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

A22:
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_{1}[C] ) implies S_{1}[B] )

assume that

A17: B <> 0 and

A18: B is limit_ordinal and

for C being Ordinal st C in B & A +^ C in omega & C <> {} holds

phi . A in phi . (A +^ C) and

A19: A +^ B in omega and

A20: B <> {} ; :: thesis: phi . A in phi . (A +^ B)

A +^ B <> {} by A20, ORDINAL3:26;

then A21: {} in A +^ B by ORDINAL3:8;

A +^ B is limit_ordinal by A17, A18, ORDINAL3:29;

then omega c= A +^ B by A21, ORDINAL1:def 11;

hence phi . A in phi . (A +^ B) by A19, ORDINAL1:5; :: thesis: verum

end;S

assume that

A17: B <> 0 and

A18: B is limit_ordinal and

for C being Ordinal st C in B & A +^ C in omega & C <> {} holds

phi . A in phi . (A +^ C) and

A19: A +^ B in omega and

A20: B <> {} ; :: thesis: phi . A in phi . (A +^ B)

A +^ B <> {} by A20, ORDINAL3:26;

then A21: {} in A +^ B by ORDINAL3:8;

A +^ B is limit_ordinal by A17, A18, ORDINAL3:29;

then omega c= A +^ B by A21, ORDINAL1:def 11;

hence phi . A in phi . (A +^ B) by A19, ORDINAL1:5; :: thesis: verum

S

proof

A28:
S
let C be Ordinal; :: thesis: ( S_{1}[C] implies S_{1}[ succ C] )

assume that

A23: ( A +^ C in omega & C <> {} implies phi . A in phi . (A +^ C) ) and

A24: A +^ (succ C) in omega and

succ C <> {} ; :: thesis: phi . A in phi . (A +^ (succ C))

reconsider D = phi . (A +^ C) as Ordinal ;

A25: A +^ C in succ (A +^ C) by ORDINAL1:6;

A26: D in F_{1}(D)
by A11;

A27: A +^ (succ C) = succ (A +^ C) by ORDINAL2:28;

then phi . (A +^ (succ C)) = F_{1}(D)
by A9, A24;

hence phi . A in phi . (A +^ (succ C)) by A23, A24, A25, A27, A26, ORDINAL1:10, ORDINAL2:27; :: thesis: verum

end;assume that

A23: ( A +^ C in omega & C <> {} implies phi . A in phi . (A +^ C) ) and

A24: A +^ (succ C) in omega and

succ C <> {} ; :: thesis: phi . A in phi . (A +^ (succ C))

reconsider D = phi . (A +^ C) as Ordinal ;

A25: A +^ C in succ (A +^ C) by ORDINAL1:6;

A26: D in F

A27: A +^ (succ C) = succ (A +^ C) by ORDINAL2:28;

then phi . (A +^ (succ C)) = F

hence phi . A in phi . (A +^ (succ C)) by A23, A24, A25, A27, A26, ORDINAL1:10, ORDINAL2:27; :: thesis: verum

A29: for C being Ordinal holds S

ex C being Ordinal st

( B = A +^ C & C <> {} ) by A14, ORDINAL3:28;

hence phi . A in phi . B by A7, A15, A29; :: thesis: verum

consider fi being Ordinal-Sequence such that

A30: ( dom fi = sup phi & ( for A being Ordinal st A in sup phi holds

fi . A = H

H

then A31: sup phi <> {} by ORDINAL2:19;

then A32: H

A33: sup fi c= sup phi

proof

A47:
fi is increasing
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in sup fi or x in sup phi )

assume A34: x in sup fi ; :: thesis: x in sup phi

then reconsider A = x as Ordinal ;

consider B being Ordinal such that

A35: B in rng fi and

A36: A c= B by A34, ORDINAL2:21;

consider y being object such that

A37: y in dom fi and

A38: B = fi . y by A35, FUNCT_1:def 3;

reconsider y = y as Ordinal by A37;

consider C being Ordinal such that

A39: C in rng phi and

A40: y c= C by A30, A37, ORDINAL2:21;

( y c< C iff ( y <> C & y c= C ) ) ;

then A41: ( H_{3}(y) in H_{3}(C) or y = C )
by A1, A40, ORDINAL1:11;

B = H_{3}(y)
by A30, A37, A38;

then A42: B c= H_{3}(C)
by A41, ORDINAL1:def 2;

consider z being object such that

A43: z in dom phi and

A44: C = phi . z by A39, FUNCT_1:def 3;

reconsider z = z as Ordinal by A43;

A45: succ z in omega by A7, A43, Lm2, ORDINAL1:28;

then A46: phi . (succ z) in rng phi by A7, FUNCT_1:def 3;

phi . (succ z) = H_{3}(C)
by A9, A44, A45;

then H_{3}(C) in sup phi
by A46, ORDINAL2:19;

then B in sup phi by A42, ORDINAL1:12;

hence x in sup phi by A36, ORDINAL1:12; :: thesis: verum

end;assume A34: x in sup fi ; :: thesis: x in sup phi

then reconsider A = x as Ordinal ;

consider B being Ordinal such that

A35: B in rng fi and

A36: A c= B by A34, ORDINAL2:21;

consider y being object such that

A37: y in dom fi and

A38: B = fi . y by A35, FUNCT_1:def 3;

reconsider y = y as Ordinal by A37;

consider C being Ordinal such that

A39: C in rng phi and

A40: y c= C by A30, A37, ORDINAL2:21;

( y c< C iff ( y <> C & y c= C ) ) ;

then A41: ( H

B = H

then A42: B c= H

consider z being object such that

A43: z in dom phi and

A44: C = phi . z by A39, FUNCT_1:def 3;

reconsider z = z as Ordinal by A43;

A45: succ z in omega by A7, A43, Lm2, ORDINAL1:28;

then A46: phi . (succ z) in rng phi by A7, FUNCT_1:def 3;

phi . (succ z) = H

then H

then B in sup phi by A42, ORDINAL1:12;

hence x in sup phi by A36, ORDINAL1:12; :: thesis: verum

proof

sup phi is limit_ordinal
by A7, A13, 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 fi or fi . A in fi . b_{1} )

let B be Ordinal; :: thesis: ( not A in B or not B in dom fi or fi . A in fi . B )

assume that

A48: A in B and

A49: B in dom fi ; :: thesis: fi . A in fi . B

A50: fi . B = H_{3}(B)
by A30, A49;

fi . A = H_{3}(A)
by A30, A48, A49, ORDINAL1:10;

hence fi . A in fi . B by A1, A48, A50; :: thesis: verum

end;( not A in b

let B be Ordinal; :: thesis: ( not A in B or not B in dom fi or fi . A in fi . B )

assume that

A48: A in B and

A49: B in dom fi ; :: thesis: fi . A in fi . B

A50: fi . B = H

fi . A = H

hence fi . A in fi . B by A1, A48, A50; :: thesis: verum

then sup fi = lim fi by A30, A31, A47, Th8

.= H

hence contradiction by A11, A33, ORDINAL1:5; :: thesis: verum