let a, b be Ordinal; :: thesis: ( a is limit_ordinal & 0 in b implies exp (a,b) is limit_ordinal )
assume A1: ( a is limit_ordinal & 0 in b ) ; :: thesis: exp (a,b) is limit_ordinal
per cases ( a = 0 or 0 in a ) by ORDINAL3:8;
suppose a = 0 ; :: thesis: exp (a,b) is limit_ordinal
hence exp (a,b) is limit_ordinal by A1, ORDINAL4:20; :: thesis: verum
end;
suppose A2: 0 in a ; :: thesis: exp (a,b) is limit_ordinal
defpred S1[ Ordinal] means ( 0 in $1 implies exp (a,$1) is limit_ordinal );
A3: S1[ 0 ] ;
A4: for c being Ordinal st S1[c] holds
S1[ succ c]
proof
let c be Ordinal; :: thesis: ( S1[c] implies S1[ succ c] )
exp (a,(succ c)) = a *^ (exp (a,c)) by ORDINAL2:44;
hence ( S1[c] implies S1[ succ c] ) by A1, ORDINAL3:40; :: thesis: verum
end;
A5: for c being Ordinal st c <> 0 & c is limit_ordinal & ( for b being Ordinal st b in c holds
S1[b] ) holds
S1[c]
proof
let c be Ordinal; :: thesis: ( c <> 0 & c is limit_ordinal & ( for b being Ordinal st b in c holds
S1[b] ) implies S1[c] )
assume that
A6: ( c <> 0 & c is limit_ordinal ) and
A7: for b being Ordinal st b in c holds
S1[b] ; :: thesis: S1[c]
deffunc H1( Ordinal) -> set = exp (a,$1);
consider f being Ordinal-Sequence such that
A8: ( dom f = c & ( for b being Ordinal st b in c holds
f . b = H1(b) ) ) from ORDINAL2:sch 3();
 A9: exp (a,c) = lim f by A6, A8, ORDINAL2:45;
f is non-decreasing by A2, A8, Th8;
then Union f is_limes_of f by A6, A8, Th6;
then A10: exp (a,c) = Union f by A9, ORDINAL2:def 10;
for d being Ordinal st d in exp (a,c) holds
succ d in exp (a,c)
proof
let d be Ordinal; :: thesis: ( d in exp (a,c) implies succ d in exp (a,c) )
assume d in exp (a,c) ; :: thesis: succ d in exp (a,c)
then consider b being object such that
A11: ( b in dom f & d in f . b ) by A10, CARD_5:2;
reconsider b = b as Ordinal by A11;
A12: succ b in dom f by A6, A8, A11, ORDINAL1:28;
then A13: ( f . b = H1(b) & f . (succ b) = H1( succ b) & S1[ succ b] ) by A7, A8, A11;
H1(b) c= H1( succ b) by A2, ORDINAL3:1, ORDINAL4:27;
then succ d in f . (succ b) by A13, A11, ORDINAL1:28, ORDINAL3:8;
hence succ d in exp (a,c) by A10, A12, CARD_5:2; :: thesis: verum
end;
hence S1[c] by ORDINAL1:28; :: thesis: verum
end;
for c being Ordinal holds S1[c] from ORDINAL2:sch 1(A3, A4, A5);
hence exp (a,b) is limit_ordinal by A1; :: thesis: verum
end;
end;