Step | Hyp | Ref
| Expression |
1 | | fveq2 6191 |
. . . . . 6
⊢ (𝑤 = ∅ → (#‘𝑤) =
(#‘∅)) |
2 | 1 | oveq1d 6665 |
. . . . 5
⊢ (𝑤 = ∅ →
((#‘𝑤)C𝑘) = ((#‘∅)C𝑘)) |
3 | | pweq 4161 |
. . . . . . 7
⊢ (𝑤 = ∅ → 𝒫
𝑤 = 𝒫
∅) |
4 | | rabeq 3192 |
. . . . . . 7
⊢
(𝒫 𝑤 =
𝒫 ∅ → {𝑥
∈ 𝒫 𝑤 ∣
(#‘𝑥) = 𝑘} = {𝑥 ∈ 𝒫 ∅ ∣
(#‘𝑥) = 𝑘}) |
5 | 3, 4 | syl 17 |
. . . . . 6
⊢ (𝑤 = ∅ → {𝑥 ∈ 𝒫 𝑤 ∣ (#‘𝑥) = 𝑘} = {𝑥 ∈ 𝒫 ∅ ∣
(#‘𝑥) = 𝑘}) |
6 | 5 | fveq2d 6195 |
. . . . 5
⊢ (𝑤 = ∅ →
(#‘{𝑥 ∈
𝒫 𝑤 ∣
(#‘𝑥) = 𝑘}) = (#‘{𝑥 ∈ 𝒫 ∅
∣ (#‘𝑥) = 𝑘})) |
7 | 2, 6 | eqeq12d 2637 |
. . . 4
⊢ (𝑤 = ∅ →
(((#‘𝑤)C𝑘) = (#‘{𝑥 ∈ 𝒫 𝑤 ∣ (#‘𝑥) = 𝑘}) ↔ ((#‘∅)C𝑘) = (#‘{𝑥 ∈ 𝒫 ∅ ∣
(#‘𝑥) = 𝑘}))) |
8 | 7 | ralbidv 2986 |
. . 3
⊢ (𝑤 = ∅ → (∀𝑘 ∈ ℤ ((#‘𝑤)C𝑘) = (#‘{𝑥 ∈ 𝒫 𝑤 ∣ (#‘𝑥) = 𝑘}) ↔ ∀𝑘 ∈ ℤ ((#‘∅)C𝑘) = (#‘{𝑥 ∈ 𝒫 ∅ ∣
(#‘𝑥) = 𝑘}))) |
9 | | fveq2 6191 |
. . . . . 6
⊢ (𝑤 = 𝑦 → (#‘𝑤) = (#‘𝑦)) |
10 | 9 | oveq1d 6665 |
. . . . 5
⊢ (𝑤 = 𝑦 → ((#‘𝑤)C𝑘) = ((#‘𝑦)C𝑘)) |
11 | | pweq 4161 |
. . . . . . 7
⊢ (𝑤 = 𝑦 → 𝒫 𝑤 = 𝒫 𝑦) |
12 | | rabeq 3192 |
. . . . . . 7
⊢
(𝒫 𝑤 =
𝒫 𝑦 → {𝑥 ∈ 𝒫 𝑤 ∣ (#‘𝑥) = 𝑘} = {𝑥 ∈ 𝒫 𝑦 ∣ (#‘𝑥) = 𝑘}) |
13 | 11, 12 | syl 17 |
. . . . . 6
⊢ (𝑤 = 𝑦 → {𝑥 ∈ 𝒫 𝑤 ∣ (#‘𝑥) = 𝑘} = {𝑥 ∈ 𝒫 𝑦 ∣ (#‘𝑥) = 𝑘}) |
14 | 13 | fveq2d 6195 |
. . . . 5
⊢ (𝑤 = 𝑦 → (#‘{𝑥 ∈ 𝒫 𝑤 ∣ (#‘𝑥) = 𝑘}) = (#‘{𝑥 ∈ 𝒫 𝑦 ∣ (#‘𝑥) = 𝑘})) |
15 | 10, 14 | eqeq12d 2637 |
. . . 4
⊢ (𝑤 = 𝑦 → (((#‘𝑤)C𝑘) = (#‘{𝑥 ∈ 𝒫 𝑤 ∣ (#‘𝑥) = 𝑘}) ↔ ((#‘𝑦)C𝑘) = (#‘{𝑥 ∈ 𝒫 𝑦 ∣ (#‘𝑥) = 𝑘}))) |
16 | 15 | ralbidv 2986 |
. . 3
⊢ (𝑤 = 𝑦 → (∀𝑘 ∈ ℤ ((#‘𝑤)C𝑘) = (#‘{𝑥 ∈ 𝒫 𝑤 ∣ (#‘𝑥) = 𝑘}) ↔ ∀𝑘 ∈ ℤ ((#‘𝑦)C𝑘) = (#‘{𝑥 ∈ 𝒫 𝑦 ∣ (#‘𝑥) = 𝑘}))) |
17 | | fveq2 6191 |
. . . . . 6
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (#‘𝑤) = (#‘(𝑦 ∪ {𝑧}))) |
18 | 17 | oveq1d 6665 |
. . . . 5
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → ((#‘𝑤)C𝑘) = ((#‘(𝑦 ∪ {𝑧}))C𝑘)) |
19 | | pweq 4161 |
. . . . . . 7
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → 𝒫 𝑤 = 𝒫 (𝑦 ∪ {𝑧})) |
20 | | rabeq 3192 |
. . . . . . 7
⊢
(𝒫 𝑤 =
𝒫 (𝑦 ∪ {𝑧}) → {𝑥 ∈ 𝒫 𝑤 ∣ (#‘𝑥) = 𝑘} = {𝑥 ∈ 𝒫 (𝑦 ∪ {𝑧}) ∣ (#‘𝑥) = 𝑘}) |
21 | 19, 20 | syl 17 |
. . . . . 6
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → {𝑥 ∈ 𝒫 𝑤 ∣ (#‘𝑥) = 𝑘} = {𝑥 ∈ 𝒫 (𝑦 ∪ {𝑧}) ∣ (#‘𝑥) = 𝑘}) |
22 | 21 | fveq2d 6195 |
. . . . 5
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (#‘{𝑥 ∈ 𝒫 𝑤 ∣ (#‘𝑥) = 𝑘}) = (#‘{𝑥 ∈ 𝒫 (𝑦 ∪ {𝑧}) ∣ (#‘𝑥) = 𝑘})) |
23 | 18, 22 | eqeq12d 2637 |
. . . 4
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (((#‘𝑤)C𝑘) = (#‘{𝑥 ∈ 𝒫 𝑤 ∣ (#‘𝑥) = 𝑘}) ↔ ((#‘(𝑦 ∪ {𝑧}))C𝑘) = (#‘{𝑥 ∈ 𝒫 (𝑦 ∪ {𝑧}) ∣ (#‘𝑥) = 𝑘}))) |
24 | 23 | ralbidv 2986 |
. . 3
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (∀𝑘 ∈ ℤ ((#‘𝑤)C𝑘) = (#‘{𝑥 ∈ 𝒫 𝑤 ∣ (#‘𝑥) = 𝑘}) ↔ ∀𝑘 ∈ ℤ ((#‘(𝑦 ∪ {𝑧}))C𝑘) = (#‘{𝑥 ∈ 𝒫 (𝑦 ∪ {𝑧}) ∣ (#‘𝑥) = 𝑘}))) |
25 | | fveq2 6191 |
. . . . . 6
⊢ (𝑤 = 𝐴 → (#‘𝑤) = (#‘𝐴)) |
26 | 25 | oveq1d 6665 |
. . . . 5
⊢ (𝑤 = 𝐴 → ((#‘𝑤)C𝑘) = ((#‘𝐴)C𝑘)) |
27 | | pweq 4161 |
. . . . . . 7
⊢ (𝑤 = 𝐴 → 𝒫 𝑤 = 𝒫 𝐴) |
28 | | rabeq 3192 |
. . . . . . 7
⊢
(𝒫 𝑤 =
𝒫 𝐴 → {𝑥 ∈ 𝒫 𝑤 ∣ (#‘𝑥) = 𝑘} = {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝑘}) |
29 | 27, 28 | syl 17 |
. . . . . 6
⊢ (𝑤 = 𝐴 → {𝑥 ∈ 𝒫 𝑤 ∣ (#‘𝑥) = 𝑘} = {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝑘}) |
30 | 29 | fveq2d 6195 |
. . . . 5
⊢ (𝑤 = 𝐴 → (#‘{𝑥 ∈ 𝒫 𝑤 ∣ (#‘𝑥) = 𝑘}) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝑘})) |
31 | 26, 30 | eqeq12d 2637 |
. . . 4
⊢ (𝑤 = 𝐴 → (((#‘𝑤)C𝑘) = (#‘{𝑥 ∈ 𝒫 𝑤 ∣ (#‘𝑥) = 𝑘}) ↔ ((#‘𝐴)C𝑘) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝑘}))) |
32 | 31 | ralbidv 2986 |
. . 3
⊢ (𝑤 = 𝐴 → (∀𝑘 ∈ ℤ ((#‘𝑤)C𝑘) = (#‘{𝑥 ∈ 𝒫 𝑤 ∣ (#‘𝑥) = 𝑘}) ↔ ∀𝑘 ∈ ℤ ((#‘𝐴)C𝑘) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝑘}))) |
33 | | hash0 13158 |
. . . . . . . . . 10
⊢
(#‘∅) = 0 |
34 | 33 | a1i 11 |
. . . . . . . . 9
⊢ (𝑘 ∈ (0...0) →
(#‘∅) = 0) |
35 | | elfz1eq 12352 |
. . . . . . . . 9
⊢ (𝑘 ∈ (0...0) → 𝑘 = 0) |
36 | 34, 35 | oveq12d 6668 |
. . . . . . . 8
⊢ (𝑘 ∈ (0...0) →
((#‘∅)C𝑘) =
(0C0)) |
37 | | 0nn0 11307 |
. . . . . . . . 9
⊢ 0 ∈
ℕ0 |
38 | | bcn0 13097 |
. . . . . . . . 9
⊢ (0 ∈
ℕ0 → (0C0) = 1) |
39 | 37, 38 | ax-mp 5 |
. . . . . . . 8
⊢ (0C0) =
1 |
40 | 36, 39 | syl6eq 2672 |
. . . . . . 7
⊢ (𝑘 ∈ (0...0) →
((#‘∅)C𝑘) =
1) |
41 | | pw0 4343 |
. . . . . . . . . 10
⊢ 𝒫
∅ = {∅} |
42 | 35 | eqcomd 2628 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (0...0) → 0 = 𝑘) |
43 | 41 | raleqi 3142 |
. . . . . . . . . . . . 13
⊢
(∀𝑥 ∈
𝒫 ∅(#‘𝑥) = 𝑘 ↔ ∀𝑥 ∈ {∅} (#‘𝑥) = 𝑘) |
44 | | 0ex 4790 |
. . . . . . . . . . . . . 14
⊢ ∅
∈ V |
45 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = ∅ → (#‘𝑥) =
(#‘∅)) |
46 | 45, 33 | syl6eq 2672 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = ∅ → (#‘𝑥) = 0) |
47 | 46 | eqeq1d 2624 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = ∅ →
((#‘𝑥) = 𝑘 ↔ 0 = 𝑘)) |
48 | 44, 47 | ralsn 4222 |
. . . . . . . . . . . . 13
⊢
(∀𝑥 ∈
{∅} (#‘𝑥) =
𝑘 ↔ 0 = 𝑘) |
49 | 43, 48 | bitri 264 |
. . . . . . . . . . . 12
⊢
(∀𝑥 ∈
𝒫 ∅(#‘𝑥) = 𝑘 ↔ 0 = 𝑘) |
50 | 42, 49 | sylibr 224 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (0...0) →
∀𝑥 ∈ 𝒫
∅(#‘𝑥) = 𝑘) |
51 | | rabid2 3118 |
. . . . . . . . . . 11
⊢
(𝒫 ∅ = {𝑥 ∈ 𝒫 ∅ ∣
(#‘𝑥) = 𝑘} ↔ ∀𝑥 ∈ 𝒫
∅(#‘𝑥) = 𝑘) |
52 | 50, 51 | sylibr 224 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (0...0) → 𝒫
∅ = {𝑥 ∈
𝒫 ∅ ∣ (#‘𝑥) = 𝑘}) |
53 | 41, 52 | syl5reqr 2671 |
. . . . . . . . 9
⊢ (𝑘 ∈ (0...0) → {𝑥 ∈ 𝒫 ∅
∣ (#‘𝑥) = 𝑘} = {∅}) |
54 | 53 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝑘 ∈ (0...0) →
(#‘{𝑥 ∈
𝒫 ∅ ∣ (#‘𝑥) = 𝑘}) = (#‘{∅})) |
55 | | hashsng 13159 |
. . . . . . . . 9
⊢ (∅
∈ V → (#‘{∅}) = 1) |
56 | 44, 55 | ax-mp 5 |
. . . . . . . 8
⊢
(#‘{∅}) = 1 |
57 | 54, 56 | syl6eq 2672 |
. . . . . . 7
⊢ (𝑘 ∈ (0...0) →
(#‘{𝑥 ∈
𝒫 ∅ ∣ (#‘𝑥) = 𝑘}) = 1) |
58 | 40, 57 | eqtr4d 2659 |
. . . . . 6
⊢ (𝑘 ∈ (0...0) →
((#‘∅)C𝑘) =
(#‘{𝑥 ∈
𝒫 ∅ ∣ (#‘𝑥) = 𝑘})) |
59 | 58 | adantl 482 |
. . . . 5
⊢ ((𝑘 ∈ ℤ ∧ 𝑘 ∈ (0...0)) →
((#‘∅)C𝑘) =
(#‘{𝑥 ∈
𝒫 ∅ ∣ (#‘𝑥) = 𝑘})) |
60 | 33 | oveq1i 6660 |
. . . . . 6
⊢
((#‘∅)C𝑘) = (0C𝑘) |
61 | | bcval3 13093 |
. . . . . . . 8
⊢ ((0
∈ ℕ0 ∧ 𝑘 ∈ ℤ ∧ ¬ 𝑘 ∈ (0...0)) → (0C𝑘) = 0) |
62 | 37, 61 | mp3an1 1411 |
. . . . . . 7
⊢ ((𝑘 ∈ ℤ ∧ ¬
𝑘 ∈ (0...0)) →
(0C𝑘) = 0) |
63 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (0 =
𝑘 → 0 = 𝑘) |
64 | | 0z 11388 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
ℤ |
65 | | elfz3 12351 |
. . . . . . . . . . . . . . 15
⊢ (0 ∈
ℤ → 0 ∈ (0...0)) |
66 | 64, 65 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
(0...0) |
67 | 63, 66 | syl6eqelr 2710 |
. . . . . . . . . . . . 13
⊢ (0 =
𝑘 → 𝑘 ∈ (0...0)) |
68 | 67 | con3i 150 |
. . . . . . . . . . . 12
⊢ (¬
𝑘 ∈ (0...0) →
¬ 0 = 𝑘) |
69 | 68 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℤ ∧ ¬
𝑘 ∈ (0...0)) →
¬ 0 = 𝑘) |
70 | 41 | raleqi 3142 |
. . . . . . . . . . . 12
⊢
(∀𝑥 ∈
𝒫 ∅ ¬ (#‘𝑥) = 𝑘 ↔ ∀𝑥 ∈ {∅} ¬ (#‘𝑥) = 𝑘) |
71 | 47 | notbid 308 |
. . . . . . . . . . . . 13
⊢ (𝑥 = ∅ → (¬
(#‘𝑥) = 𝑘 ↔ ¬ 0 = 𝑘)) |
72 | 44, 71 | ralsn 4222 |
. . . . . . . . . . . 12
⊢
(∀𝑥 ∈
{∅} ¬ (#‘𝑥)
= 𝑘 ↔ ¬ 0 = 𝑘) |
73 | 70, 72 | bitri 264 |
. . . . . . . . . . 11
⊢
(∀𝑥 ∈
𝒫 ∅ ¬ (#‘𝑥) = 𝑘 ↔ ¬ 0 = 𝑘) |
74 | 69, 73 | sylibr 224 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℤ ∧ ¬
𝑘 ∈ (0...0)) →
∀𝑥 ∈ 𝒫
∅ ¬ (#‘𝑥) =
𝑘) |
75 | | rabeq0 3957 |
. . . . . . . . . 10
⊢ ({𝑥 ∈ 𝒫 ∅
∣ (#‘𝑥) = 𝑘} = ∅ ↔ ∀𝑥 ∈ 𝒫 ∅ ¬
(#‘𝑥) = 𝑘) |
76 | 74, 75 | sylibr 224 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℤ ∧ ¬
𝑘 ∈ (0...0)) →
{𝑥 ∈ 𝒫 ∅
∣ (#‘𝑥) = 𝑘} = ∅) |
77 | 76 | fveq2d 6195 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℤ ∧ ¬
𝑘 ∈ (0...0)) →
(#‘{𝑥 ∈
𝒫 ∅ ∣ (#‘𝑥) = 𝑘}) = (#‘∅)) |
78 | 77, 33 | syl6eq 2672 |
. . . . . . 7
⊢ ((𝑘 ∈ ℤ ∧ ¬
𝑘 ∈ (0...0)) →
(#‘{𝑥 ∈
𝒫 ∅ ∣ (#‘𝑥) = 𝑘}) = 0) |
79 | 62, 78 | eqtr4d 2659 |
. . . . . 6
⊢ ((𝑘 ∈ ℤ ∧ ¬
𝑘 ∈ (0...0)) →
(0C𝑘) = (#‘{𝑥 ∈ 𝒫 ∅
∣ (#‘𝑥) = 𝑘})) |
80 | 60, 79 | syl5eq 2668 |
. . . . 5
⊢ ((𝑘 ∈ ℤ ∧ ¬
𝑘 ∈ (0...0)) →
((#‘∅)C𝑘) =
(#‘{𝑥 ∈
𝒫 ∅ ∣ (#‘𝑥) = 𝑘})) |
81 | 59, 80 | pm2.61dan 832 |
. . . 4
⊢ (𝑘 ∈ ℤ →
((#‘∅)C𝑘) =
(#‘{𝑥 ∈
𝒫 ∅ ∣ (#‘𝑥) = 𝑘})) |
82 | 81 | rgen 2922 |
. . 3
⊢
∀𝑘 ∈
ℤ ((#‘∅)C𝑘) = (#‘{𝑥 ∈ 𝒫 ∅ ∣
(#‘𝑥) = 𝑘}) |
83 | | oveq2 6658 |
. . . . . 6
⊢ (𝑘 = 𝑗 → ((#‘𝑦)C𝑘) = ((#‘𝑦)C𝑗)) |
84 | | eqeq2 2633 |
. . . . . . . . 9
⊢ (𝑘 = 𝑗 → ((#‘𝑥) = 𝑘 ↔ (#‘𝑥) = 𝑗)) |
85 | 84 | rabbidv 3189 |
. . . . . . . 8
⊢ (𝑘 = 𝑗 → {𝑥 ∈ 𝒫 𝑦 ∣ (#‘𝑥) = 𝑘} = {𝑥 ∈ 𝒫 𝑦 ∣ (#‘𝑥) = 𝑗}) |
86 | | fveq2 6191 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑧 → (#‘𝑥) = (#‘𝑧)) |
87 | 86 | eqeq1d 2624 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → ((#‘𝑥) = 𝑗 ↔ (#‘𝑧) = 𝑗)) |
88 | 87 | cbvrabv 3199 |
. . . . . . . 8
⊢ {𝑥 ∈ 𝒫 𝑦 ∣ (#‘𝑥) = 𝑗} = {𝑧 ∈ 𝒫 𝑦 ∣ (#‘𝑧) = 𝑗} |
89 | 85, 88 | syl6eq 2672 |
. . . . . . 7
⊢ (𝑘 = 𝑗 → {𝑥 ∈ 𝒫 𝑦 ∣ (#‘𝑥) = 𝑘} = {𝑧 ∈ 𝒫 𝑦 ∣ (#‘𝑧) = 𝑗}) |
90 | 89 | fveq2d 6195 |
. . . . . 6
⊢ (𝑘 = 𝑗 → (#‘{𝑥 ∈ 𝒫 𝑦 ∣ (#‘𝑥) = 𝑘}) = (#‘{𝑧 ∈ 𝒫 𝑦 ∣ (#‘𝑧) = 𝑗})) |
91 | 83, 90 | eqeq12d 2637 |
. . . . 5
⊢ (𝑘 = 𝑗 → (((#‘𝑦)C𝑘) = (#‘{𝑥 ∈ 𝒫 𝑦 ∣ (#‘𝑥) = 𝑘}) ↔ ((#‘𝑦)C𝑗) = (#‘{𝑧 ∈ 𝒫 𝑦 ∣ (#‘𝑧) = 𝑗}))) |
92 | 91 | cbvralv 3171 |
. . . 4
⊢
(∀𝑘 ∈
ℤ ((#‘𝑦)C𝑘) = (#‘{𝑥 ∈ 𝒫 𝑦 ∣ (#‘𝑥) = 𝑘}) ↔ ∀𝑗 ∈ ℤ ((#‘𝑦)C𝑗) = (#‘{𝑧 ∈ 𝒫 𝑦 ∣ (#‘𝑧) = 𝑗})) |
93 | | simpll 790 |
. . . . . . 7
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑘 ∈ ℤ ∧ ∀𝑗 ∈ ℤ ((#‘𝑦)C𝑗) = (#‘{𝑧 ∈ 𝒫 𝑦 ∣ (#‘𝑧) = 𝑗}))) → 𝑦 ∈ Fin) |
94 | | simplr 792 |
. . . . . . 7
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑘 ∈ ℤ ∧ ∀𝑗 ∈ ℤ ((#‘𝑦)C𝑗) = (#‘{𝑧 ∈ 𝒫 𝑦 ∣ (#‘𝑧) = 𝑗}))) → ¬ 𝑧 ∈ 𝑦) |
95 | | simprr 796 |
. . . . . . . 8
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑘 ∈ ℤ ∧ ∀𝑗 ∈ ℤ ((#‘𝑦)C𝑗) = (#‘{𝑧 ∈ 𝒫 𝑦 ∣ (#‘𝑧) = 𝑗}))) → ∀𝑗 ∈ ℤ ((#‘𝑦)C𝑗) = (#‘{𝑧 ∈ 𝒫 𝑦 ∣ (#‘𝑧) = 𝑗})) |
96 | 88 | fveq2i 6194 |
. . . . . . . . . 10
⊢
(#‘{𝑥 ∈
𝒫 𝑦 ∣
(#‘𝑥) = 𝑗}) = (#‘{𝑧 ∈ 𝒫 𝑦 ∣ (#‘𝑧) = 𝑗}) |
97 | 96 | eqeq2i 2634 |
. . . . . . . . 9
⊢
(((#‘𝑦)C𝑗) = (#‘{𝑥 ∈ 𝒫 𝑦 ∣ (#‘𝑥) = 𝑗}) ↔ ((#‘𝑦)C𝑗) = (#‘{𝑧 ∈ 𝒫 𝑦 ∣ (#‘𝑧) = 𝑗})) |
98 | 97 | ralbii 2980 |
. . . . . . . 8
⊢
(∀𝑗 ∈
ℤ ((#‘𝑦)C𝑗) = (#‘{𝑥 ∈ 𝒫 𝑦 ∣ (#‘𝑥) = 𝑗}) ↔ ∀𝑗 ∈ ℤ ((#‘𝑦)C𝑗) = (#‘{𝑧 ∈ 𝒫 𝑦 ∣ (#‘𝑧) = 𝑗})) |
99 | 95, 98 | sylibr 224 |
. . . . . . 7
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑘 ∈ ℤ ∧ ∀𝑗 ∈ ℤ ((#‘𝑦)C𝑗) = (#‘{𝑧 ∈ 𝒫 𝑦 ∣ (#‘𝑧) = 𝑗}))) → ∀𝑗 ∈ ℤ ((#‘𝑦)C𝑗) = (#‘{𝑥 ∈ 𝒫 𝑦 ∣ (#‘𝑥) = 𝑗})) |
100 | | simprl 794 |
. . . . . . 7
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑘 ∈ ℤ ∧ ∀𝑗 ∈ ℤ ((#‘𝑦)C𝑗) = (#‘{𝑧 ∈ 𝒫 𝑦 ∣ (#‘𝑧) = 𝑗}))) → 𝑘 ∈ ℤ) |
101 | 93, 94, 99, 100 | hashbclem 13236 |
. . . . . 6
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑘 ∈ ℤ ∧ ∀𝑗 ∈ ℤ ((#‘𝑦)C𝑗) = (#‘{𝑧 ∈ 𝒫 𝑦 ∣ (#‘𝑧) = 𝑗}))) → ((#‘(𝑦 ∪ {𝑧}))C𝑘) = (#‘{𝑥 ∈ 𝒫 (𝑦 ∪ {𝑧}) ∣ (#‘𝑥) = 𝑘})) |
102 | 101 | expr 643 |
. . . . 5
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑘 ∈ ℤ) → (∀𝑗 ∈ ℤ ((#‘𝑦)C𝑗) = (#‘{𝑧 ∈ 𝒫 𝑦 ∣ (#‘𝑧) = 𝑗}) → ((#‘(𝑦 ∪ {𝑧}))C𝑘) = (#‘{𝑥 ∈ 𝒫 (𝑦 ∪ {𝑧}) ∣ (#‘𝑥) = 𝑘}))) |
103 | 102 | ralrimdva 2969 |
. . . 4
⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (∀𝑗 ∈ ℤ ((#‘𝑦)C𝑗) = (#‘{𝑧 ∈ 𝒫 𝑦 ∣ (#‘𝑧) = 𝑗}) → ∀𝑘 ∈ ℤ ((#‘(𝑦 ∪ {𝑧}))C𝑘) = (#‘{𝑥 ∈ 𝒫 (𝑦 ∪ {𝑧}) ∣ (#‘𝑥) = 𝑘}))) |
104 | 92, 103 | syl5bi 232 |
. . 3
⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (∀𝑘 ∈ ℤ ((#‘𝑦)C𝑘) = (#‘{𝑥 ∈ 𝒫 𝑦 ∣ (#‘𝑥) = 𝑘}) → ∀𝑘 ∈ ℤ ((#‘(𝑦 ∪ {𝑧}))C𝑘) = (#‘{𝑥 ∈ 𝒫 (𝑦 ∪ {𝑧}) ∣ (#‘𝑥) = 𝑘}))) |
105 | 8, 16, 24, 32, 82, 104 | findcard2s 8201 |
. 2
⊢ (𝐴 ∈ Fin → ∀𝑘 ∈ ℤ ((#‘𝐴)C𝑘) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝑘})) |
106 | | oveq2 6658 |
. . . 4
⊢ (𝑘 = 𝐾 → ((#‘𝐴)C𝑘) = ((#‘𝐴)C𝐾)) |
107 | | eqeq2 2633 |
. . . . . 6
⊢ (𝑘 = 𝐾 → ((#‘𝑥) = 𝑘 ↔ (#‘𝑥) = 𝐾)) |
108 | 107 | rabbidv 3189 |
. . . . 5
⊢ (𝑘 = 𝐾 → {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝑘} = {𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝐾}) |
109 | 108 | fveq2d 6195 |
. . . 4
⊢ (𝑘 = 𝐾 → (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝑘}) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝐾})) |
110 | 106, 109 | eqeq12d 2637 |
. . 3
⊢ (𝑘 = 𝐾 → (((#‘𝐴)C𝑘) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝑘}) ↔ ((#‘𝐴)C𝐾) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝐾}))) |
111 | 110 | rspccva 3308 |
. 2
⊢
((∀𝑘 ∈
ℤ ((#‘𝐴)C𝑘) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝑘}) ∧ 𝐾 ∈ ℤ) → ((#‘𝐴)C𝐾) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝐾})) |
112 | 105, 111 | sylan 488 |
1
⊢ ((𝐴 ∈ Fin ∧ 𝐾 ∈ ℤ) →
((#‘𝐴)C𝐾) = (#‘{𝑥 ∈ 𝒫 𝐴 ∣ (#‘𝑥) = 𝐾})) |