let A be infinite set ; :: thesis: not A in Tarski-Class {A}
deffunc H₁( set , set ) -> set = $2 \/ (bool $2);
consider f being Function such that
A1: ( dom f = NAT & f . 0 = {{A},{}} ) and
A2: for n being Nat holds f . (n + 1) = H₁(n,f . n) from NAT_1:sch 11();
set U = Union f;
( f . (0 + 1) = (f . 0) \/ (bool (f . 0)) & {} c= {{A},{}} ) by A2;
then A3: {} in f . 1 by A1, XBOOLE_0:def 3;
then A4: {} in Union f by A1, CARD_5:2;
defpred S₁[ object , object ] means ( $1 in f . $2 & $2 in dom f & ( for i, j being Nat st i < j & j = $2 holds
not $1 in f . i ) );
A5: for x being object st x in Union f holds
ex y being object st S₁[x,y]

proof

let x be object ; :: thesis: ( x in Union f implies ex y being object st S₁[x,y] )
assume A6: x in Union f ; :: thesis: ex y being object st S₁[x,y]
consider k being object such that
A7: ( k in dom f & x in f . k ) by A6, CARD_5:2;
reconsider k = k as Nat by A7, A1;
defpred S₂[ Nat] means x in f . $1;
S₂[k] by A7;
then A8: ex k being Nat st S₂[k] ;
consider k being Nat such that
A9: S₂[k] and
A10: for n being Nat st S₂[n] holds
k <= n from NAT_1:sch 5(A8);
take k ; :: thesis: S₁[x,k]
thus S₁[x,k] by A10, A9, A1, ORDINAL1:def 12; :: thesis: verum

end;

consider Min being Function such that
A11: ( dom Min = Union f & ( for x being object st x in Union f holds
S₁[x,Min . x] ) ) from CLASSES1:sch 1(A5);
A12: Union f is subset-closed

proof

let X be set ; :: according to CLASSES1:def 1 :: thesis: for b₁ being set holds
( not X in Union f or not b₁ c= X or b₁ in Union f )
let Y be set ; :: thesis: ( not X in Union f or not Y c= X or Y in Union f )
assume A13: ( X in Union f & Y c= X ) ; :: thesis: Y in Union f
set x = Min . X;
A14: S₁[X,Min . X] by A11, A13;
then reconsider x = Min . X as Nat by A1;

per cases ( X = Y or ( x = 0 & X <> Y ) or x > 0 ) by NAT_1:3;

suppose X = Y ; :: thesis: Y in Union f

hence Y in Union f by A13; :: thesis: verum

end;

suppose ( x = 0 & X <> Y ) ; :: thesis: Y in Union f

then ( X = {A} or X = {} ) by A1, TARSKI:def 2, A14;
hence Y in Union f by A4, A13, ZFMISC_1:33; :: thesis: verum

end;

suppose x > 0 ; :: thesis: Y in Union f

then reconsider x1 = x - 1 as Element of NAT by NAT_1:20;
x1 < x1 + 1 by NAT_1:13;
then A15: not X in f . x1 by A11, A13;
A16: f . (x1 + 1) = (f . x1) \/ (bool (f . x1)) by A2;
then X in bool (f . x1) by A14, A15, XBOOLE_0:def 3;
then X c= f . x1 ;
then Y c= f . x1 by A13;
then Y in f . x by A16, XBOOLE_0:def 3;
hence Y in Union f by A14, CARD_5:2; :: thesis: verum

end;

end;

end;

A17: for X being set st X in Union f holds
bool X in Union f

proof

let X be set ; :: thesis: ( X in Union f implies bool X in Union f )
assume A18: X in Union f ; :: thesis: bool X in Union f
set x = Min . X;
A19: S₁[X,Min . X] by A11, A18;
reconsider x = Min . X as Nat by A19, A1;
A20: f . (x + 1) = (f . x) \/ (bool (f . x)) by A2;

per cases ( x = 0 or x > 0 ) by NAT_1:3;

suppose A21: x = 0 ; :: thesis: bool X in Union f

then ( X = {A} or X = {} ) by A1, TARSKI:def 2, A19;
then bool X c= {{A},{}} by ZFMISC_1:7, ZFMISC_1:24, ZFMISC_1:1;
then bool X in f . 1 by A20, A21, A1, XBOOLE_0:def 3;
hence bool X in Union f by A1, CARD_5:2; :: thesis: verum

end;

suppose x > 0 ; :: thesis: bool X in Union f

then reconsider x1 = x - 1 as Element of NAT by NAT_1:20;
x1 < x1 + 1 by NAT_1:13;
then A22: not X in f . x1 by A11, A18;
A23: f . (x1 + 1) = (f . x1) \/ (bool (f . x1)) by A2;
A24: f . (x + 1) = (f . x) \/ (bool (f . x)) by A2;
X in bool (f . x1) by A23, A19, A22, XBOOLE_0:def 3;
then bool X c= bool (f . x1) by ZFMISC_1:67;
then bool X c= f . x by A23, XBOOLE_1:10;
then bool X in f . (x + 1) by A24, XBOOLE_0:def 3;
hence bool X in Union f by A1, CARD_5:2; :: thesis: verum

end;

end;

end;

defpred S₂[ Nat] means f . $1 is finite ;
A25: S₂[ 0 ] by A1;
A26: for n being Nat st S₂[n] holds
S₂[n + 1]

proof

let n be Nat; :: thesis: ( S₂[n] implies S₂[n + 1] )
assume A27: S₂[n] ; :: thesis: S₂[n + 1]
f . (n + 1) = (f . n) \/ (bool (f . n)) by A2;
hence S₂[n + 1] by A27; :: thesis: verum

