let X be set ; :: thesis: card () = card X
defpred S1[ object , object ] means ( \$1 in X & \$2 = {\$1} );
A1: for x being object st x in X holds
ex y being object st S1[x,y] ;
consider f being Function such that
A2: dom f = X and
A3: for x being object st x in X holds
S1[x,f . x] from A4: rng f = singletons X
proof
thus rng f c= singletons X :: according to XBOOLE_0:def 10 :: thesis:
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:
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 ;
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 ; :: 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
( S1[x1,f . x1] & S1[x2,f . x2] ) by A2, A3, A10;
hence x1 = x2 by ; :: thesis: verum
end;
then X, singletons X are_equipotent by ;
hence card () = card X by CARD_1:5; :: thesis: verum