let X be set ; :: thesis: card (singletons X) = card X
defpred S₁[ object , object ] means ( $1 in X & $2 = {$1} );
A1: for x being object st x in X holds
ex y being object st S₁[x,y] ;
consider f being Function such that
A2: dom f = X and
A3: for x being object st x in X holds
S₁[x,f . x] from CLASSES1:sch 1(A1);
A4: rng f = singletons X

proof

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

proof

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;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in singletons X or y in 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;

f is one-to-one

proof

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₁[x1,f . x1] & S₁[x2,f . x2] ) by A2, A3, A10;
hence x1 = x2 by A11, ZFMISC_1:3; :: thesis: verum

end;

then X, singletons X are_equipotent by A2, A4, WELLORD2:def 4;
hence card (singletons X) = card X by CARD_1:5; :: thesis: verum