let A, B, C be Ordinal; :: thesis: ( 1 in C & A in B implies exp (C,A) in exp (C,B) )

defpred S_{1}[ Ordinal] means for A being Ordinal st A in $1 holds

exp (C,A) in exp (C,$1);

A1: for B being Ordinal st B <> 0 & B is limit_ordinal & ( for D being Ordinal st D in B holds

S_{1}[D] ) holds

S_{1}[B]

A13: for B being Ordinal st S_{1}[B] holds

S_{1}[ succ B]
_{1}[ 0 ]
;

for B being Ordinal holds S_{1}[B]
from ORDINAL2:sch 1(A17, A13, A1);

hence ( not A in B or exp (C,A) in exp (C,B) ) ; :: thesis: verum

defpred S

exp (C,A) in exp (C,$1);

A1: for B being Ordinal st B <> 0 & B is limit_ordinal & ( for D being Ordinal st D in B holds

S

S

proof

assume A12:
1 in C
; :: thesis: ( not A in B or exp (C,A) in exp (C,B) )
deffunc H_{1}( Ordinal) -> set = exp (C,$1);

let B be Ordinal; :: thesis: ( B <> 0 & B is limit_ordinal & ( for D being Ordinal st D in B holds

S_{1}[D] ) implies S_{1}[B] )

assume that

A2: B <> 0 and

A3: B is limit_ordinal and

A4: for D being Ordinal st D in B holds

S_{1}[D]
; :: thesis: S_{1}[B]

consider fi being Ordinal-Sequence such that

A5: ( dom fi = B & ( for D being Ordinal st D in B holds

fi . D = H_{1}(D) ) )
from ORDINAL2:sch 3();

fi is increasing

let A be Ordinal; :: thesis: ( A in B implies exp (C,A) in exp (C,B) )

assume A10: A in B ; :: thesis: exp (C,A) in exp (C,B)

fi . A = exp (C,A) by A10, A5;

then A11: exp (C,A) in rng fi by A10, A5, FUNCT_1:def 3;

exp (C,B) = lim fi by A2, A3, A5, ORDINAL2:45;

hence exp (C,A) in exp (C,B) by A9, A11, ORDINAL2:19; :: thesis: verum

end;let B be Ordinal; :: thesis: ( B <> 0 & B is limit_ordinal & ( for D being Ordinal st D in B holds

S

assume that

A2: B <> 0 and

A3: B is limit_ordinal and

A4: for D being Ordinal st D in B holds

S

consider fi being Ordinal-Sequence such that

A5: ( dom fi = B & ( for D being Ordinal st D in B holds

fi . D = H

fi is increasing

proof

then A9:
sup fi = lim fi
by A2, A3, A5, Th8;
let B1, B2 be Ordinal; :: according to ORDINAL2:def 12 :: thesis: ( not B1 in B2 or not B2 in dom fi or fi . B1 in fi . B2 )

assume that

A6: B1 in B2 and

A7: B2 in dom fi ; :: thesis: fi . B1 in fi . B2

A8: fi . B1 = exp (C,B1) by A5, A6, A7, ORDINAL1:10;

exp (C,B1) in exp (C,B2) by A4, A5, A6, A7;

hence fi . B1 in fi . B2 by A5, A7, A8; :: thesis: verum

end;assume that

A6: B1 in B2 and

A7: B2 in dom fi ; :: thesis: fi . B1 in fi . B2

A8: fi . B1 = exp (C,B1) by A5, A6, A7, ORDINAL1:10;

exp (C,B1) in exp (C,B2) by A4, A5, A6, A7;

hence fi . B1 in fi . B2 by A5, A7, A8; :: thesis: verum

let A be Ordinal; :: thesis: ( A in B implies exp (C,A) in exp (C,B) )

assume A10: A in B ; :: thesis: exp (C,A) in exp (C,B)

fi . A = exp (C,A) by A10, A5;

then A11: exp (C,A) in rng fi by A10, A5, FUNCT_1:def 3;

exp (C,B) = lim fi by A2, A3, A5, ORDINAL2:45;

hence exp (C,A) in exp (C,B) by A9, A11, ORDINAL2:19; :: thesis: verum

A13: for B being Ordinal st S

S

proof

A17:
S
let B be Ordinal; :: thesis: ( S_{1}[B] implies S_{1}[ succ B] )

assume A14: for A being Ordinal st A in B holds

exp (C,A) in exp (C,B) ; :: thesis: S_{1}[ succ B]

let A be Ordinal; :: thesis: ( A in succ B implies exp (C,A) in exp (C,(succ B)) )

assume A in succ B ; :: thesis: exp (C,A) in exp (C,(succ B))

then A15: A c= B by ORDINAL1:22;

hence exp (C,A) in exp (C,(succ B)) by A16, ORDINAL1:10; :: thesis: verum

end;assume A14: for A being Ordinal st A in B holds

exp (C,A) in exp (C,B) ; :: thesis: S

let A be Ordinal; :: thesis: ( A in succ B implies exp (C,A) in exp (C,(succ B)) )

assume A in succ B ; :: thesis: exp (C,A) in exp (C,(succ B))

then A15: A c= B by ORDINAL1:22;

A16: now :: thesis: ( A <> B implies exp (C,A) in exp (C,B) )

exp (C,B) in exp (C,(succ B))
by A12, Th23;assume
A <> B
; :: thesis: exp (C,A) in exp (C,B)

then A c< B by A15;

hence exp (C,A) in exp (C,B) by A14, ORDINAL1:11; :: thesis: verum

end;then A c< B by A15;

hence exp (C,A) in exp (C,B) by A14, ORDINAL1:11; :: thesis: verum

hence exp (C,A) in exp (C,(succ B)) by A16, ORDINAL1:10; :: thesis: verum

for B being Ordinal holds S

hence ( not A in B or exp (C,A) in exp (C,B) ) ; :: thesis: verum