let E be non empty finite set ; for k being Element of NAT
for x1, x2 being set st x1 <> x2 holds
card (Choose (E,k,x1,x2)) = card (the_subsets_of_card (k,E))
let k be Element of NAT ; for x1, x2 being set st x1 <> x2 holds
card (Choose (E,k,x1,x2)) = card (the_subsets_of_card (k,E))
let x1, x2 be set ; ( x1 <> x2 implies card (Choose (E,k,x1,x2)) = card (the_subsets_of_card (k,E)) )
set f = { [fX,X] where fX is Function of E,{x1,x2}, X is Subset of E : ( card (fX " {x1}) = k & fX " {x1} = X ) } ;
now for x being object st x in { [fX,X] where fX is Function of E,{x1,x2}, X is Subset of E : ( card (fX " {x1}) = k & fX " {x1} = X ) } holds
ex y, z being object st x = [y,z]let x be
object ;
( x in { [fX,X] where fX is Function of E,{x1,x2}, X is Subset of E : ( card (fX " {x1}) = k & fX " {x1} = X ) } implies ex y, z being object st x = [y,z] )assume
x in { [fX,X] where fX is Function of E,{x1,x2}, X is Subset of E : ( card (fX " {x1}) = k & fX " {x1} = X ) }
;
ex y, z being object st x = [y,z]then consider y being
Function of
E,
{x1,x2},
z being
Subset of
E such that A1:
x = [y,z]
and
card (y " {x1}) = k
and
y " {x1} = z
;
reconsider y =
y,
z =
z as
object ;
take y =
y;
ex z being object st x = [y,z]take z =
z;
x = [y,z]thus
x = [y,z]
by A1;
verum end;
then reconsider f = { [fX,X] where fX is Function of E,{x1,x2}, X is Subset of E : ( card (fX " {x1}) = k & fX " {x1} = X ) } as Relation-like set by RELAT_1:def 1;
now for x, y1, y2 being object st [x,y1] in f & [x,y2] in f holds
y1 = y2let x,
y1,
y2 be
object ;
( [x,y1] in f & [x,y2] in f implies y1 = y2 )assume
[x,y1] in f
;
( [x,y2] in f implies y1 = y2 )then consider fX1 being
Function of
E,
{x1,x2},
X1 being
Subset of
E such that A2:
[x,y1] = [fX1,X1]
and
card (fX1 " {x1}) = k
and A3:
fX1 " {x1} = X1
;
A4:
x = fX1
by A2, XTUPLE_0:1;
assume
[x,y2] in f
;
y1 = y2then consider fX2 being
Function of
E,
{x1,x2},
X2 being
Subset of
E such that A5:
[x,y2] = [fX2,X2]
and
card (fX2 " {x1}) = k
and A6:
fX2 " {x1} = X2
;
x = fX2
by A5, XTUPLE_0:1;
hence
y1 = y2
by A2, A3, A5, A6, A4, XTUPLE_0:1;
verum end;
then reconsider f = f as Function by FUNCT_1:def 1;
assume A7:
x1 <> x2
; card (Choose (E,k,x1,x2)) = card (the_subsets_of_card (k,E))
now for y1, y2 being object st y1 in dom f & y2 in dom f & f . y1 = f . y2 holds
y1 = y2let y1,
y2 be
object ;
( y1 in dom f & y2 in dom f & f . y1 = f . y2 implies y1 = y2 )assume that A8:
y1 in dom f
and A9:
y2 in dom f
;
( f . y1 = f . y2 implies y1 = y2 )assume A10:
f . y1 = f . y2
;
y1 = y2
[y2,(f . y2)] in f
by A9, FUNCT_1:1;
then consider fX2 being
Function of
E,
{x1,x2},
X2 being
Subset of
E such that A11:
[y2,(f . y2)] = [fX2,X2]
and
card (fX2 " {x1}) = k
and A12:
fX2 " {x1} = X2
;
A13:
y2 = fX2
by A11, XTUPLE_0:1;
[y1,(f . y1)] in f
by A8, FUNCT_1:1;
then consider fX1 being
Function of
E,
{x1,x2},
X1 being
Subset of
E such that A14:
[y1,(f . y1)] = [fX1,X1]
and
card (fX1 " {x1}) = k
and A15:
fX1 " {x1} = X1
;
dom fX1 = E
by FUNCT_2:def 1;
then A16:
dom fX1 = dom fX2
by FUNCT_2:def 1;
f . y1 = X1
by A14, XTUPLE_0:1;
then A17:
fX1 " {x1} = fX2 " {x1}
by A10, A15, A11, A12, XTUPLE_0:1;
A18:
for
z being
object st
z in dom fX1 holds
fX1 . z = fX2 . z
proof
given z being
object such that A19:
z in dom fX1
and A20:
fX1 . z <> fX2 . z
;
contradiction
A21:
fX1 . z in {x1,x2}
by A19, FUNCT_2:5;
fX2 . z in {x1,x2}
by A19, FUNCT_2:5;
then A22:
(
fX2 . z = x1 or
fX2 . z = x2 )
by TARSKI:def 2;
per cases
( ( fX1 . z = x1 & fX2 . z = x2 ) or ( fX1 . z = x2 & fX2 . z = x1 ) )
by A20, A21, A22, TARSKI:def 2;
suppose A23:
(
fX1 . z = x1 &
fX2 . z = x2 )
;
contradictionend; suppose A27:
(
fX1 . z = x2 &
fX2 . z = x1 )
;
contradictionthen A28:
fX2 . z in {x1}
by TARSKI:def 1;
[z,(fX2 . z)] in fX2
by A16, A19, FUNCT_1:1;
then
z in fX1 " {x1}
by A17, A28, RELAT_1:def 14;
then consider z9 being
object such that A29:
[z,z9] in fX1
and A30:
z9 in {x1}
by RELAT_1:def 14;
z9 = fX1 . z
by A29, FUNCT_1:1;
hence
contradiction
by A7, A27, A30, TARSKI:def 1;
verum end; end;
end;
y1 = fX1
by A14, XTUPLE_0:1;
hence
y1 = y2
by A13, A16, A18, FUNCT_1:2;
verum end;
then A31:
f is one-to-one
by FUNCT_1:def 4;
for y being object holds
( y in the_subsets_of_card (k,E) iff ex x being object st [x,y] in f )
proof
let y be
object ;
( y in the_subsets_of_card (k,E) iff ex x being object st [x,y] in f )
hereby ( ex x being object st [x,y] in f implies y in the_subsets_of_card (k,E) )
assume
y in the_subsets_of_card (
k,
E)
;
ex x being object st [x,y] in fthen consider X being
Subset of
E such that A32:
(
y = X &
card X = k )
;
defpred S1[
set ,
set ]
means ( ( $1
in X & $2
= x1 ) or ( not $1
in X & $2
= x2 ) );
A33:
for
z1 being
Element of
E ex
z2 being
Element of
{x1,x2} st
S1[
z1,
z2]
ex
f being
Function of
E,
{x1,x2} st
for
z being
Element of
E holds
S1[
z,
f . z]
from FUNCT_2:sch 3(A33);
then consider f9 being
Function of
E,
{x1,x2} such that A36:
for
z being
Element of
E holds
S1[
z,
f9 . z]
;
reconsider x =
f9 as
object ;
take x =
x;
[x,y] in fthen
X = f9 " {x1}
by TARSKI:2;
hence
[x,y] in f
by A32;
verum
end;
given x being
object such that A41:
[x,y] in f
;
y in the_subsets_of_card (k,E)
consider fX being
Function of
E,
{x1,x2},
X being
Subset of
E such that A42:
[x,y] = [fX,X]
and A43:
(
card (fX " {x1}) = k &
fX " {x1} = X )
by A41;
y = X
by A42, XTUPLE_0:1;
hence
y in the_subsets_of_card (
k,
E)
by A43;
verum
end;
then A44:
rng f = the_subsets_of_card (k,E)
by XTUPLE_0:def 13;
for x being object holds
( x in Choose (E,k,x1,x2) iff ex y being object st [x,y] in f )
proof
let x be
object ;
( x in Choose (E,k,x1,x2) iff ex y being object st [x,y] in f )
thus
(
x in Choose (
E,
k,
x1,
x2) implies ex
y being
object st
[x,y] in f )
( ex y being object st [x,y] in f implies x in Choose (E,k,x1,x2) )
thus
( ex
y being
object st
[x,y] in f implies
x in Choose (
E,
k,
x1,
x2) )
verumproof
given y being
object such that A46:
[x,y] in f
;
x in Choose (E,k,x1,x2)
consider fX being
Function of
E,
{x1,x2},
X being
Subset of
E such that A47:
[x,y] = [fX,X]
and A48:
card (fX " {x1}) = k
and
fX " {x1} = X
by A46;
x = fX
by A47, XTUPLE_0:1;
hence
x in Choose (
E,
k,
x1,
x2)
by A48, CARD_FIN:def 1;
verum
end;
end;
then
dom f = Choose (E,k,x1,x2)
by XTUPLE_0:def 12;
then
Choose (E,k,x1,x2), the_subsets_of_card (k,E) are_equipotent
by A31, A44;
hence
card (Choose (E,k,x1,x2)) = card (the_subsets_of_card (k,E))
by CARD_1:5; verum