let A be non empty set ; for O being Ordinal holds A c= ConsecutiveSet2 (A,O)
let O be Ordinal; A c= ConsecutiveSet2 (A,O)
defpred S1[ Ordinal] means A c= ConsecutiveSet2 (A,$1);
A1:
for O1 being Ordinal st S1[O1] holds
S1[ succ O1]
A3:
for O1 being Ordinal st O1 <> 0 & O1 is limit_ordinal & ( for O2 being Ordinal st O2 in O1 holds
S1[O2] ) holds
S1[O1]
proof
deffunc H1(
Ordinal)
-> set =
ConsecutiveSet2 (
A,$1);
let O2 be
Ordinal;
( O2 <> 0 & O2 is limit_ordinal & ( for O2 being Ordinal st O2 in O2 holds
S1[O2] ) implies S1[O2] )
assume that A4:
O2 <> 0
and A5:
O2 is
limit_ordinal
and
for
O1 being
Ordinal st
O1 in O2 holds
A c= ConsecutiveSet2 (
A,
O1)
;
S1[O2]
A6:
{} in O2
by A4, ORDINAL3:8;
consider Ls being
Sequence such that A7:
(
dom Ls = O2 & ( for
O1 being
Ordinal st
O1 in O2 holds
Ls . O1 = H1(
O1) ) )
from ORDINAL2:sch 2();
Ls . {} =
ConsecutiveSet2 (
A,
{})
by A4, A7, ORDINAL3:8
.=
A
by Th14
;
then A8:
A in rng Ls
by A7, A6, FUNCT_1:def 3;
ConsecutiveSet2 (
A,
O2)
= union (rng Ls)
by A4, A5, A7, Th16;
hence
S1[
O2]
by A8, ZFMISC_1:74;
verum
end;
A9:
S1[ 0 ]
by Th14;
for O being Ordinal holds S1[O]
from ORDINAL2:sch 1(A9, A1, A3);
hence
A c= ConsecutiveSet2 (A,O)
; verum