let e be epsilon Ordinal; :: thesis: first_epsilon_greater_than e = e |^|^ omega
deffunc H₁( Ordinal) -> set = exp (omega,$1);
A1: for a, b being Ordinal st a in b holds
H₁(a) in H₁(b) by ORDINAL4:24;

A2: now :: thesis: for a being Ordinal st not a is empty & a is limit_ordinal holds
for phi being Ordinal-Sequence st dom phi = a & ( for b being Ordinal st b in a holds
phi . b = H₁(b) ) holds
H₁(a) is_limes_of phi

let a be Ordinal; :: thesis: ( not a is empty & a is limit_ordinal implies for phi being Ordinal-Sequence st dom phi = a & ( for b being Ordinal st b in a holds
phi . b = H₁(b) ) holds
H₁(a) is_limes_of phi )
assume A3: ( not a is empty & a is limit_ordinal ) ; :: thesis: for phi being Ordinal-Sequence st dom phi = a & ( for b being Ordinal st b in a holds
phi . b = H₁(b) ) holds
H₁(a) is_limes_of phi
let phi be Ordinal-Sequence; :: thesis: ( dom phi = a & ( for b being Ordinal st b in a holds
phi . b = H₁(b) ) implies H₁(a) is_limes_of phi )
assume A4: ( dom phi = a & ( for b being Ordinal st b in a holds
phi . b = H₁(b) ) ) ; :: thesis: H₁(a) is_limes_of phi
phi is non-decreasing

proof

let b be Ordinal; :: according to ORDINAL5:def 2 :: thesis: for b being Ordinal st b in b & b in dom phi holds
phi . b c= phi . b
let c be Ordinal; :: thesis: ( b in c & c in dom phi implies phi . b c= phi . c )
assume A5: ( b in c & c in dom phi ) ; :: thesis: phi . b c= phi . c
then ( phi . b = H₁(b) & phi . c = H₁(c) ) by A4, ORDINAL1:10;
then phi . b in phi . c by A5, ORDINAL4:24;
hence phi . b c= phi . c by ORDINAL1:def 2; :: thesis: verum

end;

then ( Union phi is_limes_of phi & H₁(a) = lim phi ) by A3, A4, Th6, ORDINAL2:45;
hence H₁(a) is_limes_of phi by ORDINAL2:def 10; :: thesis: verum

end;

deffunc H₂( Ordinal, Ordinal) -> set = H₁($2);
deffunc H₃( Ordinal, Ordinal-Sequence) -> set = lim $2;
consider f being Ordinal-Sequence such that
A6: dom f = omega and
A7: ( 0 in omega implies f . 0 = succ e ) and
A8: for a being Ordinal st succ a in omega holds
f . (succ a) = H₂(a,f . a) and
for a being Ordinal st a in omega & a <> 0 & a is limit_ordinal holds
f . a = H₃(a,f | a) from ORDINAL2:sch 11();
A9: ( dom f = omega & f . 0 = succ e ) by A6, A7;
A10: for a being Ordinal st a in omega holds
f . (succ a) = H₁(f . a) by A8, ORDINAL1:28;
A11: ( succ e c= Union f & H₁( Union f) = Union f & ( for b being Ordinal st succ e c= b & H₁(b) = b holds
Union f c= b ) ) from ORDINAL5:sch 1(A1, A2, A9, A10);
Union f is epsilon by A11;
then reconsider e9 = Union f as epsilon Ordinal ;

A12: now :: thesis: ( e in e9 & ( for b being epsilon Ordinal st e in b holds
e9 c= b ) )

e in succ e by ORDINAL1:6;
hence e in e9 by A11; :: thesis: for b being epsilon Ordinal st e in b holds
e9 c= b
let b be epsilon Ordinal; :: thesis: ( e in b implies e9 c= b )
assume e in b ; :: thesis: e9 c= b
then ( succ e c= b & H₁(b) = b ) by Def5, ORDINAL1:21;
hence e9 c= b by A11; :: thesis: verum

end;

