Step | Hyp | Ref
| Expression |
1 | | fveq2 6774 |
. . . . . 6
⊢ (𝑤 = ∅ →
(♯‘𝑤) =
(♯‘∅)) |
2 | 1 | oveq1d 7290 |
. . . . 5
⊢ (𝑤 = ∅ →
((♯‘𝑤)C𝑘) =
((♯‘∅)C𝑘)) |
3 | | pweq 4549 |
. . . . . . 7
⊢ (𝑤 = ∅ → 𝒫
𝑤 = 𝒫
∅) |
4 | 3 | rabeqdv 3419 |
. . . . . 6
⊢ (𝑤 = ∅ → {𝑥 ∈ 𝒫 𝑤 ∣ (♯‘𝑥) = 𝑘} = {𝑥 ∈ 𝒫 ∅ ∣
(♯‘𝑥) = 𝑘}) |
5 | 4 | fveq2d 6778 |
. . . . 5
⊢ (𝑤 = ∅ →
(♯‘{𝑥 ∈
𝒫 𝑤 ∣
(♯‘𝑥) = 𝑘}) = (♯‘{𝑥 ∈ 𝒫 ∅
∣ (♯‘𝑥) =
𝑘})) |
6 | 2, 5 | eqeq12d 2754 |
. . . 4
⊢ (𝑤 = ∅ →
(((♯‘𝑤)C𝑘) = (♯‘{𝑥 ∈ 𝒫 𝑤 ∣ (♯‘𝑥) = 𝑘}) ↔ ((♯‘∅)C𝑘) = (♯‘{𝑥 ∈ 𝒫 ∅
∣ (♯‘𝑥) =
𝑘}))) |
7 | 6 | ralbidv 3112 |
. . 3
⊢ (𝑤 = ∅ → (∀𝑘 ∈ ℤ
((♯‘𝑤)C𝑘) = (♯‘{𝑥 ∈ 𝒫 𝑤 ∣ (♯‘𝑥) = 𝑘}) ↔ ∀𝑘 ∈ ℤ
((♯‘∅)C𝑘)
= (♯‘{𝑥 ∈
𝒫 ∅ ∣ (♯‘𝑥) = 𝑘}))) |
8 | | fveq2 6774 |
. . . . . 6
⊢ (𝑤 = 𝑦 → (♯‘𝑤) = (♯‘𝑦)) |
9 | 8 | oveq1d 7290 |
. . . . 5
⊢ (𝑤 = 𝑦 → ((♯‘𝑤)C𝑘) = ((♯‘𝑦)C𝑘)) |
10 | | pweq 4549 |
. . . . . . 7
⊢ (𝑤 = 𝑦 → 𝒫 𝑤 = 𝒫 𝑦) |
11 | 10 | rabeqdv 3419 |
. . . . . 6
⊢ (𝑤 = 𝑦 → {𝑥 ∈ 𝒫 𝑤 ∣ (♯‘𝑥) = 𝑘} = {𝑥 ∈ 𝒫 𝑦 ∣ (♯‘𝑥) = 𝑘}) |
12 | 11 | fveq2d 6778 |
. . . . 5
⊢ (𝑤 = 𝑦 → (♯‘{𝑥 ∈ 𝒫 𝑤 ∣ (♯‘𝑥) = 𝑘}) = (♯‘{𝑥 ∈ 𝒫 𝑦 ∣ (♯‘𝑥) = 𝑘})) |
13 | 9, 12 | eqeq12d 2754 |
. . . 4
⊢ (𝑤 = 𝑦 → (((♯‘𝑤)C𝑘) = (♯‘{𝑥 ∈ 𝒫 𝑤 ∣ (♯‘𝑥) = 𝑘}) ↔ ((♯‘𝑦)C𝑘) = (♯‘{𝑥 ∈ 𝒫 𝑦 ∣ (♯‘𝑥) = 𝑘}))) |
14 | 13 | ralbidv 3112 |
. . 3
⊢ (𝑤 = 𝑦 → (∀𝑘 ∈ ℤ ((♯‘𝑤)C𝑘) = (♯‘{𝑥 ∈ 𝒫 𝑤 ∣ (♯‘𝑥) = 𝑘}) ↔ ∀𝑘 ∈ ℤ ((♯‘𝑦)C𝑘) = (♯‘{𝑥 ∈ 𝒫 𝑦 ∣ (♯‘𝑥) = 𝑘}))) |
15 | | fveq2 6774 |
. . . . . 6
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (♯‘𝑤) = (♯‘(𝑦 ∪ {𝑧}))) |
16 | 15 | oveq1d 7290 |
. . . . 5
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → ((♯‘𝑤)C𝑘) = ((♯‘(𝑦 ∪ {𝑧}))C𝑘)) |
17 | | pweq 4549 |
. . . . . . 7
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → 𝒫 𝑤 = 𝒫 (𝑦 ∪ {𝑧})) |
18 | 17 | rabeqdv 3419 |
. . . . . 6
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → {𝑥 ∈ 𝒫 𝑤 ∣ (♯‘𝑥) = 𝑘} = {𝑥 ∈ 𝒫 (𝑦 ∪ {𝑧}) ∣ (♯‘𝑥) = 𝑘}) |
19 | 18 | fveq2d 6778 |
. . . . 5
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (♯‘{𝑥 ∈ 𝒫 𝑤 ∣ (♯‘𝑥) = 𝑘}) = (♯‘{𝑥 ∈ 𝒫 (𝑦 ∪ {𝑧}) ∣ (♯‘𝑥) = 𝑘})) |
20 | 16, 19 | eqeq12d 2754 |
. . . 4
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (((♯‘𝑤)C𝑘) = (♯‘{𝑥 ∈ 𝒫 𝑤 ∣ (♯‘𝑥) = 𝑘}) ↔ ((♯‘(𝑦 ∪ {𝑧}))C𝑘) = (♯‘{𝑥 ∈ 𝒫 (𝑦 ∪ {𝑧}) ∣ (♯‘𝑥) = 𝑘}))) |
21 | 20 | ralbidv 3112 |
. . 3
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (∀𝑘 ∈ ℤ ((♯‘𝑤)C𝑘) = (♯‘{𝑥 ∈ 𝒫 𝑤 ∣ (♯‘𝑥) = 𝑘}) ↔ ∀𝑘 ∈ ℤ ((♯‘(𝑦 ∪ {𝑧}))C𝑘) = (♯‘{𝑥 ∈ 𝒫 (𝑦 ∪ {𝑧}) ∣ (♯‘𝑥) = 𝑘}))) |
22 | | fveq2 6774 |
. . . . . 6
⊢ (𝑤 = 𝐴 → (♯‘𝑤) = (♯‘𝐴)) |
23 | 22 | oveq1d 7290 |
. . . . 5
⊢ (𝑤 = 𝐴 → ((♯‘𝑤)C𝑘) = ((♯‘𝐴)C𝑘)) |
24 | | pweq 4549 |
. . . . . . 7
⊢ (𝑤 = 𝐴 → 𝒫 𝑤 = 𝒫 𝐴) |
25 | 24 | rabeqdv 3419 |
. . . . . 6
⊢ (𝑤 = 𝐴 → {𝑥 ∈ 𝒫 𝑤 ∣ (♯‘𝑥) = 𝑘} = {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑘}) |
26 | 25 | fveq2d 6778 |
. . . . 5
⊢ (𝑤 = 𝐴 → (♯‘{𝑥 ∈ 𝒫 𝑤 ∣ (♯‘𝑥) = 𝑘}) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑘})) |
27 | 23, 26 | eqeq12d 2754 |
. . . 4
⊢ (𝑤 = 𝐴 → (((♯‘𝑤)C𝑘) = (♯‘{𝑥 ∈ 𝒫 𝑤 ∣ (♯‘𝑥) = 𝑘}) ↔ ((♯‘𝐴)C𝑘) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑘}))) |
28 | 27 | ralbidv 3112 |
. . 3
⊢ (𝑤 = 𝐴 → (∀𝑘 ∈ ℤ ((♯‘𝑤)C𝑘) = (♯‘{𝑥 ∈ 𝒫 𝑤 ∣ (♯‘𝑥) = 𝑘}) ↔ ∀𝑘 ∈ ℤ ((♯‘𝐴)C𝑘) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑘}))) |
29 | | hash0 14082 |
. . . . . . . . . 10
⊢
(♯‘∅) = 0 |
30 | 29 | a1i 11 |
. . . . . . . . 9
⊢ (𝑘 ∈ (0...0) →
(♯‘∅) = 0) |
31 | | elfz1eq 13267 |
. . . . . . . . 9
⊢ (𝑘 ∈ (0...0) → 𝑘 = 0) |
32 | 30, 31 | oveq12d 7293 |
. . . . . . . 8
⊢ (𝑘 ∈ (0...0) →
((♯‘∅)C𝑘)
= (0C0)) |
33 | | 0nn0 12248 |
. . . . . . . . 9
⊢ 0 ∈
ℕ0 |
34 | | bcn0 14024 |
. . . . . . . . 9
⊢ (0 ∈
ℕ0 → (0C0) = 1) |
35 | 33, 34 | ax-mp 5 |
. . . . . . . 8
⊢ (0C0) =
1 |
36 | 32, 35 | eqtrdi 2794 |
. . . . . . 7
⊢ (𝑘 ∈ (0...0) →
((♯‘∅)C𝑘)
= 1) |
37 | 31 | eqcomd 2744 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (0...0) → 0 = 𝑘) |
38 | | pw0 4745 |
. . . . . . . . . . . . . 14
⊢ 𝒫
∅ = {∅} |
39 | 38 | raleqi 3346 |
. . . . . . . . . . . . 13
⊢
(∀𝑥 ∈
𝒫 ∅(♯‘𝑥) = 𝑘 ↔ ∀𝑥 ∈ {∅} (♯‘𝑥) = 𝑘) |
40 | | 0ex 5231 |
. . . . . . . . . . . . . 14
⊢ ∅
∈ V |
41 | | fveq2 6774 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = ∅ →
(♯‘𝑥) =
(♯‘∅)) |
42 | 41, 29 | eqtrdi 2794 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = ∅ →
(♯‘𝑥) =
0) |
43 | 42 | eqeq1d 2740 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = ∅ →
((♯‘𝑥) = 𝑘 ↔ 0 = 𝑘)) |
44 | 40, 43 | ralsn 4617 |
. . . . . . . . . . . . 13
⊢
(∀𝑥 ∈
{∅} (♯‘𝑥)
= 𝑘 ↔ 0 = 𝑘) |
45 | 39, 44 | bitri 274 |
. . . . . . . . . . . 12
⊢
(∀𝑥 ∈
𝒫 ∅(♯‘𝑥) = 𝑘 ↔ 0 = 𝑘) |
46 | 37, 45 | sylibr 233 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (0...0) →
∀𝑥 ∈ 𝒫
∅(♯‘𝑥) =
𝑘) |
47 | | rabid2 3314 |
. . . . . . . . . . 11
⊢
(𝒫 ∅ = {𝑥 ∈ 𝒫 ∅ ∣
(♯‘𝑥) = 𝑘} ↔ ∀𝑥 ∈ 𝒫
∅(♯‘𝑥) =
𝑘) |
48 | 46, 47 | sylibr 233 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (0...0) → 𝒫
∅ = {𝑥 ∈
𝒫 ∅ ∣ (♯‘𝑥) = 𝑘}) |
49 | 48, 38 | eqtr3di 2793 |
. . . . . . . . 9
⊢ (𝑘 ∈ (0...0) → {𝑥 ∈ 𝒫 ∅
∣ (♯‘𝑥) =
𝑘} =
{∅}) |
50 | 49 | fveq2d 6778 |
. . . . . . . 8
⊢ (𝑘 ∈ (0...0) →
(♯‘{𝑥 ∈
𝒫 ∅ ∣ (♯‘𝑥) = 𝑘}) =
(♯‘{∅})) |
51 | | hashsng 14084 |
. . . . . . . . 9
⊢ (∅
∈ V → (♯‘{∅}) = 1) |
52 | 40, 51 | ax-mp 5 |
. . . . . . . 8
⊢
(♯‘{∅}) = 1 |
53 | 50, 52 | eqtrdi 2794 |
. . . . . . 7
⊢ (𝑘 ∈ (0...0) →
(♯‘{𝑥 ∈
𝒫 ∅ ∣ (♯‘𝑥) = 𝑘}) = 1) |
54 | 36, 53 | eqtr4d 2781 |
. . . . . 6
⊢ (𝑘 ∈ (0...0) →
((♯‘∅)C𝑘)
= (♯‘{𝑥 ∈
𝒫 ∅ ∣ (♯‘𝑥) = 𝑘})) |
55 | 54 | adantl 482 |
. . . . 5
⊢ ((𝑘 ∈ ℤ ∧ 𝑘 ∈ (0...0)) →
((♯‘∅)C𝑘)
= (♯‘{𝑥 ∈
𝒫 ∅ ∣ (♯‘𝑥) = 𝑘})) |
56 | 29 | oveq1i 7285 |
. . . . . 6
⊢
((♯‘∅)C𝑘) = (0C𝑘) |
57 | | bcval3 14020 |
. . . . . . . 8
⊢ ((0
∈ ℕ0 ∧ 𝑘 ∈ ℤ ∧ ¬ 𝑘 ∈ (0...0)) → (0C𝑘) = 0) |
58 | 33, 57 | mp3an1 1447 |
. . . . . . 7
⊢ ((𝑘 ∈ ℤ ∧ ¬
𝑘 ∈ (0...0)) →
(0C𝑘) = 0) |
59 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (0 =
𝑘 → 0 = 𝑘) |
60 | | 0z 12330 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
ℤ |
61 | | elfz3 13266 |
. . . . . . . . . . . . . . 15
⊢ (0 ∈
ℤ → 0 ∈ (0...0)) |
62 | 60, 61 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
(0...0) |
63 | 59, 62 | eqeltrrdi 2848 |
. . . . . . . . . . . . 13
⊢ (0 =
𝑘 → 𝑘 ∈ (0...0)) |
64 | 63 | con3i 154 |
. . . . . . . . . . . 12
⊢ (¬
𝑘 ∈ (0...0) →
¬ 0 = 𝑘) |
65 | 64 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℤ ∧ ¬
𝑘 ∈ (0...0)) →
¬ 0 = 𝑘) |
66 | 38 | raleqi 3346 |
. . . . . . . . . . . 12
⊢
(∀𝑥 ∈
𝒫 ∅ ¬ (♯‘𝑥) = 𝑘 ↔ ∀𝑥 ∈ {∅} ¬ (♯‘𝑥) = 𝑘) |
67 | 43 | notbid 318 |
. . . . . . . . . . . . 13
⊢ (𝑥 = ∅ → (¬
(♯‘𝑥) = 𝑘 ↔ ¬ 0 = 𝑘)) |
68 | 40, 67 | ralsn 4617 |
. . . . . . . . . . . 12
⊢
(∀𝑥 ∈
{∅} ¬ (♯‘𝑥) = 𝑘 ↔ ¬ 0 = 𝑘) |
69 | 66, 68 | bitri 274 |
. . . . . . . . . . 11
⊢
(∀𝑥 ∈
𝒫 ∅ ¬ (♯‘𝑥) = 𝑘 ↔ ¬ 0 = 𝑘) |
70 | 65, 69 | sylibr 233 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℤ ∧ ¬
𝑘 ∈ (0...0)) →
∀𝑥 ∈ 𝒫
∅ ¬ (♯‘𝑥) = 𝑘) |
71 | | rabeq0 4318 |
. . . . . . . . . 10
⊢ ({𝑥 ∈ 𝒫 ∅
∣ (♯‘𝑥) =
𝑘} = ∅ ↔
∀𝑥 ∈ 𝒫
∅ ¬ (♯‘𝑥) = 𝑘) |
72 | 70, 71 | sylibr 233 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℤ ∧ ¬
𝑘 ∈ (0...0)) →
{𝑥 ∈ 𝒫 ∅
∣ (♯‘𝑥) =
𝑘} =
∅) |
73 | 72 | fveq2d 6778 |
. . . . . . . 8
⊢ ((𝑘 ∈ ℤ ∧ ¬
𝑘 ∈ (0...0)) →
(♯‘{𝑥 ∈
𝒫 ∅ ∣ (♯‘𝑥) = 𝑘}) =
(♯‘∅)) |
74 | 73, 29 | eqtrdi 2794 |
. . . . . . 7
⊢ ((𝑘 ∈ ℤ ∧ ¬
𝑘 ∈ (0...0)) →
(♯‘{𝑥 ∈
𝒫 ∅ ∣ (♯‘𝑥) = 𝑘}) = 0) |
75 | 58, 74 | eqtr4d 2781 |
. . . . . 6
⊢ ((𝑘 ∈ ℤ ∧ ¬
𝑘 ∈ (0...0)) →
(0C𝑘) =
(♯‘{𝑥 ∈
𝒫 ∅ ∣ (♯‘𝑥) = 𝑘})) |
76 | 56, 75 | eqtrid 2790 |
. . . . 5
⊢ ((𝑘 ∈ ℤ ∧ ¬
𝑘 ∈ (0...0)) →
((♯‘∅)C𝑘)
= (♯‘{𝑥 ∈
𝒫 ∅ ∣ (♯‘𝑥) = 𝑘})) |
77 | 55, 76 | pm2.61dan 810 |
. . . 4
⊢ (𝑘 ∈ ℤ →
((♯‘∅)C𝑘)
= (♯‘{𝑥 ∈
𝒫 ∅ ∣ (♯‘𝑥) = 𝑘})) |
78 | 77 | rgen 3074 |
. . 3
⊢
∀𝑘 ∈
ℤ ((♯‘∅)C𝑘) = (♯‘{𝑥 ∈ 𝒫 ∅ ∣
(♯‘𝑥) = 𝑘}) |
79 | | oveq2 7283 |
. . . . . 6
⊢ (𝑘 = 𝑗 → ((♯‘𝑦)C𝑘) = ((♯‘𝑦)C𝑗)) |
80 | | eqeq2 2750 |
. . . . . . . . 9
⊢ (𝑘 = 𝑗 → ((♯‘𝑥) = 𝑘 ↔ (♯‘𝑥) = 𝑗)) |
81 | 80 | rabbidv 3414 |
. . . . . . . 8
⊢ (𝑘 = 𝑗 → {𝑥 ∈ 𝒫 𝑦 ∣ (♯‘𝑥) = 𝑘} = {𝑥 ∈ 𝒫 𝑦 ∣ (♯‘𝑥) = 𝑗}) |
82 | | fveqeq2 6783 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → ((♯‘𝑥) = 𝑗 ↔ (♯‘𝑧) = 𝑗)) |
83 | 82 | cbvrabv 3426 |
. . . . . . . 8
⊢ {𝑥 ∈ 𝒫 𝑦 ∣ (♯‘𝑥) = 𝑗} = {𝑧 ∈ 𝒫 𝑦 ∣ (♯‘𝑧) = 𝑗} |
84 | 81, 83 | eqtrdi 2794 |
. . . . . . 7
⊢ (𝑘 = 𝑗 → {𝑥 ∈ 𝒫 𝑦 ∣ (♯‘𝑥) = 𝑘} = {𝑧 ∈ 𝒫 𝑦 ∣ (♯‘𝑧) = 𝑗}) |
85 | 84 | fveq2d 6778 |
. . . . . 6
⊢ (𝑘 = 𝑗 → (♯‘{𝑥 ∈ 𝒫 𝑦 ∣ (♯‘𝑥) = 𝑘}) = (♯‘{𝑧 ∈ 𝒫 𝑦 ∣ (♯‘𝑧) = 𝑗})) |
86 | 79, 85 | eqeq12d 2754 |
. . . . 5
⊢ (𝑘 = 𝑗 → (((♯‘𝑦)C𝑘) = (♯‘{𝑥 ∈ 𝒫 𝑦 ∣ (♯‘𝑥) = 𝑘}) ↔ ((♯‘𝑦)C𝑗) = (♯‘{𝑧 ∈ 𝒫 𝑦 ∣ (♯‘𝑧) = 𝑗}))) |
87 | 86 | cbvralvw 3383 |
. . . 4
⊢
(∀𝑘 ∈
ℤ ((♯‘𝑦)C𝑘) = (♯‘{𝑥 ∈ 𝒫 𝑦 ∣ (♯‘𝑥) = 𝑘}) ↔ ∀𝑗 ∈ ℤ ((♯‘𝑦)C𝑗) = (♯‘{𝑧 ∈ 𝒫 𝑦 ∣ (♯‘𝑧) = 𝑗})) |
88 | | simpll 764 |
. . . . . . 7
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑘 ∈ ℤ ∧ ∀𝑗 ∈ ℤ
((♯‘𝑦)C𝑗) = (♯‘{𝑧 ∈ 𝒫 𝑦 ∣ (♯‘𝑧) = 𝑗}))) → 𝑦 ∈ Fin) |
89 | | simplr 766 |
. . . . . . 7
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑘 ∈ ℤ ∧ ∀𝑗 ∈ ℤ
((♯‘𝑦)C𝑗) = (♯‘{𝑧 ∈ 𝒫 𝑦 ∣ (♯‘𝑧) = 𝑗}))) → ¬ 𝑧 ∈ 𝑦) |
90 | | simprr 770 |
. . . . . . . 8
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑘 ∈ ℤ ∧ ∀𝑗 ∈ ℤ
((♯‘𝑦)C𝑗) = (♯‘{𝑧 ∈ 𝒫 𝑦 ∣ (♯‘𝑧) = 𝑗}))) → ∀𝑗 ∈ ℤ ((♯‘𝑦)C𝑗) = (♯‘{𝑧 ∈ 𝒫 𝑦 ∣ (♯‘𝑧) = 𝑗})) |
91 | 83 | fveq2i 6777 |
. . . . . . . . . 10
⊢
(♯‘{𝑥
∈ 𝒫 𝑦 ∣
(♯‘𝑥) = 𝑗}) = (♯‘{𝑧 ∈ 𝒫 𝑦 ∣ (♯‘𝑧) = 𝑗}) |
92 | 91 | eqeq2i 2751 |
. . . . . . . . 9
⊢
(((♯‘𝑦)C𝑗) = (♯‘{𝑥 ∈ 𝒫 𝑦 ∣ (♯‘𝑥) = 𝑗}) ↔ ((♯‘𝑦)C𝑗) = (♯‘{𝑧 ∈ 𝒫 𝑦 ∣ (♯‘𝑧) = 𝑗})) |
93 | 92 | ralbii 3092 |
. . . . . . . 8
⊢
(∀𝑗 ∈
ℤ ((♯‘𝑦)C𝑗) = (♯‘{𝑥 ∈ 𝒫 𝑦 ∣ (♯‘𝑥) = 𝑗}) ↔ ∀𝑗 ∈ ℤ ((♯‘𝑦)C𝑗) = (♯‘{𝑧 ∈ 𝒫 𝑦 ∣ (♯‘𝑧) = 𝑗})) |
94 | 90, 93 | sylibr 233 |
. . . . . . 7
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑘 ∈ ℤ ∧ ∀𝑗 ∈ ℤ
((♯‘𝑦)C𝑗) = (♯‘{𝑧 ∈ 𝒫 𝑦 ∣ (♯‘𝑧) = 𝑗}))) → ∀𝑗 ∈ ℤ ((♯‘𝑦)C𝑗) = (♯‘{𝑥 ∈ 𝒫 𝑦 ∣ (♯‘𝑥) = 𝑗})) |
95 | | simprl 768 |
. . . . . . 7
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑘 ∈ ℤ ∧ ∀𝑗 ∈ ℤ
((♯‘𝑦)C𝑗) = (♯‘{𝑧 ∈ 𝒫 𝑦 ∣ (♯‘𝑧) = 𝑗}))) → 𝑘 ∈ ℤ) |
96 | 88, 89, 94, 95 | hashbclem 14164 |
. . . . . 6
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑘 ∈ ℤ ∧ ∀𝑗 ∈ ℤ
((♯‘𝑦)C𝑗) = (♯‘{𝑧 ∈ 𝒫 𝑦 ∣ (♯‘𝑧) = 𝑗}))) → ((♯‘(𝑦 ∪ {𝑧}))C𝑘) = (♯‘{𝑥 ∈ 𝒫 (𝑦 ∪ {𝑧}) ∣ (♯‘𝑥) = 𝑘})) |
97 | 96 | expr 457 |
. . . . 5
⊢ (((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑘 ∈ ℤ) → (∀𝑗 ∈ ℤ
((♯‘𝑦)C𝑗) = (♯‘{𝑧 ∈ 𝒫 𝑦 ∣ (♯‘𝑧) = 𝑗}) → ((♯‘(𝑦 ∪ {𝑧}))C𝑘) = (♯‘{𝑥 ∈ 𝒫 (𝑦 ∪ {𝑧}) ∣ (♯‘𝑥) = 𝑘}))) |
98 | 97 | ralrimdva 3106 |
. . . 4
⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (∀𝑗 ∈ ℤ ((♯‘𝑦)C𝑗) = (♯‘{𝑧 ∈ 𝒫 𝑦 ∣ (♯‘𝑧) = 𝑗}) → ∀𝑘 ∈ ℤ ((♯‘(𝑦 ∪ {𝑧}))C𝑘) = (♯‘{𝑥 ∈ 𝒫 (𝑦 ∪ {𝑧}) ∣ (♯‘𝑥) = 𝑘}))) |
99 | 87, 98 | syl5bi 241 |
. . 3
⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (∀𝑘 ∈ ℤ ((♯‘𝑦)C𝑘) = (♯‘{𝑥 ∈ 𝒫 𝑦 ∣ (♯‘𝑥) = 𝑘}) → ∀𝑘 ∈ ℤ ((♯‘(𝑦 ∪ {𝑧}))C𝑘) = (♯‘{𝑥 ∈ 𝒫 (𝑦 ∪ {𝑧}) ∣ (♯‘𝑥) = 𝑘}))) |
100 | 7, 14, 21, 28, 78, 99 | findcard2s 8948 |
. 2
⊢ (𝐴 ∈ Fin → ∀𝑘 ∈ ℤ
((♯‘𝐴)C𝑘) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑘})) |
101 | | oveq2 7283 |
. . . 4
⊢ (𝑘 = 𝐾 → ((♯‘𝐴)C𝑘) = ((♯‘𝐴)C𝐾)) |
102 | | eqeq2 2750 |
. . . . . 6
⊢ (𝑘 = 𝐾 → ((♯‘𝑥) = 𝑘 ↔ (♯‘𝑥) = 𝐾)) |
103 | 102 | rabbidv 3414 |
. . . . 5
⊢ (𝑘 = 𝐾 → {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑘} = {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝐾}) |
104 | 103 | fveq2d 6778 |
. . . 4
⊢ (𝑘 = 𝐾 → (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑘}) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝐾})) |
105 | 101, 104 | eqeq12d 2754 |
. . 3
⊢ (𝑘 = 𝐾 → (((♯‘𝐴)C𝑘) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑘}) ↔ ((♯‘𝐴)C𝐾) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝐾}))) |
106 | 105 | rspccva 3560 |
. 2
⊢
((∀𝑘 ∈
ℤ ((♯‘𝐴)C𝑘) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑘}) ∧ 𝐾 ∈ ℤ) →
((♯‘𝐴)C𝐾) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝐾})) |
107 | 100, 106 | sylan 580 |
1
⊢ ((𝐴 ∈ Fin ∧ 𝐾 ∈ ℤ) →
((♯‘𝐴)C𝐾) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝐾})) |