let A be infinite set ; :: thesis: not A in Tarski-Class {A}

deffunc H_{1}( 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_{1}(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_{1}[ 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_{1}[x,y]

A11: ( dom Min = Union f & ( for x being object st x in Union f holds

S_{1}[x,Min . x] ) )
from CLASSES1:sch 1(A5);

A12: Union f is subset-closed

bool X in Union f_{2}[ Nat] means f . $1 is finite ;

A25: S_{2}[ 0 ]
by A1;

A26: for n being Nat st S_{2}[n] holds

S_{2}[n + 1]
_{2}[n]
from NAT_1:sch 2(A25, A26);

A29: for x being set st x in dom f holds

f . x is countable

for X being set holds

( not X c= Union f or X, Union f are_equipotent or X in Union f )

( {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

deffunc H

consider f being Function such that

A1: ( dom f = NAT & f . 0 = {{A},{}} ) and

A2: for n being Nat holds f . (n + 1) = H

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

not $1 in f . i ) );

A5: for x being object st x in Union f holds

ex y being object st S

proof

consider Min being Function such that
let x be object ; :: thesis: ( x in Union f implies ex y being object st S_{1}[x,y] )

assume A6: x in Union f ; :: thesis: ex y being object st S_{1}[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_{2}[ Nat] means x in f . $1;

S_{2}[k]
by A7;

then A8: ex k being Nat st S_{2}[k]
;

consider k being Nat such that

A9: S_{2}[k]
and

A10: for n being Nat st S_{2}[n] holds

k <= n from NAT_1:sch 5(A8);

take k ; :: thesis: S_{1}[x,k]

thus S_{1}[x,k]
by A10, A9, A1, ORDINAL1:def 12; :: thesis: verum

end;assume A6: x in Union f ; :: thesis: ex y being object st S

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

S

then A8: ex k being Nat st S

consider k being Nat such that

A9: S

A10: for n being Nat st S

k <= n from NAT_1:sch 5(A8);

take k ; :: thesis: S

thus S

A11: ( dom Min = Union f & ( for x being object st x in Union f holds

S

A12: Union f is subset-closed

proof

A17:
for X being set st X in Union f holds
let X be set ; :: according to CLASSES1:def 1 :: thesis: for b_{1} being set holds

( not X in Union f or not b_{1} c= X or b_{1} 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_{1}[X,Min . X]
by A11, A13;

then reconsider x = Min . X as Nat by A1;

end;( not X in Union f or not b

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

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;

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;hence Y in Union f by A4, A13, ZFMISC_1:33; :: thesis: verum

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;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

bool X in Union f

proof

defpred S
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_{1}[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;

end;assume A18: X in Union f ; :: thesis: bool X in Union f

set x = Min . X;

A19: S

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;

end;

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;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

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;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

A25: S

A26: for n being Nat st S

S

proof

A28:
for n being Nat holds S
let n be Nat; :: thesis: ( S_{2}[n] implies S_{2}[n + 1] )

assume A27: S_{2}[n]
; :: thesis: S_{2}[n + 1]

f . (n + 1) = (f . n) \/ (bool (f . n)) by A2;

hence S_{2}[n + 1]
by A27; :: thesis: verum

end;assume A27: S

f . (n + 1) = (f . n) \/ (bool (f . n)) by A2;

hence S

A29: for x being set st x in dom f holds

f . x is countable

proof

then A31:
Union f is countable
by CARD_4:11, A1;
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_{2}[x]
by A28;

hence f . x is countable ; :: thesis: verum

end;assume A30: x in dom f ; :: thesis: f . x is countable

reconsider x = x as Nat by A30, A1;

S

hence f . x is countable ; :: thesis: verum

for X being set holds

( not X c= Union f or X, Union f are_equipotent or X in Union f )

proof

then A45:
Union f is Tarski
by A12, A17;
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 )

end;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 <> {} ) )
;

end;

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;hence ( X, Union f are_equipotent or X in Union f ) by A3, A1, CARD_5:2, CARD_1:5; :: thesis: verum

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_{3}[ 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_{3}[x,u]

A36: dom fX = X and

A37: for x being object st x in X holds

S_{3}[x,fX . x]
from CLASSES1:sch 1(A35);

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

hence ( X, Union f are_equipotent or X in Union f ) by A1, CARD_5:2; :: thesis: verum

end;then card X in omega by ORDINAL1:11;

then A34: X is finite ;

defpred S

A35: for x being object st x in X holds

ex u being object st S

proof

consider fX being Function such that
let x be object ; :: thesis: ( x in X implies ex u being object st S_{3}[x,u] )

assume x in X ; :: thesis: ex u being object st S_{3}[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_{3}[x,u]
; :: thesis: verum

end;assume x in X ; :: thesis: ex u being object st S

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

A36: dom fX = X and

A37: for x being object st x in X holds

S

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

y is natural

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;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;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

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

then
X in f . (m + 1)
by A39, XBOOLE_0:def 3;
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_{3}[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_{4}[ Nat] means x in f . $1;

A42: S_{4}[k]
by A40, A37;

A43: for i being Nat st k <= i & S_{4}[i] holds

S_{4}[i + 1]

S_{4}[i]
from NAT_1:sch 8(A42, A43);

hence x in f . m by A41; :: thesis: verum

end;assume A40: x in X ; :: thesis: x in f . m

S

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

A42: S

A43: for i being Nat st k <= i & S

S

proof

for i being Nat st k <= i holds
let i be Nat; :: thesis: ( k <= i & S_{4}[i] implies S_{4}[i + 1] )

assume A44: ( k <= i & S_{4}[i] )
; :: thesis: S_{4}[i + 1]

f . (i + 1) = (f . i) \/ (bool (f . i)) by A2;

hence S_{4}[i + 1]
by A44, XBOOLE_0:def 3; :: thesis: verum

end;assume A44: ( k <= i & S

f . (i + 1) = (f . i) \/ (bool (f . i)) by A2;

hence S

S

hence x in f . m by A41; :: thesis: verum

hence ( X, Union f are_equipotent or X in Union f ) by A1, CARD_5:2; :: thesis: verum

( {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

hence
not A in Tarski-Class {A}
by A46; :: thesis: verum
assume A48:
A in Union f
; :: thesis: contradiction

then A49: S_{1}[A,Min . A]
by A11;

then reconsider x = Min . A as Nat by A1;

end;then A49: S

then reconsider x = Min . A as Nat by A1;

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

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;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