let A, C be Ordinal; :: thesis: ( 1 in C implies A c= exp (C,A) )

defpred S_{1}[ Ordinal] means $1 c= exp (C,$1);

assume A1: 1 in C ; :: thesis: A c= exp (C,A)

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

S_{1}[ succ B]

S_{1}[B] ) holds

S_{1}[A]
_{1}[ 0 ]
by XBOOLE_1:2;

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

hence A c= exp (C,A) ; :: thesis: verum

defpred S

assume A1: 1 in C ; :: thesis: A c= exp (C,A)

A2: for B being Ordinal st S

S

proof

A5:
for A being Ordinal st A <> 0 & A is limit_ordinal & ( for B being Ordinal st B in A holds
let B be Ordinal; :: thesis: ( S_{1}[B] implies S_{1}[ succ B] )

assume A3: B c= exp (C,B) ; :: thesis: S_{1}[ succ B]

A4: exp (C,B) = 1 *^ (exp (C,B)) by ORDINAL2:39;

exp (C,(succ B)) = C *^ (exp (C,B)) by ORDINAL2:44;

then exp (C,B) in exp (C,(succ B)) by A1, A4, Th22, ORDINAL2:40;

then B in exp (C,(succ B)) by A3, ORDINAL1:12;

hence S_{1}[ succ B]
by ORDINAL1:21; :: thesis: verum

end;assume A3: B c= exp (C,B) ; :: thesis: S

A4: exp (C,B) = 1 *^ (exp (C,B)) by ORDINAL2:39;

exp (C,(succ B)) = C *^ (exp (C,B)) by ORDINAL2:44;

then exp (C,B) in exp (C,(succ B)) by A1, A4, Th22, ORDINAL2:40;

then B in exp (C,(succ B)) by A3, ORDINAL1:12;

hence S

S

S

proof

A13:
S
deffunc H_{1}( Ordinal) -> set = exp (C,$1);

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

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

assume that

A6: A <> 0 and

A7: A is limit_ordinal and

A8: for B being Ordinal st B in A holds

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

consider fi being Ordinal-Sequence such that

A9: ( dom fi = A & ( for B being Ordinal st B in A holds

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

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in exp (C,A) )

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

then reconsider B = x as Ordinal ;

fi . B = exp (C,B) by A9, A10;

then exp (C,B) in rng fi by A9, A10, FUNCT_1:def 3;

then A11: exp (C,B) in sup fi by ORDINAL2:19;

fi is increasing by A1, A9, Th25;

then A12: sup fi = lim fi by A6, A7, A9, Th8

.= exp (C,A) by A6, A7, A9, ORDINAL2:45 ;

B c= exp (C,B) by A8, A10;

hence x in exp (C,A) by A12, A11, ORDINAL1:12; :: thesis: verum

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

S

assume that

A6: A <> 0 and

A7: A is limit_ordinal and

A8: for B being Ordinal st B in A holds

B c= exp (C,B) ; :: thesis: S

consider fi being Ordinal-Sequence such that

A9: ( dom fi = A & ( for B being Ordinal st B in A holds

fi . B = H

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in exp (C,A) )

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

then reconsider B = x as Ordinal ;

fi . B = exp (C,B) by A9, A10;

then exp (C,B) in rng fi by A9, A10, FUNCT_1:def 3;

then A11: exp (C,B) in sup fi by ORDINAL2:19;

fi is increasing by A1, A9, Th25;

then A12: sup fi = lim fi by A6, A7, A9, Th8

.= exp (C,A) by A6, A7, A9, ORDINAL2:45 ;

B c= exp (C,B) by A8, A10;

hence x in exp (C,A) by A12, A11, ORDINAL1:12; :: thesis: verum

for B being Ordinal holds S

hence A c= exp (C,A) ; :: thesis: verum