let X be set ; ( X is epsilon-transitive implies ex A being Ordinal st Tarski-Class X c= Rank A )
assume A1:
X is epsilon-transitive
; ex A being Ordinal st Tarski-Class X c= Rank A
assume A2:
for A being Ordinal holds not Tarski-Class X c= Rank A
; contradiction
defpred S1[ object ] means ex A being Ordinal st $1 in Rank A;
consider Power being set such that
A3:
for x being object holds
( x in Power iff ( x in Tarski-Class X & S1[x] ) )
from XBOOLE_0:sch 1();
defpred S2[ object , object ] means ex A being Ordinal st
( $2 = A & not $1 in Rank A & $1 in Rank (succ A) );
A4:
for x, y, z being object st S2[x,y] & S2[x,z] holds
y = z
proof
let x,
y,
z be
object ;
( S2[x,y] & S2[x,z] implies y = z )
given A1 being
Ordinal such that A5:
y = A1
and A6:
not
x in Rank A1
and A7:
x in Rank (succ A1)
;
( not S2[x,z] or y = z )
given A2 being
Ordinal such that A8:
z = A2
and A9:
not
x in Rank A2
and A10:
x in Rank (succ A2)
;
y = z
assume
y <> z
;
contradiction
then A11:
(
A1 in A2 or
A2 in A1 )
by A5, A8, ORDINAL1:14;
then
Rank (succ A2) c= Rank A1
by A11, Th37, ORDINAL1:21;
hence
contradiction
by A6, A10;
verum
end;
consider Y being set such that
A12:
for x being object holds
( x in Y iff ex y being object st
( y in Power & S2[y,x] ) )
from TARSKI:sch 1(A4);
now for A being Ordinal holds A in Ylet A be
Ordinal;
A in Y
(Rank A) /\ (Tarski-Class X) <> (Rank (succ A)) /\ (Tarski-Class X)
by A1, A2, Th46;
then consider y being
object such that A13:
( (
y in (Rank A) /\ (Tarski-Class X) & not
y in (Rank (succ A)) /\ (Tarski-Class X) ) or (
y in (Rank (succ A)) /\ (Tarski-Class X) & not
y in (Rank A) /\ (Tarski-Class X) ) )
by TARSKI:2;
A14:
A c= succ A
by ORDINAL1:6, ORDINAL1:def 2;
then A15:
Rank A c= Rank (succ A)
by Th37;
(Rank A) /\ (Tarski-Class X) c= (Rank (succ A)) /\ (Tarski-Class X)
by XBOOLE_1:26, A14, Th37;
then A16:
y in Rank (succ A)
by A13, XBOOLE_0:def 4;
A17:
y in Tarski-Class X
by A13, XBOOLE_0:def 4;
then A18:
not
y in Rank A
by A13, A15, XBOOLE_0:def 4;
y in Power
by A3, A16, A17;
hence
A in Y
by A12, A16, A18;
verum end;
hence
contradiction
by ORDINAL1:26; verum