let a be Ordinal; ex A being Cantor-normal-form Ordinal-Sequence st a = Sum^ A
defpred S1[ Ordinal] means ( 0 in $1 implies ex A being non empty Cantor-normal-form Ordinal-Sequence st $1 = Sum^ A );
A1:
for a being Ordinal st ( for b being Ordinal st b in a holds
S1[b] ) holds
S1[a]
proof
let a be
Ordinal;
( ( for b being Ordinal st b in a holds
S1[b] ) implies S1[a] )
assume that A2:
for
b being
Ordinal st
b in a holds
S1[
b]
and A3:
0 in a
;
ex A being non empty Cantor-normal-form Ordinal-Sequence st a = Sum^ A
consider n being
Nat,
b being
Ordinal such that A4:
(
a = (n *^ (exp (omega,(omega -exponent a)))) +^ b &
0 in Segm n &
b in exp (
omega,
(omega -exponent a)) )
by A3, Th62;
reconsider s =
n *^ (exp (omega,(omega -exponent a))) as
Cantor-component Ordinal by A4, Def9;
set c =
omega -exponent a;
A5:
exp (
omega,
(omega -exponent a))
c= a
by A3, Def10;
per cases
( b = 0 or 0 in b )
by ORDINAL3:8;
suppose
0 in b
;
ex A being non empty Cantor-normal-form Ordinal-Sequence st a = Sum^ Athen consider A being non
empty Cantor-normal-form Ordinal-Sequence such that A7:
b = Sum^ A
by A5, A2, A4;
A8:
A . 0 in exp (
omega,
(omega -exponent a))
by A4, A7, Th56, ORDINAL1:12;
0 in dom A
by ORDINAL3:8;
then
A . 0 is
Cantor-component Ordinal
by Def11;
then
0 in A . 0
by ORDINAL3:8;
then
exp (
omega,
(omega -exponent (A . 0)))
c= A . 0
by Def10;
then A9:
exp (
omega,
(omega -exponent (A . 0)))
in exp (
omega,
(omega -exponent a))
by A8, ORDINAL1:12;
n in omega
by ORDINAL1:def 12;
then
omega -exponent s = omega -exponent a
by A4, Th58;
then reconsider B =
<%s%> ^ A as non
empty Cantor-normal-form Ordinal-Sequence by A9, Th68, Th12;
take
B
;
a = Sum^ Bthus
a = Sum^ B
by A4, A7, Th55;
verum end; end;
end;
A10:
for b being Ordinal holds S1[b]
from ORDINAL1:sch 2(A1);