per cases ( ( a = 0 & b = 0 ) or ( a = 0 & b <> 0 ) or 0 in a ) by ORDINAL3:8;
suppose ( a = 0 & b = 0 ) ; :: thesis: exp (a,b) is Ordinal of U
then exp (a,b) = 1-element_of U by ORDINAL2:43;
hence exp (a,b) is Ordinal of U ; :: thesis: verum
end;
suppose ( a = 0 & b <> 0 ) ; :: thesis: exp (a,b) is Ordinal of U
hence exp (a,b) is Ordinal of U ; :: thesis: verum
end;
suppose A1: 0 in a ; :: thesis: exp (a,b) is Ordinal of U
defpred S1[ Ordinal] means ( $1 in U implies exp (a,$1) in U );
exp (a,0) = succ 0 by ORDINAL2:43;
then A2: S1[ 0 ] by CLASSES2:5;
A3: for b being Ordinal st S1[b] holds
S1[ succ b]
proof
let b be Ordinal; :: thesis: ( S1[b] implies S1[ succ b] )
assume that
A4: S1[b] and
A5: succ b in U ; :: thesis: exp (a,(succ b)) in U
b in succ b by ORDINAL1:6;
then reconsider b = b as Ordinal of U by A5, ORDINAL1:10;
reconsider ab = exp (a,b) as Ordinal of U by A4;
exp (a,(succ b)) = a *^ ab by ORDINAL2:44;
hence exp (a,(succ b)) in U ; :: thesis: verum
end;
A6: 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
A7: ( b <> 0 & b is limit_ordinal ) and
A8: for c being Ordinal st c in b holds
S1[c] and
A9: b in U ; :: thesis: exp (a,b) in U
deffunc H1( Ordinal) -> set = exp (a,$1);
consider f being Ordinal-Sequence such that
A10: ( dom f = b & ( for c being Ordinal st c in b holds
f . c = H1(c) ) ) from ORDINAL2:sch 3();
 rng f c= On U
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in On U )
assume x in rng f ; :: thesis: x in On U
then consider y being object such that
A11: ( y in b & x = f . y ) by A10, FUNCT_1:def 3;
reconsider y = y as Ordinal by A11;
( S1[y] & y in U & x = H1(y) ) by A9, A8, A10, A11, ORDINAL1:10;
hence x in On U by ORDINAL1:def 9; :: thesis: verum
end;
then reconsider f = f as Ordinal-Sequence of b,U by A10, FUNCT_2:2;
A12: exp (a,b) = lim f by A7, A10, ORDINAL2:45;
f is non-decreasing by A1, A10, ORDINAL5:8;
then Union f is_limes_of f by A7, ORDINAL5:6;
then exp (a,b) = Union f by A12, ORDINAL2:def 10;
hence exp (a,b) in U by A9, Th41; :: thesis: verum
end;
for b being Ordinal holds S1[b] from ORDINAL2:sch 1(A2, A3, A6);
hence exp (a,b) is Ordinal of U ; :: thesis: verum
end;
end;