let X be set ; :: thesis: card (singletons X) = card X
defpred S₁[ set , set ] means ( $1 in X & $2 = {$1} );
A1: for x being set st x in X holds
ex y being set st S₁[x,y] ;
consider f being Function such that
A2: dom f = X and
A3: for x being set 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 set ; :: 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 set such that
A5: x in dom f and
A6: y = f . x by FUNCT_1:def 5;
A7: f . x = {x} by A2, A3, A5;
then reconsider fx = f . x as Subset of X by A2, A5, ZFMISC_1:37;
fx is Singleton by A7;
hence y in singletons X by A6; :: thesis: verum

end;

let y be set ; :: 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
A9: ex z being Subset of X st
( y = z & z is Singleton ) by A8;
reconsider y = y as Subset of X by A8;
consider x being set such that
A10: x in X and
A11: y = {x} by A9, Def9;
reconsider x = x as Element of X by A10;
y = f . x by A3, A10, A11;
hence y in rng f by A2, A10, FUNCT_1:12; :: thesis: verum

end;

f is one-to-one

proof

let x1, x2 be set ; :: according to FUNCT_1:def 8 :: thesis: ( not x1 in proj1 f or not x2 in proj1 f or not f . x1 = f . x2 or x1 = x2 )
assume that
A12: ( x1 in dom f & x2 in dom f ) and
A13: f . x1 = f . x2 ; :: thesis: x1 = x2
( S₁[x1,f . x1] & S₁[x2,f . x2] ) by A2, A3, A12;
hence x1 = x2 by A13, ZFMISC_1:6; :: thesis: verum

end;

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