let X be finite set ; :: thesis: for n being Nat holds card { Y where Y is Subset of X : card Y = n } = (card X) choose n
let n be Nat; :: thesis: card { Y where Y is Subset of X : card Y = n } = (card X) choose n
reconsider N = n as Element of NAT by ORDINAL1:def 12;
set YY = { Y where Y is Subset of X : card Y = n } ;
set CH = Choose (X,N,1,0);
deffunc H1( set ) -> set = (X --> 0) +* ($1 --> 1);
consider f being Function such that
A1: ( dom f = { Y where Y is Subset of X : card Y = n } & ( for x being set st x in { Y where Y is Subset of X : card Y = n } holds
f . x = H1(x) ) ) from FUNCT_1:sch 5();
 A2: Choose (X,N,1,0) c= rng f
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Choose (X,N,1,0) or y in rng f )
A3: dom (X --> 0) = X ;
assume y in Choose (X,N,1,0) ; :: thesis: y in rng f
then consider g being Function of X,{0,1} such that
A4: g = y and
A5: card (g " {1}) = n by CARD_FIN:def 1;
X = dom g by FUNCT_2:def 1;
then reconsider Y = g " {1} as Subset of X by RELAT_1:132;
A6: Y in { Y where Y is Subset of X : card Y = n } by A5;
A7: now :: thesis: for x being object st x in dom g holds
g . x = H1(Y) . x
let x be object ; :: thesis: ( x in dom g implies g . x = H1(Y) . x )
assume A8: x in dom g ; :: thesis: g . x = H1(Y) . x
hence g . x = H1(Y) . x ; :: thesis: verum
end;
dom (Y --> 1) = Y ;
then A17: dom H1(Y) = X \/ Y by A3, FUNCT_4:def 1
.= X by XBOOLE_1:12 ;
dom g = X by FUNCT_2:def 1;
then H1(Y) = g by A17, A7;
then f . Y = g by A1, A6;
hence y in rng f by A1, A4, A6, FUNCT_1:def 3; :: thesis: verum
end;
for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2
proof
let x1, x2 be object ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume that
A18: x1 in dom f and
A19: x2 in dom f and
A20: f . x1 = f . x2 ; :: thesis: x1 = x2
consider Y2 being Subset of X such that
A21: x2 = Y2 and
A22: card Y2 = n by A1, A19;
consider Y1 being Subset of X such that
A23: x1 = Y1 and
A24: card Y1 = n by A1, A18;
Y1 c= Y2
proof
A25: dom (Y1 --> 1) = Y1 ;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Y1 or y in Y2 )
assume A26: y in Y1 ; :: thesis: y in Y2
(Y1 --> 1) . y = 1 by A26, FUNCOP_1:7;
then A27: H1(Y1) . y = 1 by A26, A25, FUNCT_4:13;
A28: H1(Y1) = f . x1 by A1, A18, A23;
A29: dom (Y2 --> 1) = Y2 ;
assume A30: not y in Y2 ; :: thesis: contradiction
(X --> 0) . y = 0 by A26, FUNCOP_1:7;
then H1(Y2) . y = 0 by A30, A29, FUNCT_4:11;
hence contradiction by A1, A19, A20, A21, A27, A28; :: thesis: verum
end;
hence x1 = x2 by A23, A24, A21, A22, CARD_2:102; :: thesis: verum
end;
then A31: f is one-to-one ;
rng f c= Choose (X,N,1,0)
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in Choose (X,N,1,0) )
assume y in rng f ; :: thesis: y in Choose (X,N,1,0)
then consider x being object such that
A32: x in dom f and
A33: f . x = y by FUNCT_1:def 3;
consider Y being Subset of X such that
A34: x = Y and
A35: card Y = n by A1, A32;
Y \/ X = X by XBOOLE_1:12;
then H1(Y) in Choose (X,N,1,0) by A35, CARD_FIN:17;
hence y in Choose (X,N,1,0) by A1, A32, A33, A34; :: thesis: verum
end;
then rng f = Choose (X,N,1,0) by A2, XBOOLE_0:def 10;
then { Y where Y is Subset of X : card Y = n } , Choose (X,N,1,0) are_equipotent by A1, A31, WELLORD2:def 4;
then card { Y where Y is Subset of X : card Y = n } = card (Choose (X,N,1,0)) by CARD_1:5;
hence card { Y where Y is Subset of X : card Y = n } = (card X) choose n by CARD_FIN:16; :: thesis: verum