A3: now :: thesis: for A being Ordinal holds not S1[A]
defpred S1[ Ordinal] means not $1 c= F1($1);
assume A4: ex A being Ordinal st S1[A] ; :: thesis: contradiction
consider A being Ordinal such that
A5: S1[A] and
A6: for B being Ordinal st S1[B] holds
A c= B from ORDINAL1:sch 1(A4);
 F1(F1(A)) in F1(A) by A1, A5, ORDINAL1:16;
then not F1(A) c= F1(F1(A)) by ORDINAL1:5;
hence contradiction by A5, A6; :: thesis: verum
end;
deffunc H1( Ordinal, Sequence) -> set = {} ;
deffunc H2( Ordinal, Ordinal) -> Ordinal = F1($2);
consider phi being Ordinal-Sequence such that
A7: dom phi = omega and
A8: ( 0 in omega implies phi . 0 = F1(0) ) and
A9: for A being Ordinal st succ A in omega holds
phi . (succ A) = H2(A,phi . A) and
for A being Ordinal st A in omega & A <> 0 & A is limit_ordinal holds
phi . A = H1(A,phi | A) from ORDINAL2:sch 11();
 assume A10: for A being Ordinal holds not F1(A) = A ; :: thesis: contradiction
A11: now :: thesis: for A being Ordinal holds A in F1(A)
let A be Ordinal; :: thesis: A in F1(A)
A12: A <> F1(A) by A10;
A c= F1(A) by A3;
then A c< F1(A) by A12;
hence A in F1(A) by ORDINAL1:11; :: thesis: verum
end;
A13: phi 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 phi or phi . A in phi . b1 )
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 S1[ 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
S1[C] ) holds
S1[B]
proof
let B be Ordinal; :: thesis: ( B <> 0 & B is limit_ordinal & ( for C being Ordinal st C in B holds
S1[C] ) implies S1[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;
A22: for C being Ordinal st S1[C] holds
S1[ succ C]
proof
let C be Ordinal; :: thesis: ( S1[C] implies S1[ 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 F1(D) by A11;
A27: A +^ (succ C) = succ (A +^ C) by ORDINAL2:28;
then phi . (A +^ (succ C)) = F1(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;
A28: S1[ 0 ] ;
A29: for C being Ordinal holds S1[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;
deffunc H3( Ordinal) -> Ordinal = F1($1);
consider fi being Ordinal-Sequence such that
A30: ( dom fi = sup phi & ( for A being Ordinal st A in sup phi holds
fi . A = H3(A) ) ) from ORDINAL2:sch 3();
 H3( {} ) in rng phi by A7, A8, Lm1, FUNCT_1:def 3;
then A31: sup phi <> {} by ORDINAL2:19;
then A32: H3( sup phi) is_limes_of fi by A2, A7, A13, A30, Lm2, Th16;
A33: sup fi c= sup phi
proof
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: ( H3(y) in H3(C) or y = C ) by A1, A40, ORDINAL1:11;
B = H3(y) by A30, A37, A38;
then A42: B c= H3(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) = H3(C) by A9, A44, A45;
then H3(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;
A47: fi 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 fi or fi . A in fi . b1 )
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 = H3(B) by A30, A49;
fi . A = H3(A) by A30, A48, A49, ORDINAL1:10;
hence fi . A in fi . B by A1, A48, A50; :: thesis: verum
end;
sup phi is limit_ordinal by A7, A13, Lm2, Th16;
then sup fi = lim fi by A30, A31, A47, Th8
.= H3( sup phi) by A32, ORDINAL2:def 10 ;
hence contradiction by A11, A33, ORDINAL1:5; :: thesis: verum