let X be set ; :: thesis: card (SmallestPartition X) = card X
set A = SmallestPartition X;
per cases ( X = {} or X <> {} ) ;
suppose X = {} ; :: thesis: card (SmallestPartition X) = card X
hence card (SmallestPartition X) = card X ; :: thesis: verum
end;
suppose X <> {} ; :: thesis: card (SmallestPartition X) = card X
then reconsider X = X as non empty set ;
deffunc H1( object ) -> set = {$1};
A1: SmallestPartition X = { {x} where x is Element of X : verum } by EQREL_1:37;
then A2: for a being object st a in X holds
H1(a) in SmallestPartition X ;
consider f being Function of X,(SmallestPartition X) such that
A3: for a being object st a in X holds
f . a = H1(a) from FUNCT_2:sch 2(A2);
A4: rng f = SmallestPartition X
proof
thus rng f c= SmallestPartition X ; :: according to XBOOLE_0:def 10 :: thesis: SmallestPartition X c= rng f
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in SmallestPartition X or a in rng f )
assume a in SmallestPartition X ; :: thesis: a in rng f
then consider b being Element of X such that
A5: a = {b} by A1;
f . b = a by A3, A5;
hence a in rng f by FUNCT_2:4; :: thesis: verum
end;
A6: f is one-to-one
proof
let a, b be object ; :: according to FUNCT_1:def 4 :: thesis: ( not a in proj1 f or not b in proj1 f or not f . a = f . b or a = b )
assume that
A7: a in dom f and
A8: b in dom f ; :: thesis: ( not f . a = f . b or a = b )
assume f . a = f . b ; :: thesis: a = b
then {a} = f . b by A3, A7
.= {b} by A3, A8 ;
hence a = b by ZFMISC_1:3; :: thesis: verum
end;
dom f = X by FUNCT_2:def 1;
then X, SmallestPartition X are_equipotent by A4, A6, WELLORD2:def 4;
hence card (SmallestPartition X) = card X by CARD_1:5; :: thesis: verum
end;
end;