begin
Lm1:
for X being set holds Tarski-Class X is Tarski
defpred S1[ Ordinal] means for W being set st W is Tarski & $1 in On W holds
( card (Rank $1) in card W & Rank $1 in W );
Lm2:
S1[ {} ]
by Th9, CARD_1:27, CLASSES1:29, ORDINAL1:def 9;
Lm3:
for A being Ordinal st S1[A] holds
S1[ succ A]
Lm4:
for A being Ordinal st A <> {} & A is limit_ordinal & ( for B being Ordinal st B in A holds
S1[B] ) holds
S1[A]
deffunc H1( set ) -> set = the_rank_of $1;
deffunc H2( set ) -> set = card (bool $1);
theorem
for
U1,
U2 being
Universe holds
(
U1 in U2 or
U1 = U2 or
U2 in U1 )
Lm5:
omega is limit_ordinal
by ORDINAL1:def 11;
deffunc H3( Ordinal, set ) -> set = Tarski-Class $2;
deffunc H4( Ordinal, T-Sequence) -> Universe = Universe_closure (Union $2);
deffunc H5( Ordinal) -> set = UNIVERSE $1;
Lm6:
now ( H5( {} ) = FinSETS & ( for A being Ordinal holds H5( succ A) = H3(A,H5(A)) ) & ( for A being Ordinal
for L being T-Sequence st A <> {} & A is limit_ordinal & dom L = A & ( for B being Ordinal st B in A holds
L . B = H5(B) ) holds
H5(A) = H4(A,L) ) )
A1:
for
A being
Ordinal for
x being
set holds
(
x = H5(
A) iff ex
L being
T-Sequence st
(
x = last L &
dom L = succ A &
L . {} = FinSETS & ( for
C being
Ordinal st
succ C in succ A holds
L . (succ C) = H3(
C,
L . C) ) & ( for
C being
Ordinal st
C in succ A &
C <> {} &
C is
limit_ordinal holds
L . C = H4(
C,
L | C) ) ) )
by Def5;
thus
H5(
{} )
= FinSETS
from ORDINAL2:sch 8(A1); ( ( for A being Ordinal holds H5( succ A) = H3(A,H5(A)) ) & ( for A being Ordinal
for L being T-Sequence st A <> {} & A is limit_ordinal & dom L = A & ( for B being Ordinal st B in A holds
L . B = H5(B) ) holds
H5(A) = H4(A,L) ) )thus
for
A being
Ordinal holds
H5(
succ A)
= H3(
A,
H5(
A))
from ORDINAL2:sch 9(A1); for A being Ordinal
for L being T-Sequence st A <> {} & A is limit_ordinal & dom L = A & ( for B being Ordinal st B in A holds
L . B = H5(B) ) holds
H5(A) = H4(A,L)let A be
Ordinal;
for L being T-Sequence st A <> {} & A is limit_ordinal & dom L = A & ( for B being Ordinal st B in A holds
L . B = H5(B) ) holds
H5(A) = H4(A,L)let L be
T-Sequence;
( A <> {} & A is limit_ordinal & dom L = A & ( for B being Ordinal st B in A holds
L . B = H5(B) ) implies H5(A) = H4(A,L) )assume that A2:
(
A <> {} &
A is
limit_ordinal )
and A3:
dom L = A
and A4:
for
B being
Ordinal st
B in A holds
L . B = H5(
B)
;
H5(A) = H4(A,L)thus
H5(
A)
= H4(
A,
L)
from ORDINAL2:sch 10(A1, A2, A3, A4); verum
end;
Lm7:
1 = succ 0
;