let X be set ; ex A being Ordinal st Tarski-Class (X,A) = Tarski-Class (X,(succ A))
assume A1:
for A being Ordinal holds Tarski-Class (X,A) <> Tarski-Class (X,(succ A))
; contradiction
defpred S1[ object ] means ex A being Ordinal st $1 in Tarski-Class (X,A);
consider Z being set such that
A2:
for x being object holds
( x in Z 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 & $1 in Tarski-Class (X,(succ A)) & not $1 in Tarski-Class (X,A) );
A3:
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 A being
Ordinal such that A4:
y = A
and A5:
x in Tarski-Class (
X,
(succ A))
and A6:
not
x in Tarski-Class (
X,
A)
;
( not S2[x,z] or y = z )
given B being
Ordinal such that A7:
z = B
and A8:
x in Tarski-Class (
X,
(succ B))
and A9:
not
x in Tarski-Class (
X,
B)
;
y = z
assume A10:
y <> z
;
contradiction
(
A c= B or
B c= A )
;
then A11:
(
A c< B or
B c< A )
by A4, A7, A10;
then
succ B c= A
by ORDINAL1:11, ORDINAL1:21, A11;
then
Tarski-Class (
X,
(succ B))
c= Tarski-Class (
X,
A)
by Th16;
hence
contradiction
by A6, A8;
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 Z & S2[y,x] ) )
from TARSKI:sch 1(A3);
now for A being Ordinal holds A in Ylet A be
Ordinal;
A in YA13:
Tarski-Class (
X,
A)
c= Tarski-Class (
X,
(succ A))
by Th15;
consider x being
object such that A14:
( (
x in Tarski-Class (
X,
A) & not
x in Tarski-Class (
X,
(succ A)) ) or (
x in Tarski-Class (
X,
(succ A)) & not
x in Tarski-Class (
X,
A) ) )
by A1, TARSKI:2;
x in Z
by A2, A14;
hence
A in Y
by A12, A13, A14;
verum end;
hence
contradiction
by ORDINAL1:26; verum