let X, x, y be set ; ( ( x in Tarski-Class X implies {x} in Tarski-Class X ) & ( x in Tarski-Class X & y in Tarski-Class X implies {x,y} in Tarski-Class X ) )
assume that
A1:
x in Tarski-Class X
and
A2:
y in Tarski-Class X
; {x,y} in Tarski-Class X
A3:
{x} in Tarski-Class X
by Z1, A1;
bool {x} = {{},{x}}
by ZFMISC_1:24;
then A4:
not {{},{x}}, Tarski-Class X are_equipotent
by A3, Th4, Th25;
now ( x <> y implies {x,y} in Tarski-Class X )assume A5:
x <> y
;
{x,y} in Tarski-Class X
{{},{x}},
{x,y} are_equipotent
proof
defpred S1[
object ]
means $1
= {} ;
deffunc H1(
object )
-> set =
x;
deffunc H2(
object )
-> set =
y;
consider f being
Function such that A6:
(
dom f = {{},{x}} & ( for
z being
object st
z in {{},{x}} holds
( (
S1[
z] implies
f . z = H1(
z) ) & ( not
S1[
z] implies
f . z = H2(
z) ) ) ) )
from PARTFUN1:sch 1();
take
f
;
WELLORD2:def 4 ( f is one-to-one & dom f = {{},{x}} & rng f = {x,y} )
thus
f is
one-to-one
( dom f = {{},{x}} & rng f = {x,y} )proof
let x1,
x2 be
object ;
FUNCT_1:def 4 ( not x1 in dom f or not x2 in dom f or not f . x1 = f . x2 or x1 = x2 )
assume that A7:
x1 in dom f
and A8:
x2 in dom f
;
( not f . x1 = f . x2 or x1 = x2 )
A9:
(
x2 = {} or
x2 = {x} )
by A6, A8, TARSKI:def 2;
A10:
(
x1 = {} implies
f . x1 = x )
by A6, A7;
(
x1 <> {} implies
f . x1 = y )
by A6, A7;
hence
( not
f . x1 = f . x2 or
x1 = x2 )
by A5, A6, A7, A8, A9, A10, TARSKI:def 2;
verum
end;
thus
dom f = {{},{x}}
by A6;
rng f = {x,y}
thus
rng f c= {x,y}
XBOOLE_0:def 10 {x,y} c= rng f
let z be
object ;
TARSKI:def 3 ( not z in {x,y} or z in rng f )
assume
z in {x,y}
;
z in rng f
then A11:
(
z = x or
z = y )
by TARSKI:def 2;
A12:
{} in dom f
by A6, TARSKI:def 2;
A13:
{x} in dom f
by A6, TARSKI:def 2;
A14:
f . {} = x
by A6, A12;
f . {x} = y
by A6, A13;
hence
z in rng f
by A11, A12, A13, A14, FUNCT_1:def 3;
verum
end; then A15:
not
{x,y},
Tarski-Class X are_equipotent
by A4, WELLORD2:15;
{x,y} c= Tarski-Class X
by A1, A2, ZFMISC_1:32;
hence
{x,y} in Tarski-Class X
by A15, Th5;
verum end;
hence
{x,y} in Tarski-Class X
by A3, ENUMSET1:29; verum