A13: ( succ 0 = 1 & succ 1 = 2 & succ 2 = 3 ) ;
then A14: f . 1 = H₁( succ e) by A7, A8
.= omega *^ H₁(e) by ORDINAL2:44
.= omega *^ e by Def5 ;
then A15: f . 2 = H₁(omega *^ e) by A13, A8
.= exp (H₁(e),omega) by ORDINAL4:31
.= exp (e,omega) by Def5 ;
then A16: f . 3 = H₁( exp (e,omega)) by A13, A8
.= exp (e,(exp (e,omega))) by Th38 ;
A17: ( e |^|^ 0 = 1 & e |^|^ 1 = e & e |^|^ 2 = exp (e,e) ) by Th13, Th16, Th18;
( omega in e & 1 in omega ) by Th37;
then A18: 1 in e by ORDINAL1:10;
then ( exp (e,1) in exp (e,e) & exp (e,1) in exp (e,omega) ) by ORDINAL4:24;
then A19: ( e in exp (e,e) & e in exp (e,omega) ) by ORDINAL2:46;
defpred S₁[ Nat] means ( e |^|^ $1 in f . ($1 + 1) & f . $1 in e |^|^ ($1 + 2) );
( e in exp (e,e) & exp (e,e) is limit_ordinal ) by A17, A18, Th24, Th9, ORDINAL3:8;
then A20: S₁[ 0 ] by A7, A14, A17, ORDINAL1:28, ORDINAL3:32;
A21: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A22: S₁[n] ; :: thesis: S₁[n + 1]
A23: ( Segm (n + 1) = succ (Segm n) & Segm ((n + 1) + 1) = succ (Segm (n + 1)) & n in omega & n + 1 in omega ) by NAT_1:38, ORDINAL1:def 12;
then A24: ( f . (n + 1) = H₁(f . n) & f . ((n + 1) + 1) = H₁(f . (n + 1)) ) by A10;
thus e |^|^ (n + 1) in f . ((n + 1) + 1) :: thesis: f . (n + 1) in e |^|^ ((n + 1) + 2)

proof

per cases ( n = 0 or n = 1 or n >= 2 ) by NAT_1:23;

suppose n = 0 ; :: thesis: e |^|^ (n + 1) in f . ((n + 1) + 1)

hence e |^|^ (n + 1) in f . ((n + 1) + 1) by A15, Th16, A19; :: thesis: verum

end;

suppose n = 1 ; :: thesis: e |^|^ (n + 1) in f . ((n + 1) + 1)

hence e |^|^ (n + 1) in f . ((n + 1) + 1) by A16, A17, A18, A19, ORDINAL4:24; :: thesis: verum

end;

suppose n >= 2 ; :: thesis: e |^|^ (n + 1) in f . ((n + 1) + 1)

then consider k being Nat such that
A25: n = 2 + k by NAT_1:10;
( 0 in Segm (k + 1) & k + 2 = (k + 1) + 1 ) by NAT_1:44;
then H₁(e |^|^ (k + 2)) = e |^|^ ((k + 1) + 2) by Th39;
hence e |^|^ (n + 1) in f . ((n + 1) + 1) by A24, A25, A22, ORDINAL4:24; :: thesis: verum

end;

end;

end;

( 0 in Segm (n + 1) & n + 2 = (n + 1) + 1 ) by NAT_1:44;
then H₁(e |^|^ (n + 2)) = e |^|^ ((n + 1) + 2) by Th39;
then H₁(f . n) in e |^|^ ((n + 1) + 2) by A22, ORDINAL4:24;
hence f . (n + 1) in e |^|^ ((n + 1) + 2) by A23, A10; :: thesis: verum

end;

A26: for n being Nat holds S₁[n] from NAT_1:sch 2(A20, A21);
deffunc H₄( Ordinal) -> Ordinal = e |^|^ $1;
consider g being Ordinal-Sequence such that
A27: ( dom g = omega & ( for a being Ordinal st a in omega holds
g . a = H₄(a) ) ) from ORDINAL2:sch 3();
A28: e |^|^ omega = lim g by A27, Th15;
( 1 in omega & omega in e ) by Th37;
then 1 in e by ORDINAL1:10;
then g is increasing Ordinal-Sequence by A27, Th25;
then Union g is_limes_of g by A27, Th6;
then A29: e |^|^ omega = Union g by A28, ORDINAL2:def 10;
e9 = Union g

proof

thus e9 c= Union g :: according to XBOOLE_0:def 10 :: thesis: not Union g c/= e9

proof

let x be Ordinal; :: according to ORDINAL1:def 5 :: thesis: ( not x in e9 or x in Union g )
assume x in e9 ; :: thesis: x in Union g
then consider a being object such that
A30: ( a in dom f & x in f . a ) by CARD_5:2;
reconsider a = a as Element of omega by A6, A30;
( f . a in e |^|^ (a + 2) & g . (a + 2) = H₄(a + 2) ) by A26, A27;
then f . a in Union g by A27, CARD_5:2;
hence x in Union g by A30, ORDINAL1:10; :: thesis: verum

end;

let x be Ordinal; :: according to ORDINAL1:def 5 :: thesis: ( not x in Union g or x in e9 )
assume x in Union g ; :: thesis: x in e9
then consider a being object such that
A31: ( a in dom g & x in g . a ) by CARD_5:2;
reconsider a = a as Element of omega by A27, A31;
( a + 1 in omega & e |^|^ a in f . (a + 1) & g . a = H₄(a) ) by A26, A27;
then g . a in Union f by A6, CARD_5:2;
hence x in e9 by A31, ORDINAL1:10; :: thesis: verum

end;

hence first_epsilon_greater_than e = e |^|^ omega by A12, A29, Def6; :: thesis: verum