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 ( ( 𝐴 ∈ Fin ∧ 𝐾 ∈ ℤ ) → ( ( ♯ ‘ 𝐴 ) C 𝐾 ) = ( ♯ ‘ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ♯ ‘ 𝑥 ) = 𝐾 } ) )

Proof

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