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 ∈ ℤ → ( A K) = x ∈ 𝒫 A | x = K

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ w = ∅ → w = ∅
2 1 oveq1d ⊢ w = ∅ → ( w k) = ( ∅ 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 = ∅ → ( w k) = x ∈ 𝒫 w | x = k ↔ ( ∅ k) = x ∈ 𝒫 ∅ | x = k
7 6 ralbidv ⊢ w = ∅ → ∀ k ∈ ℤ ( w k) = x ∈ 𝒫 w | x = k ↔ ∀ k ∈ ℤ ( ∅ k) = x ∈ 𝒫 ∅ | x = k
8 fveq2 ⊢ w = y → w = y
9 8 oveq1d ⊢ w = y → ( w k) = ( y k)
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 → ( w k) = x ∈ 𝒫 w | x = k ↔ ( y k) = x ∈ 𝒫 y | x = k
14 13 ralbidv ⊢ w = y → ∀ k ∈ ℤ ( w k) = x ∈ 𝒫 w | x = k ↔ ∀ k ∈ ℤ ( y k) = x ∈ 𝒫 y | x = k
15 fveq2 ⊢ w = y ∪ z → w = y ∪ z
16 15 oveq1d ⊢ w = y ∪ z → ( w k) = ( y ∪ z k)
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 → ( w k) = x ∈ 𝒫 w | x = k ↔ ( y ∪ z k) = x ∈ 𝒫 y ∪ z | x = k
21 20 ralbidv ⊢ w = y ∪ z → ∀ k ∈ ℤ ( w k) = x ∈ 𝒫 w | x = k ↔ ∀ k ∈ ℤ ( y ∪ z k) = x ∈ 𝒫 y ∪ z | x = k
22 fveq2 ⊢ w = A → w = A
23 22 oveq1d ⊢ w = A → ( w k) = ( A k)
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 → ( w k) = x ∈ 𝒫 w | x = k ↔ ( A k) = x ∈ 𝒫 A | x = k
28 27 ralbidv ⊢ w = A → ∀ k ∈ ℤ ( w k) = x ∈ 𝒫 w | x = k ↔ ∀ k ∈ ℤ ( A k) = 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) = ( 0 0 )
33 0nn0 ⊢ 0 ∈ ℕ 0
34 bcn0 ⊢ 0 ∈ ℕ 0 → ( 0 0 ) = 1
35 33 34 ax-mp ⊢ ( 0 0 ) = 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) = ( 0 k)
57 bcval3 ⊢ 0 ∈ ℕ 0 ∧ k ∈ ℤ ∧ ¬ k ∈ 0 … 0 → ( 0 k) = 0
58 33 57 mp3an1 ⊢ k ∈ ℤ ∧ ¬ k ∈ 0 … 0 → ( 0 k) = 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 → ( 0 k) = 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 → ( y k) = ( y j)
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 → ( y k) = x ∈ 𝒫 y | x = k ↔ ( y j) = z ∈ 𝒫 y | z = j
87 86 cbvralvw ⊢ ∀ k ∈ ℤ ( y k) = x ∈ 𝒫 y | x = k ↔ ∀ j ∈ ℤ ( y j) = z ∈ 𝒫 y | z = j
88 simpll ⊢ y ∈ Fin ∧ ¬ z ∈ y ∧ k ∈ ℤ ∧ ∀ j ∈ ℤ ( y j) = z ∈ 𝒫 y | z = j → y ∈ Fin
89 simplr ⊢ y ∈ Fin ∧ ¬ z ∈ y ∧ k ∈ ℤ ∧ ∀ j ∈ ℤ ( y j) = z ∈ 𝒫 y | z = j → ¬ z ∈ y
90 simprr ⊢ y ∈ Fin ∧ ¬ z ∈ y ∧ k ∈ ℤ ∧ ∀ j ∈ ℤ ( y j) = z ∈ 𝒫 y | z = j → ∀ j ∈ ℤ ( y j) = z ∈ 𝒫 y | z = j
91 83 fveq2i ⊢ x ∈ 𝒫 y | x = j = z ∈ 𝒫 y | z = j
92 91 eqeq2i ⊢ ( y j) = x ∈ 𝒫 y | x = j ↔ ( y j) = z ∈ 𝒫 y | z = j
93 92 ralbii ⊢ ∀ j ∈ ℤ ( y j) = x ∈ 𝒫 y | x = j ↔ ∀ j ∈ ℤ ( y j) = z ∈ 𝒫 y | z = j
94 90 93 sylibr ⊢ y ∈ Fin ∧ ¬ z ∈ y ∧ k ∈ ℤ ∧ ∀ j ∈ ℤ ( y j) = z ∈ 𝒫 y | z = j → ∀ j ∈ ℤ ( y j) = x ∈ 𝒫 y | x = j
95 simprl ⊢ y ∈ Fin ∧ ¬ z ∈ y ∧ k ∈ ℤ ∧ ∀ j ∈ ℤ ( y j) = z ∈ 𝒫 y | z = j → k ∈ ℤ
96 88 89 94 95 hashbclem ⊢ y ∈ Fin ∧ ¬ z ∈ y ∧ k ∈ ℤ ∧ ∀ j ∈ ℤ ( y j) = z ∈ 𝒫 y | z = j → ( y ∪ z k) = x ∈ 𝒫 y ∪ z | x = k
97 96 expr ⊢ y ∈ Fin ∧ ¬ z ∈ y ∧ k ∈ ℤ → ∀ j ∈ ℤ ( y j) = z ∈ 𝒫 y | z = j → ( y ∪ z k) = x ∈ 𝒫 y ∪ z | x = k
98 97 ralrimdva ⊢ y ∈ Fin ∧ ¬ z ∈ y → ∀ j ∈ ℤ ( y j) = z ∈ 𝒫 y | z = j → ∀ k ∈ ℤ ( y ∪ z k) = x ∈ 𝒫 y ∪ z | x = k
99 87 98 biimtrid ⊢ y ∈ Fin ∧ ¬ z ∈ y → ∀ k ∈ ℤ ( y k) = x ∈ 𝒫 y | x = k → ∀ k ∈ ℤ ( y ∪ z k) = x ∈ 𝒫 y ∪ z | x = k
100 7 14 21 28 78 99 findcard2s ⊢ A ∈ Fin → ∀ k ∈ ℤ ( A k) = x ∈ 𝒫 A | x = k
101 oveq2 ⊢ k = K → ( A k) = ( A K)
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 → ( A k) = x ∈ 𝒫 A | x = k ↔ ( A K) = x ∈ 𝒫 A | x = K
106 105 rspccva ⊢ ∀ k ∈ ℤ ( A k) = x ∈ 𝒫 A | x = k ∧ K ∈ ℤ → ( A K) = x ∈ 𝒫 A | x = K
107 100 106 sylan ⊢ A ∈ Fin ∧ K ∈ ℤ → ( A K) = x ∈ 𝒫 A | x = K