let A be Ordinal; :: thesis: ( A <> {} implies exp ({},A) = {} )

defpred S_{1}[ Ordinal] means ( $1 <> {} implies exp ({},$1) = {} );

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

S_{1}[ succ B]

S_{1}[C] ) holds

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

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

hence ( A <> {} implies exp ({},A) = {} ) ; :: thesis: verum

defpred S

A1: for B being Ordinal st S

S

proof

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

assume that

S_{1}[B]
and

succ B <> {} ; :: thesis: exp ({},(succ B)) = {}

thus exp ({},(succ B)) = {} *^ (exp ({},B)) by ORDINAL2:44

.= {} by ORDINAL2:35 ; :: thesis: verum

end;assume that

S

succ B <> {} ; :: thesis: exp ({},(succ B)) = {}

thus exp ({},(succ B)) = {} *^ (exp ({},B)) by ORDINAL2:44

.= {} by ORDINAL2:35 ; :: thesis: verum

S

S

proof

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

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

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

assume that

A3: A <> 0 and

A4: A is limit_ordinal and

A5: for C being Ordinal st C in A holds

S_{1}[C]
and

A <> {} ; :: thesis: exp ({},A) = {}

consider fi being Ordinal-Sequence such that

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

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

0 is_limes_of fi

hence exp ({},A) = {} by A3, A4, A6, ORDINAL2:45; :: thesis: verum

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

S

assume that

A3: A <> 0 and

A4: A is limit_ordinal and

A5: for C being Ordinal st C in A holds

S

A <> {} ; :: thesis: exp ({},A) = {}

consider fi being Ordinal-Sequence such that

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

fi . B = H

0 is_limes_of fi

proof
end;

then
lim fi = {}
by ORDINAL2:def 10;per cases
( 0 = 0 or 0 <> 0 )
;

:: according to ORDINAL2:def 9end;

:: according to ORDINAL2:def 9

case
0 = 0
; :: thesis: ex b_{1} being set st

( b_{1} in dom fi & ( for b_{2} being set holds

( not b_{1} c= b_{2} or not b_{2} in dom fi or fi . b_{2} = 0 ) ) )

( b

( not b

take B = 1; :: thesis: ( B in dom fi & ( for b_{1} being set holds

( not B c= b_{1} or not b_{1} in dom fi or fi . b_{1} = 0 ) ) )

{} in A by A3, ORDINAL3:8;

hence B in dom fi by A4, A6, Lm3, ORDINAL1:28; :: thesis: for b_{1} being set holds

( not B c= b_{1} or not b_{1} in dom fi or fi . b_{1} = 0 )

let D be Ordinal; :: thesis: ( not B c= D or not D in dom fi or fi . D = 0 )

assume A7: B c= D ; :: thesis: ( not D in dom fi or fi . D = 0 )

assume A8: D in dom fi ; :: thesis: fi . D = 0

then S_{1}[D]
by A5, A6;

hence fi . D = 0 by A6, A7, A8, Lm3, ORDINAL1:21; :: thesis: verum

end;( not B c= b

{} in A by A3, ORDINAL3:8;

hence B in dom fi by A4, A6, Lm3, ORDINAL1:28; :: thesis: for b

( not B c= b

let D be Ordinal; :: thesis: ( not B c= D or not D in dom fi or fi . D = 0 )

assume A7: B c= D ; :: thesis: ( not D in dom fi or fi . D = 0 )

assume A8: D in dom fi ; :: thesis: fi . D = 0

then S

hence fi . D = 0 by A6, A7, A8, Lm3, ORDINAL1:21; :: thesis: verum

case
0 <> 0
; :: thesis: for b_{1}, b_{2} being set holds

( not b_{1} in 0 or not 0 in b_{2} or ex b_{3} being set st

( b_{3} in dom fi & ( for b_{4} being set holds

( not b_{3} c= b_{4} or not b_{4} in dom fi or ( b_{1} in fi . b_{4} & fi . b_{4} in b_{2} ) ) ) ) )

( not b

( b

( not b

thus
for b_{1}, b_{2} being set holds

( not b_{1} in 0 or not 0 in b_{2} or ex b_{3} being set st

( b_{3} in dom fi & ( for b_{4} being set holds

( not b_{3} c= b_{4} or not b_{4} in dom fi or ( b_{1} in fi . b_{4} & fi . b_{4} in b_{2} ) ) ) ) )
; :: thesis: verum

end;( not b

( b

( not b

hence exp ({},A) = {} by A3, A4, A6, ORDINAL2:45; :: thesis: verum

for B being Ordinal holds S

hence ( A <> {} implies exp ({},A) = {} ) ; :: thesis: verum