Metamath Proof Explorer

Theorem hashbc

Description: The binomial coefficient counts the number of subsets of a finite set of a given size. This is Metamath 100 proof #58 (formula for the number of combinations). (Contributed by Mario Carneiro, 13-Jul-2014)

Ref Expression
Assertion hashbc ⊢A∈Fin∧K∈ℤ→(AK)=x∈𝒫A|x=K

Proof

Step Hyp Ref Expression
1 fveq2 ⊢w=∅→w=∅
2 1 oveq1d ⊢w=∅→(wk)=(∅k)
3 pweq ⊢w=∅→𝒫w=𝒫∅
4 3 rabeqdv ⊢w=∅→x∈𝒫w|x=k=x∈𝒫∅|x=k
5 4 fveq2d ⊢w=∅→x∈𝒫w|x=k=x∈𝒫∅|x=k
6 2 5 eqeq12d ⊢w=∅→(wk)=x∈𝒫w|x=k↔(∅k)=x∈𝒫∅|x=k
7 6 ralbidv ⊢w=∅→∀k∈ℤ(wk)=x∈𝒫w|x=k↔∀k∈ℤ(∅k)=x∈𝒫∅|x=k
8 fveq2 ⊢w=y→w=y
9 8 oveq1d ⊢w=y→(wk)=(yk)
10 pweq ⊢w=y→𝒫w=𝒫y
11 10 rabeqdv ⊢w=y→x∈𝒫w|x=k=x∈𝒫y|x=k
12 11 fveq2d ⊢w=y→x∈𝒫w|x=k=x∈𝒫y|x=k
13 9 12 eqeq12d ⊢w=y→(wk)=x∈𝒫w|x=k↔(yk)=x∈𝒫y|x=k
14 13 ralbidv ⊢w=y→∀k∈ℤ(wk)=x∈𝒫w|x=k↔∀k∈ℤ(yk)=x∈𝒫y|x=k
15 fveq2 ⊢w=y∪z→w=y∪z
16 15 oveq1d ⊢w=y∪z→(wk)=(y∪zk)
17 pweq ⊢w=y∪z→𝒫w=𝒫y∪z
18 17 rabeqdv ⊢w=y∪z→x∈𝒫w|x=k=x∈𝒫y∪z|x=k
19 18 fveq2d ⊢w=y∪z→x∈𝒫w|x=k=x∈𝒫y∪z|x=k
20 16 19 eqeq12d ⊢w=y∪z→(wk)=x∈𝒫w|x=k↔(y∪zk)=x∈𝒫y∪z|x=k
21 20 ralbidv ⊢w=y∪z→∀k∈ℤ(wk)=x∈𝒫w|x=k↔∀k∈ℤ(y∪zk)=x∈𝒫y∪z|x=k
22 fveq2 ⊢w=A→w=A
23 22 oveq1d ⊢w=A→(wk)=(Ak)
24 pweq ⊢w=A→𝒫w=𝒫A
25 24 rabeqdv ⊢w=A→x∈𝒫w|x=k=x∈𝒫A|x=k
26 25 fveq2d ⊢w=A→x∈𝒫w|x=k=x∈𝒫A|x=k
27 23 26 eqeq12d ⊢w=A→(wk)=x∈𝒫w|x=k↔(Ak)=x∈𝒫A|x=k
28 27 ralbidv ⊢w=A→∀k∈ℤ(wk)=x∈𝒫w|x=k↔∀k∈ℤ(Ak)=x∈𝒫A|x=k
29 hash0 ⊢∅=0
30 29 a1i ⊢k∈0…0→∅=0
31 elfz1eq ⊢k∈0…0→k=0
32 30 31 oveq12d ⊢k∈0…0→(∅k)=(00)
33 0nn0 ⊢0∈ℕ0
34 bcn0 ⊢0∈ℕ0→(00)=1
35 33 34 ax-mp ⊢(00)=1
36 32 35 eqtrdi ⊢k∈0…0→(∅k)=1
37 31 eqcomd ⊢k∈0…0→0=k
38 pw0 ⊢𝒫∅=∅
39 38 raleqi ⊢∀x∈𝒫∅x=k↔∀x∈∅x=k
40 0ex ⊢∅∈V
41 fveq2 ⊢x=∅→x=∅
42 41 29 eqtrdi ⊢x=∅→x=0
43 42 eqeq1d ⊢x=∅→x=k↔0=k
44 40 43 ralsn ⊢∀x∈∅x=k↔0=k
45 39 44 bitri ⊢∀x∈𝒫∅x=k↔0=k
46 37 45 sylibr ⊢k∈0…0→∀x∈𝒫∅x=k
47 rabid2 ⊢𝒫∅=x∈𝒫∅|x=k↔∀x∈𝒫∅x=k
48 46 47 sylibr ⊢k∈0…0→𝒫∅=x∈𝒫∅|x=k
49 48 38 eqtr3di ⊢k∈0…0→x∈𝒫∅|x=k=∅
50 49 fveq2d ⊢k∈0…0→x∈𝒫∅|x=k=∅
51 hashsng ⊢∅∈V→∅=1
52 40 51 ax-mp ⊢∅=1
53 50 52 eqtrdi ⊢k∈0…0→x∈𝒫∅|x=k=1
54 36 53 eqtr4d ⊢k∈0…0→(∅k)=x∈𝒫∅|x=k
55 54 adantl ⊢k∈ℤ∧k∈0…0→(∅k)=x∈𝒫∅|x=k
56 29 oveq1i ⊢(∅k)=(0k)
57 bcval3 ⊢0∈ℕ0∧k∈ℤ∧¬k∈0…0→(0k)=0
58 33 57 mp3an1 ⊢k∈ℤ∧¬k∈0…0→(0k)=0
59 id ⊢0=k→0=k
60 0z ⊢0∈ℤ
61 elfz3 ⊢0∈ℤ→0∈0…0
62 60 61 ax-mp ⊢0∈0…0
63 59 62 eqeltrrdi ⊢0=k→k∈0…0
64 63 con3i ⊢¬k∈0…0→¬0=k
65 64 adantl ⊢k∈ℤ∧¬k∈0…0→¬0=k
66 38 raleqi ⊢∀x∈𝒫∅¬x=k↔∀x∈∅¬x=k
67 43 notbid ⊢x=∅→¬x=k↔¬0=k
68 40 67 ralsn ⊢∀x∈∅¬x=k↔¬0=k
69 66 68 bitri ⊢∀x∈𝒫∅¬x=k↔¬0=k
70 65 69 sylibr ⊢k∈ℤ∧¬k∈0…0→∀x∈𝒫∅¬x=k
71 rabeq0 ⊢x∈𝒫∅|x=k=∅↔∀x∈𝒫∅¬x=k
72 70 71 sylibr ⊢k∈ℤ∧¬k∈0…0→x∈𝒫∅|x=k=∅
73 72 fveq2d ⊢k∈ℤ∧¬k∈0…0→x∈𝒫∅|x=k=∅
74 73 29 eqtrdi ⊢k∈ℤ∧¬k∈0…0→x∈𝒫∅|x=k=0
75 58 74 eqtr4d ⊢k∈ℤ∧¬k∈0…0→(0k)=x∈𝒫∅|x=k
76 56 75 eqtrid ⊢k∈ℤ∧¬k∈0…0→(∅k)=x∈𝒫∅|x=k
77 55 76 pm2.61dan ⊢k∈ℤ→(∅k)=x∈𝒫∅|x=k
78 77 rgen ⊢∀k∈ℤ(∅k)=x∈𝒫∅|x=k
79 oveq2 ⊢k=j→(yk)=(yj)
80 eqeq2 ⊢k=j→x=k↔x=j
81 80 rabbidv ⊢k=j→x∈𝒫y|x=k=x∈𝒫y|x=j
82 fveqeq2 ⊢x=z→x=j↔z=j
83 82 cbvrabv ⊢x∈𝒫y|x=j=z∈𝒫y|z=j
84 81 83 eqtrdi ⊢k=j→x∈𝒫y|x=k=z∈𝒫y|z=j
85 84 fveq2d ⊢k=j→x∈𝒫y|x=k=z∈𝒫y|z=j
86 79 85 eqeq12d ⊢k=j→(yk)=x∈𝒫y|x=k↔(yj)=z∈𝒫y|z=j
87 86 cbvralvw ⊢∀k∈ℤ(yk)=x∈𝒫y|x=k↔∀j∈ℤ(yj)=z∈𝒫y|z=j
88 simpll ⊢y∈Fin∧¬z∈y∧k∈ℤ∧∀j∈ℤ(yj)=z∈𝒫y|z=j→y∈Fin
89 simplr ⊢y∈Fin∧¬z∈y∧k∈ℤ∧∀j∈ℤ(yj)=z∈𝒫y|z=j→¬z∈y
90 simprr ⊢y∈Fin∧¬z∈y∧k∈ℤ∧∀j∈ℤ(yj)=z∈𝒫y|z=j→∀j∈ℤ(yj)=z∈𝒫y|z=j
91 83 fveq2i ⊢x∈𝒫y|x=j=z∈𝒫y|z=j
92 91 eqeq2i ⊢(yj)=x∈𝒫y|x=j↔(yj)=z∈𝒫y|z=j
93 92 ralbii ⊢∀j∈ℤ(yj)=x∈𝒫y|x=j↔∀j∈ℤ(yj)=z∈𝒫y|z=j
94 90 93 sylibr ⊢y∈Fin∧¬z∈y∧k∈ℤ∧∀j∈ℤ(yj)=z∈𝒫y|z=j→∀j∈ℤ(yj)=x∈𝒫y|x=j
95 simprl ⊢y∈Fin∧¬z∈y∧k∈ℤ∧∀j∈ℤ(yj)=z∈𝒫y|z=j→k∈ℤ
96 88 89 94 95 hashbclem ⊢y∈Fin∧¬z∈y∧k∈ℤ∧∀j∈ℤ(yj)=z∈𝒫y|z=j→(y∪zk)=x∈𝒫y∪z|x=k
97 96 expr ⊢y∈Fin∧¬z∈y∧k∈ℤ→∀j∈ℤ(yj)=z∈𝒫y|z=j→(y∪zk)=x∈𝒫y∪z|x=k
98 97 ralrimdva ⊢y∈Fin∧¬z∈y→∀j∈ℤ(yj)=z∈𝒫y|z=j→∀k∈ℤ(y∪zk)=x∈𝒫y∪z|x=k
99 87 98 biimtrid ⊢y∈Fin∧¬z∈y→∀k∈ℤ(yk)=x∈𝒫y|x=k→∀k∈ℤ(y∪zk)=x∈𝒫y∪z|x=k
100 7 14 21 28 78 99 findcard2s ⊢A∈Fin→∀k∈ℤ(Ak)=x∈𝒫A|x=k
101 oveq2 ⊢k=K→(Ak)=(AK)
102 eqeq2 ⊢k=K→x=k↔x=K
103 102 rabbidv ⊢k=K→x∈𝒫A|x=k=x∈𝒫A|x=K
104 103 fveq2d ⊢k=K→x∈𝒫A|x=k=x∈𝒫A|x=K
105 101 104 eqeq12d ⊢k=K→(Ak)=x∈𝒫A|x=k↔(AK)=x∈𝒫A|x=K
106 105 rspccva ⊢∀k∈ℤ(Ak)=x∈𝒫A|x=k∧K∈ℤ→(AK)=x∈𝒫A|x=K
107 100 106 sylan ⊢A∈Fin∧K∈ℤ→(AK)=x∈𝒫A|x=K