let A be infinite set ; :: thesis: not A in Tarski-Class {A}
deffunc H1( 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) = H1(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 ;
then A4: {} in Union f by ;
defpred S1[ 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 S1[x,y]
proof
let x be object ; :: thesis: ( x in Union f implies ex y being object st S1[x,y] )
assume A6: x in Union f ; :: thesis: ex y being object st S1[x,y]
consider k being object such that
A7: ( k in dom f & x in f . k ) by ;
reconsider k = k as Nat by A7, A1;
defpred S2[ Nat] means x in f . \$1;
S2[k] by A7;
then A8: ex k being Nat st S2[k] ;
consider k being Nat such that
A9: S2[k] and
A10: for n being Nat st S2[n] holds
k <= n from take k ; :: thesis: S1[x,k]
thus S1[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
S1[x,Min . x] ) ) from A12: Union f is subset-closed
proof
let X be set ; :: according to CLASSES1:def 1 :: thesis: for b1 being set holds
( not X in Union f or not b1 c= X or b1 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: S1[X,Min . X] by ;
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 = 0 & X <> Y ) ; :: thesis: Y in Union f
then ( X = {A} or X = {} ) by ;
hence Y in Union f by ; :: 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 ;
A16: f . (x1 + 1) = (f . x1) \/ (bool (f . x1)) by A2;
then X in bool (f . x1) by ;
then X c= f . x1 ;
then Y c= f . x1 by A13;
then Y in f . x by ;
hence Y in Union f by ; :: 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:
set x = Min . X;
A19: S1[X,Min . X] by ;
reconsider x = Min . X as Nat by ;
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:
then ( X = {A} or X = {} ) by ;
then bool X c= {{A},{}} by ;
then bool X in f . 1 by ;
hence bool X in Union f by ; :: thesis: verum
end;
suppose x > 0 ; :: thesis:
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 ;
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 ;
then bool X c= bool (f . x1) by ZFMISC_1:67;
then bool X c= f . x by ;
then bool X in f . (x + 1) by ;
hence bool X in Union f by ; :: thesis: verum
end;
end;
end;
defpred S2[ Nat] means f . \$1 is finite ;
A25: S2[ 0 ] by A1;
A26: for n being Nat st S2[n] holds
S2[n + 1]
proof
let n be Nat; :: thesis: ( S2[n] implies S2[n + 1] )
assume A27: S2[n] ; :: thesis: S2[n + 1]
f . (n + 1) = (f . n) \/ (bool (f . n)) by A2;
hence S2[n + 1] by A27; :: thesis: verum
end;
A28: for n being Nat holds S2[n] from 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 ;
S2[x] by A28;
hence f . x is countable ; :: thesis: verum
end;
then A31: Union f is countable by ;
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 () = card X or X = {} ) by ;
hence ( X, Union f are_equipotent or X in Union f ) by ; :: 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 ;
then card X in omega by ORDINAL1:11;
then A34: X is finite ;
defpred S3[ 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 S3[x,u]
proof
let x be object ; :: thesis: ( x in X implies ex u being object st S3[x,u] )
assume x in X ; :: thesis: ex u being object st S3[x,u]
then ex n being object st
( n in dom f & x in f . n ) by ;
hence ex u being object st S3[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
S3[x,fX . x] from
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 ;
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
S3[x,fX . x] by ;
then reconsider k = fX . x as Nat by A1;
k in rng fX by ;
then A41: k <= m by XXREAL_2:def 8;
defpred S4[ Nat] means x in f . \$1;
A42: S4[k] by A40, A37;
A43: for i being Nat st k <= i & S4[i] holds
S4[i + 1]
proof
let i be Nat; :: thesis: ( k <= i & S4[i] implies S4[i + 1] )
assume A44: ( k <= i & S4[i] ) ; :: thesis: S4[i + 1]
f . (i + 1) = (f . i) \/ (bool (f . i)) by A2;
hence S4[i + 1] by ; :: thesis: verum
end;
for i being Nat st k <= i holds
S4[i] from hence x in f . m by A41; :: thesis: verum
end;
then X in f . (m + 1) by ;
hence ( X, Union f are_equipotent or X in Union f ) by ; :: thesis: verum
end;
end;
end;
then A45: Union f is Tarski by ;
( {A} in f . 0 & 0 in omega ) by ;
then Union f is_Tarski-Class_of {A} by ;
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: S1[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
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 ;
A51: f . (x1 + 1) = (f . x1) \/ (bool (f . x1)) by A2;
A in bool (f . x1) by ;
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