let A, C be Ordinal; ( C <> {} implies exp (C,A) <> {} )
defpred S1[ Ordinal] means exp (C,$1) <> {} ;
assume A1:
C <> {}
; exp (C,A) <> {}
A2:
for A being Ordinal st S1[A] holds
S1[ succ A]
A4:
for A being Ordinal st A <> 0 & A is limit_ordinal & ( for B being Ordinal st B in A holds
S1[B] ) holds
S1[A]
proof
let A be
Ordinal;
( A <> 0 & A is limit_ordinal & ( for B being Ordinal st B in A holds
S1[B] ) implies S1[A] )
assume that A5:
A <> 0
and A6:
A is
limit_ordinal
and A7:
for
B being
Ordinal st
B in A holds
exp (
C,
B)
<> {}
;
S1[A]
consider fi being
Ordinal-Sequence such that A8:
dom fi = A
and A9:
for
B being
Ordinal st
B in A holds
fi . B = exp (
C,
B)
and A10:
ex
D being
Ordinal st
D is_limes_of fi
by A5, A6, Lm8;
A11:
exp (
C,
A)
= lim fi
by A5, A6, A8, A9, ORDINAL2:45;
assume A12:
exp (
C,
A)
= {}
;
contradiction
consider D being
Ordinal such that A13:
D is_limes_of fi
by A10;
lim fi = D
by A13, ORDINAL2:def 10;
then consider B being
Ordinal such that A14:
B in dom fi
and A15:
for
D being
Ordinal st
B c= D &
D in dom fi holds
fi . D = {}
by A11, A13, A12, ORDINAL2:def 9;
fi . B = exp (
C,
B)
by A8, A9, A14;
hence
contradiction
by A7, A8, A14, A15;
verum
end;
A16:
S1[ 0 ]
by ORDINAL2:43;
for A being Ordinal holds S1[A]
from ORDINAL2:sch 1(A16, A2, A4);
hence
exp (C,A) <> {}
; verum