let X be set ; :: thesis: card (singletons X) = card X

defpred S_{1}[ object , object ] means ( $1 in X & $2 = {$1} );

A1: for x being object st x in X holds

ex y being object st S_{1}[x,y]
;

consider f being Function such that

A2: dom f = X and

A3: for x being object st x in X holds

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

A4: rng f = singletons X

hence card (singletons X) = card X by CARD_1:5; :: thesis: verum

defpred S

A1: for x being object st x in X holds

ex y being object st S

consider f being Function such that

A2: dom f = X and

A3: for x being object st x in X holds

S

A4: rng f = singletons X

proof

f is one-to-one
thus
rng f c= singletons X
:: according to XBOOLE_0:def 10 :: thesis: singletons X c= rng f

assume A8: y in singletons X ; :: thesis: y in rng f

reconsider X = X as non empty set by A8;

ex z being Subset of X st

( y = z & z is 1 -element ) by A8;

then reconsider y = y as 1 -element Subset of X ;

consider x being Element of X such that

A9: y = {x} by CARD_1:65;

y = f . x by A3, A9;

hence y in rng f by A2, FUNCT_1:3; :: thesis: verum

end;proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in singletons X or y in rng f )
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in singletons X )

assume y in rng f ; :: thesis: y in singletons X

then consider x being object such that

A5: x in dom f and

A6: y = f . x by FUNCT_1:def 3;

A7: f . x = {x} by A2, A3, A5;

then reconsider fx = f . x as Subset of X by A2, A5, ZFMISC_1:31;

fx is 1 -element by A7;

hence y in singletons X by A6; :: thesis: verum

end;assume y in rng f ; :: thesis: y in singletons X

then consider x being object such that

A5: x in dom f and

A6: y = f . x by FUNCT_1:def 3;

A7: f . x = {x} by A2, A3, A5;

then reconsider fx = f . x as Subset of X by A2, A5, ZFMISC_1:31;

fx is 1 -element by A7;

hence y in singletons X by A6; :: thesis: verum

assume A8: y in singletons X ; :: thesis: y in rng f

reconsider X = X as non empty set by A8;

ex z being Subset of X st

( y = z & z is 1 -element ) by A8;

then reconsider y = y as 1 -element Subset of X ;

consider x being Element of X such that

A9: y = {x} by CARD_1:65;

y = f . x by A3, A9;

hence y in rng f by A2, FUNCT_1:3; :: thesis: verum

proof

then
X, singletons X are_equipotent
by A2, A4, WELLORD2:def 4;
let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom f or not x2 in dom f or not f . x1 = f . x2 or x1 = x2 )

assume that

A10: ( x1 in dom f & x2 in dom f ) and

A11: f . x1 = f . x2 ; :: thesis: x1 = x2

( S_{1}[x1,f . x1] & S_{1}[x2,f . x2] )
by A2, A3, A10;

hence x1 = x2 by A11, ZFMISC_1:3; :: thesis: verum

end;assume that

A10: ( x1 in dom f & x2 in dom f ) and

A11: f . x1 = f . x2 ; :: thesis: x1 = x2

( S

hence x1 = x2 by A11, ZFMISC_1:3; :: thesis: verum

hence card (singletons X) = card X by CARD_1:5; :: thesis: verum