end;

A28: for n being Nat holds S₂[n] from NAT_1:sch 2(A25, A26);
A29: for x being set st x in dom f holds
f . x is countable

proof

let x be set ; :: thesis: ( x in dom f implies f . x is countable )
assume A30: x in dom f ; :: thesis: f . x is countable
reconsider x = x as Nat by A30, A1;
S₂[x] by A28;
hence f . x is countable ; :: thesis: verum

end;

then A31: Union f is countable by CARD_4:11, A1;
for X being set holds
( not X c= Union f or X, Union f are_equipotent or X in Union f )

proof

let X be set ; :: thesis: ( not X c= Union f or X, Union f are_equipotent or X in Union f )
assume A32: X c= Union f ; :: thesis: ( X, Union f are_equipotent or X in Union f )

per cases ( card X = omega or X = {} or ( card X <> omega & X <> {} ) ) ;

suppose ( card X = omega or X = {} ) ; :: thesis: ( X, Union f are_equipotent or X in Union f )

then ( card (Union f) = card X or X = {} ) by A32, CARD_1:11, CARD_3:def 14, A29, CARD_4:11, A1;
hence ( X, Union f are_equipotent or X in Union f ) by A3, A1, CARD_5:2, CARD_1:5; :: thesis: verum

end;

suppose A33: ( card X <> omega & X <> {} ) ; :: thesis: ( X, Union f are_equipotent or X in Union f )

then card X c< omega by A32, CARD_3:def 14, A31;
then card X in omega by ORDINAL1:11;
then A34: X is finite ;
defpred S₃[ object , object ] means ( $1 in f . $2 & $2 in dom f );
A35: for x being object st x in X holds
ex u being object st S₃[x,u]

proof

let x be object ; :: thesis: ( x in X implies ex u being object st S₃[x,u] )
assume x in X ; :: thesis: ex u being object st S₃[x,u]
then ex n being object st
( n in dom f & x in f . n ) by A32, CARD_5:2;
hence ex u being object st S₃[x,u] ; :: thesis: verum

end;

consider fX being Function such that
A36: dom fX = X and
A37: for x being object st x in X holds
S₃[x,fX . x] from CLASSES1:sch 1(A35);

A38: now :: thesis: for y being object st y in rng fX holds
y is natural

let y be object ; :: thesis: ( y in rng fX implies y is natural )
assume y in rng fX ; :: thesis: y is natural
then ex x being object st
( x in dom fX & fX . x = y ) by FUNCT_1:def 3;
hence y is natural by A1, A37, A36; :: thesis: verum

end;

reconsider RNG = rng fX as non empty finite natural-membered set by A33, RELAT_1:42, A38, MEMBERED:def 6, A36, A34, FINSET_1:8;
set m = max RNG;
max RNG in omega by ORDINAL1:def 12;
then reconsider m = max RNG as Nat ;
A39: ( f . (m + 1) = (f . m) \/ (bool (f . m)) & m + 1 in omega ) by A2;
X c= f . m

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in f . m )
assume A40: x in X ; :: thesis: x in f . m
S₃[x,fX . x] by A40, A37;
then reconsider k = fX . x as Nat by A1;
k in rng fX by A40, A36, FUNCT_1:def 3;
then A41: k <= m by XXREAL_2:def 8;
defpred S₄[ Nat] means x in f . $1;
A42: S₄[k] by A40, A37;
A43: for i being Nat st k <= i & S₄[i] holds
S₄[i + 1]

proof

let i be Nat; :: thesis: ( k <= i & S₄[i] implies S₄[i + 1] )
assume A44: ( k <= i & S₄[i] ) ; :: thesis: S₄[i + 1]
f . (i + 1) = (f . i) \/ (bool (f . i)) by A2;
hence S₄[i + 1] by A44, XBOOLE_0:def 3; :: thesis: verum

end;

for i being Nat st k <= i holds
S₄[i] from NAT_1:sch 8(A42, A43);
hence x in f . m by A41; :: thesis: verum

end;

then X in f . (m + 1) by A39, XBOOLE_0:def 3;
hence ( X, Union f are_equipotent or X in Union f ) by A1, CARD_5:2; :: thesis: verum

end;

end;

end;

then A45: Union f is Tarski by A12, A17;
( {A} in f . 0 & 0 in omega ) by A1, TARSKI:def 2;
then Union f is_Tarski-Class_of {A} by A45, CARD_5:2, A1;
then A46: Tarski-Class {A} c= Union f by CLASSES1:def 4;
not A in Union f

proof

assume A48: A in Union f ; :: thesis: contradiction
then A49: S₁[A,Min . A] by A11;
then reconsider x = Min . A as Nat by A1;

per cases ( x = 0 or x > 0 ) by NAT_1:3;

suppose x = 0 ; :: thesis: contradiction

hence contradiction by A1, A49; :: thesis: verum

end;

suppose x > 0 ; :: thesis: contradiction

then reconsider x1 = x - 1 as Element of NAT by NAT_1:20;
x1 < x1 + 1 by NAT_1:13;
then A50: not A in f . x1 by A48, A11;
A51: f . (x1 + 1) = (f . x1) \/ (bool (f . x1)) by A2;
A in bool (f . x1) by A51, A49, A50, XBOOLE_0:def 3;
then ( A c= f . x1 & f . x1 is finite ) by A28;
hence contradiction ; :: thesis: verum

end;

end;

end;

hence not A in Tarski-Class {A} by A46; :: thesis: verum