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 number st a in b holds
H₁(a) in H₁(b) by ORDINAL4:24;

A2: now

let a be ordinal number ; :: thesis: ( not a is empty & a is limit_ordinal implies for phi being Ordinal-Sequence st dom phi = a & ( for b being ordinal number st b in a holds
phi . b = H₁(b) ) holds
H₁(a) is_limes_of phi )
assume B1: ( not a is empty & a is limit_ordinal ) ; :: thesis: for phi being Ordinal-Sequence st dom phi = a & ( for b being ordinal number 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 number st b in a holds
phi . b = H₁(b) ) implies H₁(a) is_limes_of phi )
assume B2: ( dom phi = a & ( for b being ordinal number 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 number ; :: according to ORDINAL5:def 2 :: thesis: for b being ordinal number st b in b & b in dom phi holds
phi . b c= phi . b
let c be ordinal number ; :: thesis: ( b in c & c in dom phi implies phi . b c= phi . c )
assume B3: ( b in c & c in dom phi ) ; :: thesis: phi . b c= phi . c
then ( phi . b = H₁(b) & phi . c = H₁(c) ) by B2, ORDINAL1:19;
then phi . b in phi . c by B3, 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 B1, B2, ThND, ORDINAL2:62;
hence H₁(a) is_limes_of phi by ORDINAL2:def 14; :: 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
A4: dom f = omega and
A5: ( {} in omega implies f . {} = succ e ) and
A6: for a being ordinal number st succ a in omega holds
f . (succ a) = H₂(a,f . a) and
for a being ordinal number st a in omega & a <> {} & a is limit_ordinal holds
f . a = H₃(a,f | a) from ORDINAL2:sch 11();
F1: ( dom f = omega & f . 0 = succ e ) by A4, A5;

F2: now

let a be ordinal number ; :: thesis: ( a in omega implies f . (succ a) = H₁(f . a) )
assume a in omega ; :: thesis: f . (succ a) = H₁(f . a)
then succ a in omega by ORDINAL1:41;
hence f . (succ a) = H₁(f . a) by A6; :: thesis: verum

end;

A7: ( succ e c= Union f & H₁( Union f) = Union f & ( for b being ordinal number st succ e c= b & H₁(b) = b holds
Union f c= b ) ) from ORDINAL5:sch 1(A1, A2, F1, F2);
Union f is epsilon

proof

thus H₁( Union f) = Union f by A7; :: according to ORDINAL5:def 5 :: thesis: verum

end;

then reconsider e9 = Union f as epsilon Ordinal ;

now

e in succ e by ORDINAL1:10;
hence e in e9 by A7; :: 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 EPSILON, ORDINAL1:33;
hence e9 c= b by A7; :: thesis: verum

end;

then A3: e9 = first_epsilon_greater_than e by FEGT;
H0: ( succ 0 = 1 & succ 1 = 2 & succ 2 = 3 ) ;
then H1: f . 1 = H₁( succ e) by F1, A6
.= omega *^ H₁(e) by ORDINAL2:61
.= omega *^ e by EPSILON ;
then H2: f . 2 = H₁(omega *^ e) by H0, A6
.= exp H₁(e),omega by ORDINAL4:31
.= exp e,omega by EPSILON ;
then H3: f . 3 = H₁( exp e,omega ) by H0, A6
.= exp e,(exp e,omega ) by Th22 ;
H4: ( e |^|^ 0 = 1 & e |^|^ 1 = e & e |^|^ 2 = exp e,e ) by Th0, Th3, Th39;
( omega in e & 1 in omega ) by Th21;
then H5: 1 in e by ORDINAL1:19;
then ( exp e,1 in exp e,e & exp e,1 in exp e,omega ) by ORDINAL4:24;
then H6: ( e in exp e,e & e in exp e,omega ) by ORDINAL2:63;
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 H4, H5, Th7, Th002, ORDINAL3:10;
then I1: S₁[ 0 ] by F1, H1, H4, ORDINAL1:41, ORDINAL3:35;
I2: for n being natural number st S₁[n] holds
S₁[n + 1]

proof

let n be natural number ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume I3: S₁[n] ; :: thesis: S₁[n + 1]
I4: ( n + 1 = succ n & (n + 1) + 1 = succ (n + 1) & n in omega & n + 1 in omega ) by NAT_1:39, ORDINAL1:def 13;
then I5: ( f . (n + 1) = H₁(f . n) & f . ((n + 1) + 1) = H₁(f . (n + 1)) ) by F2;
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 H2, H4, H6; :: 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 H3, H4, H5, H6, ORDINAL4:24; :: thesis: verum

end;

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

then consider k being Nat such that
J1: n = 2 + k by NAT_1:10;
( 0 in k + 1 & k + 2 = (k + 1) + 1 ) by NAT_1:45;
then H₁(e |^|^ (k + 2)) = e |^|^ ((k + 1) + 2) by Th23;
hence e |^|^ (n + 1) in f . ((n + 1) + 1) by I5, J1, I3, ORDINAL4:24; :: thesis: verum

end;

end;

end;

( 0 in n + 1 & n + 2 = (n + 1) + 1 ) by NAT_1:45;
then H₁(e |^|^ (n + 2)) = e |^|^ ((n + 1) + 2) by Th23;
then H₁(f . n) in e |^|^ ((n + 1) + 2) by I3, ORDINAL4:24;
hence f . (n + 1) in e |^|^ ((n + 1) + 2) by I4, F2; :: thesis: verum

end;

A8: for n being natural number holds S₁[n] from NAT_1:sch 2(I1, I2);
deffunc H₄( Ordinal) -> Ordinal = e |^|^ $1;
consider g being Ordinal-Sequence such that
G0: ( dom g = omega & ( for a being ordinal number st a in omega holds
g . a = H₄(a) ) ) from ORDINAL2:sch 3();
A9: e |^|^ omega = lim g by G0, Th2;
( 1 in omega & omega in e ) by Th21;
then 1 in e by ORDINAL1:19;
then g is increasing Ordinal-Sequence by G0, Th8;
then Union g is_limes_of g by G0, ThND;
then AA: e |^|^ omega = Union g by A9, ORDINAL2:def 14;
e9 = Union g

proof

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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in e9 or x in Union g )
assume x in e9 ; :: thesis: x in Union g
then consider a being set such that
C1: ( a in dom f & x in f . a ) by CARD_5:10;
reconsider a = a as Element of omega by A4, C1;
( f . a in e |^|^ (a + 2) & g . (a + 2) = H₄(a + 2) ) by A8, G0;
then f . a in Union g by G0, CARD_5:10;
hence x in Union g by C1, ORDINAL1:19; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Union g or x in e9 )
assume x in Union g ; :: thesis: x in e9
then consider a being set such that
C1: ( a in dom g & x in g . a ) by CARD_5:10;
reconsider a = a as Element of omega by G0, C1;
( a + 1 in omega & e |^|^ a in f . (a + 1) & g . a = H₄(a) ) by A8, G0;
then g . a in Union f by A4, CARD_5:10;
hence x in e9 by C1, ORDINAL1:19; :: thesis: verum

end;

hence first_epsilon_greater_than e = e |^|^ omega by A3, AA; :: thesis: verum