Step | Hyp | Ref
| Expression |
1 | | oveq2 7230 |
. . . . . 6
⊢ (𝑗 = 𝐾 → ((♯‘𝐴)C𝑗) = ((♯‘𝐴)C𝐾)) |
2 | | eqeq2 2750 |
. . . . . . . 8
⊢ (𝑗 = 𝐾 → ((♯‘𝑥) = 𝑗 ↔ (♯‘𝑥) = 𝐾)) |
3 | 2 | rabbidv 3397 |
. . . . . . 7
⊢ (𝑗 = 𝐾 → {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑗} = {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝐾}) |
4 | 3 | fveq2d 6730 |
. . . . . 6
⊢ (𝑗 = 𝐾 → (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑗}) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝐾})) |
5 | 1, 4 | eqeq12d 2754 |
. . . . 5
⊢ (𝑗 = 𝐾 → (((♯‘𝐴)C𝑗) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑗}) ↔ ((♯‘𝐴)C𝐾) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝐾}))) |
6 | | hashbc.3 |
. . . . 5
⊢ (𝜑 → ∀𝑗 ∈ ℤ ((♯‘𝐴)C𝑗) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑗})) |
7 | | hashbc.4 |
. . . . 5
⊢ (𝜑 → 𝐾 ∈ ℤ) |
8 | 5, 6, 7 | rspcdva 3546 |
. . . 4
⊢ (𝜑 → ((♯‘𝐴)C𝐾) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝐾})) |
9 | | ssun1 4095 |
. . . . . . . . . . . . 13
⊢ 𝐴 ⊆ (𝐴 ∪ {𝑧}) |
10 | 9 | sspwi 4536 |
. . . . . . . . . . . 12
⊢ 𝒫
𝐴 ⊆ 𝒫 (𝐴 ∪ {𝑧}) |
11 | 10 | sseli 3905 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧})) |
12 | 11 | adantl 485 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝐴) → 𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧})) |
13 | | hashbc.2 |
. . . . . . . . . . 11
⊢ (𝜑 → ¬ 𝑧 ∈ 𝐴) |
14 | | elpwi 4531 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝒫 𝐴 → 𝑥 ⊆ 𝐴) |
15 | 14 | ssneld 3912 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝒫 𝐴 → (¬ 𝑧 ∈ 𝐴 → ¬ 𝑧 ∈ 𝑥)) |
16 | 13, 15 | mpan9 510 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝐴) → ¬ 𝑧 ∈ 𝑥) |
17 | 12, 16 | jca 515 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝐴) → (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥)) |
18 | | elpwi 4531 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) → 𝑥 ⊆ (𝐴 ∪ {𝑧})) |
19 | | uncom 4076 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∪ {𝑧}) = ({𝑧} ∪ 𝐴) |
20 | 18, 19 | sseqtrdi 3960 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) → 𝑥 ⊆ ({𝑧} ∪ 𝐴)) |
21 | 20 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥) → 𝑥 ⊆ ({𝑧} ∪ 𝐴)) |
22 | | simpr 488 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥) → ¬ 𝑧 ∈ 𝑥) |
23 | | disjsn 4636 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑥) |
24 | 22, 23 | sylibr 237 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥) → (𝑥 ∩ {𝑧}) = ∅) |
25 | | disjssun 4391 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∩ {𝑧}) = ∅ → (𝑥 ⊆ ({𝑧} ∪ 𝐴) ↔ 𝑥 ⊆ 𝐴)) |
26 | 24, 25 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥) → (𝑥 ⊆ ({𝑧} ∪ 𝐴) ↔ 𝑥 ⊆ 𝐴)) |
27 | 21, 26 | mpbid 235 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥) → 𝑥 ⊆ 𝐴) |
28 | | vex 3419 |
. . . . . . . . . . . 12
⊢ 𝑥 ∈ V |
29 | 28 | elpw 4526 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴) |
30 | 27, 29 | sylibr 237 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥) → 𝑥 ∈ 𝒫 𝐴) |
31 | 30 | adantl 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥)) → 𝑥 ∈ 𝒫 𝐴) |
32 | 17, 31 | impbida 801 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝒫 𝐴 ↔ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥))) |
33 | 32 | anbi1d 633 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ 𝒫 𝐴 ∧ (♯‘𝑥) = 𝐾) ↔ ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥) ∧ (♯‘𝑥) = 𝐾))) |
34 | | anass 472 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥) ∧ (♯‘𝑥) = 𝐾) ↔ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾))) |
35 | 33, 34 | bitrdi 290 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ 𝒫 𝐴 ∧ (♯‘𝑥) = 𝐾) ↔ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)))) |
36 | 35 | rabbidva2 3393 |
. . . . 5
⊢ (𝜑 → {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝐾} = {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) |
37 | 36 | fveq2d 6730 |
. . . 4
⊢ (𝜑 → (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝐾}) = (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)})) |
38 | 8, 37 | eqtrd 2778 |
. . 3
⊢ (𝜑 → ((♯‘𝐴)C𝐾) = (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)})) |
39 | | oveq2 7230 |
. . . . . 6
⊢ (𝑗 = (𝐾 − 1) → ((♯‘𝐴)C𝑗) = ((♯‘𝐴)C(𝐾 − 1))) |
40 | | eqeq2 2750 |
. . . . . . . 8
⊢ (𝑗 = (𝐾 − 1) → ((♯‘𝑥) = 𝑗 ↔ (♯‘𝑥) = (𝐾 − 1))) |
41 | 40 | rabbidv 3397 |
. . . . . . 7
⊢ (𝑗 = (𝐾 − 1) → {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑗} = {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)}) |
42 | 41 | fveq2d 6730 |
. . . . . 6
⊢ (𝑗 = (𝐾 − 1) → (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑗}) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)})) |
43 | 39, 42 | eqeq12d 2754 |
. . . . 5
⊢ (𝑗 = (𝐾 − 1) → (((♯‘𝐴)C𝑗) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑗}) ↔ ((♯‘𝐴)C(𝐾 − 1)) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)}))) |
44 | | peano2zm 12233 |
. . . . . 6
⊢ (𝐾 ∈ ℤ → (𝐾 − 1) ∈
ℤ) |
45 | 7, 44 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐾 − 1) ∈ ℤ) |
46 | 43, 6, 45 | rspcdva 3546 |
. . . 4
⊢ (𝜑 → ((♯‘𝐴)C(𝐾 − 1)) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)})) |
47 | | hashbc.1 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ Fin) |
48 | | pwfi 8867 |
. . . . . . . 8
⊢ (𝐴 ∈ Fin ↔ 𝒫
𝐴 ∈
Fin) |
49 | 47, 48 | sylib 221 |
. . . . . . 7
⊢ (𝜑 → 𝒫 𝐴 ∈ Fin) |
50 | | rabexg 5233 |
. . . . . . 7
⊢
(𝒫 𝐴 ∈
Fin → {𝑥 ∈
𝒫 𝐴 ∣
(♯‘𝑥) = (𝐾 − 1)} ∈
V) |
51 | 49, 50 | syl 17 |
. . . . . 6
⊢ (𝜑 → {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ∈ V) |
52 | | snfi 8732 |
. . . . . . . . 9
⊢ {𝑧} ∈ Fin |
53 | | unfi 8861 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Fin ∧ {𝑧} ∈ Fin) → (𝐴 ∪ {𝑧}) ∈ Fin) |
54 | 47, 52, 53 | sylancl 589 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 ∪ {𝑧}) ∈ Fin) |
55 | | pwfi 8867 |
. . . . . . . 8
⊢ ((𝐴 ∪ {𝑧}) ∈ Fin ↔ 𝒫 (𝐴 ∪ {𝑧}) ∈ Fin) |
56 | 54, 55 | sylib 221 |
. . . . . . 7
⊢ (𝜑 → 𝒫 (𝐴 ∪ {𝑧}) ∈ Fin) |
57 | | ssrab2 4002 |
. . . . . . 7
⊢ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ⊆ 𝒫 (𝐴 ∪ {𝑧}) |
58 | | ssfi 8862 |
. . . . . . 7
⊢
((𝒫 (𝐴 ∪
{𝑧}) ∈ Fin ∧
{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ⊆ 𝒫 (𝐴 ∪ {𝑧})) → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ Fin) |
59 | 56, 57, 58 | sylancl 589 |
. . . . . 6
⊢ (𝜑 → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ Fin) |
60 | | fveqeq2 6735 |
. . . . . . . 8
⊢ (𝑥 = 𝑢 → ((♯‘𝑥) = (𝐾 − 1) ↔ (♯‘𝑢) = (𝐾 − 1))) |
61 | 60 | elrab 3609 |
. . . . . . 7
⊢ (𝑢 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ↔ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) |
62 | | eleq2 2827 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑢 ∪ {𝑧}) → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ (𝑢 ∪ {𝑧}))) |
63 | | fveqeq2 6735 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑢 ∪ {𝑧}) → ((♯‘𝑥) = 𝐾 ↔ (♯‘(𝑢 ∪ {𝑧})) = 𝐾)) |
64 | 62, 63 | anbi12d 634 |
. . . . . . . . 9
⊢ (𝑥 = (𝑢 ∪ {𝑧}) → ((𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ↔ (𝑧 ∈ (𝑢 ∪ {𝑧}) ∧ (♯‘(𝑢 ∪ {𝑧})) = 𝐾))) |
65 | | elpwi 4531 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ 𝒫 𝐴 → 𝑢 ⊆ 𝐴) |
66 | 65 | ad2antrl 728 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → 𝑢 ⊆ 𝐴) |
67 | | unss1 4102 |
. . . . . . . . . . 11
⊢ (𝑢 ⊆ 𝐴 → (𝑢 ∪ {𝑧}) ⊆ (𝐴 ∪ {𝑧})) |
68 | 66, 67 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (𝑢 ∪ {𝑧}) ⊆ (𝐴 ∪ {𝑧})) |
69 | | vex 3419 |
. . . . . . . . . . . 12
⊢ 𝑢 ∈ V |
70 | | snex 5333 |
. . . . . . . . . . . 12
⊢ {𝑧} ∈ V |
71 | 69, 70 | unex 7540 |
. . . . . . . . . . 11
⊢ (𝑢 ∪ {𝑧}) ∈ V |
72 | 71 | elpw 4526 |
. . . . . . . . . 10
⊢ ((𝑢 ∪ {𝑧}) ∈ 𝒫 (𝐴 ∪ {𝑧}) ↔ (𝑢 ∪ {𝑧}) ⊆ (𝐴 ∪ {𝑧})) |
73 | 68, 72 | sylibr 237 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (𝑢 ∪ {𝑧}) ∈ 𝒫 (𝐴 ∪ {𝑧})) |
74 | 47 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → 𝐴 ∈ Fin) |
75 | 74, 66 | ssfid 8911 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → 𝑢 ∈ Fin) |
76 | 52 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → {𝑧} ∈ Fin) |
77 | 13 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → ¬ 𝑧 ∈ 𝐴) |
78 | 66, 77 | ssneldd 3913 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → ¬ 𝑧 ∈ 𝑢) |
79 | | disjsn 4636 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑢) |
80 | 78, 79 | sylibr 237 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (𝑢 ∩ {𝑧}) = ∅) |
81 | | hashun 13962 |
. . . . . . . . . . . 12
⊢ ((𝑢 ∈ Fin ∧ {𝑧} ∈ Fin ∧ (𝑢 ∩ {𝑧}) = ∅) → (♯‘(𝑢 ∪ {𝑧})) = ((♯‘𝑢) + (♯‘{𝑧}))) |
82 | 75, 76, 80, 81 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (♯‘(𝑢 ∪ {𝑧})) = ((♯‘𝑢) + (♯‘{𝑧}))) |
83 | | simprr 773 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (♯‘𝑢) = (𝐾 − 1)) |
84 | | hashsng 13949 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ V →
(♯‘{𝑧}) =
1) |
85 | 84 | elv 3421 |
. . . . . . . . . . . . 13
⊢
(♯‘{𝑧})
= 1 |
86 | 85 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (♯‘{𝑧}) = 1) |
87 | 83, 86 | oveq12d 7240 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → ((♯‘𝑢) + (♯‘{𝑧})) = ((𝐾 − 1) + 1)) |
88 | 7 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → 𝐾 ∈ ℤ) |
89 | 88 | zcnd 12296 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → 𝐾 ∈ ℂ) |
90 | | ax-1cn 10800 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℂ |
91 | | npcan 11100 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝐾 −
1) + 1) = 𝐾) |
92 | 89, 90, 91 | sylancl 589 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → ((𝐾 − 1) + 1) = 𝐾) |
93 | 82, 87, 92 | 3eqtrd 2782 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (♯‘(𝑢 ∪ {𝑧})) = 𝐾) |
94 | | ssun2 4096 |
. . . . . . . . . . 11
⊢ {𝑧} ⊆ (𝑢 ∪ {𝑧}) |
95 | | vex 3419 |
. . . . . . . . . . . 12
⊢ 𝑧 ∈ V |
96 | 95 | snss 4708 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ (𝑢 ∪ {𝑧}) ↔ {𝑧} ⊆ (𝑢 ∪ {𝑧})) |
97 | 94, 96 | mpbir 234 |
. . . . . . . . . 10
⊢ 𝑧 ∈ (𝑢 ∪ {𝑧}) |
98 | 93, 97 | jctil 523 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (𝑧 ∈ (𝑢 ∪ {𝑧}) ∧ (♯‘(𝑢 ∪ {𝑧})) = 𝐾)) |
99 | 64, 73, 98 | elrabd 3611 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (𝑢 ∪ {𝑧}) ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) |
100 | 99 | ex 416 |
. . . . . . 7
⊢ (𝜑 → ((𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) → (𝑢 ∪ {𝑧}) ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)})) |
101 | 61, 100 | syl5bi 245 |
. . . . . 6
⊢ (𝜑 → (𝑢 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} → (𝑢 ∪ {𝑧}) ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)})) |
102 | | eleq2 2827 |
. . . . . . . . 9
⊢ (𝑥 = 𝑣 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑣)) |
103 | | fveqeq2 6735 |
. . . . . . . . 9
⊢ (𝑥 = 𝑣 → ((♯‘𝑥) = 𝐾 ↔ (♯‘𝑣) = 𝐾)) |
104 | 102, 103 | anbi12d 634 |
. . . . . . . 8
⊢ (𝑥 = 𝑣 → ((𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ↔ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) |
105 | 104 | elrab 3609 |
. . . . . . 7
⊢ (𝑣 ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ↔ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) |
106 | | fveqeq2 6735 |
. . . . . . . . 9
⊢ (𝑥 = (𝑣 ∖ {𝑧}) → ((♯‘𝑥) = (𝐾 − 1) ↔ (♯‘(𝑣 ∖ {𝑧})) = (𝐾 − 1))) |
107 | | elpwi 4531 |
. . . . . . . . . . . . 13
⊢ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) → 𝑣 ⊆ (𝐴 ∪ {𝑧})) |
108 | 107 | ad2antrl 728 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → 𝑣 ⊆ (𝐴 ∪ {𝑧})) |
109 | 108, 19 | sseqtrdi 3960 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → 𝑣 ⊆ ({𝑧} ∪ 𝐴)) |
110 | | ssundif 4408 |
. . . . . . . . . . 11
⊢ (𝑣 ⊆ ({𝑧} ∪ 𝐴) ↔ (𝑣 ∖ {𝑧}) ⊆ 𝐴) |
111 | 109, 110 | sylib 221 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑣 ∖ {𝑧}) ⊆ 𝐴) |
112 | | vex 3419 |
. . . . . . . . . . . 12
⊢ 𝑣 ∈ V |
113 | 112 | difexi 5230 |
. . . . . . . . . . 11
⊢ (𝑣 ∖ {𝑧}) ∈ V |
114 | 113 | elpw 4526 |
. . . . . . . . . 10
⊢ ((𝑣 ∖ {𝑧}) ∈ 𝒫 𝐴 ↔ (𝑣 ∖ {𝑧}) ⊆ 𝐴) |
115 | 111, 114 | sylibr 237 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑣 ∖ {𝑧}) ∈ 𝒫 𝐴) |
116 | 47 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → 𝐴 ∈ Fin) |
117 | 116, 111 | ssfid 8911 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑣 ∖ {𝑧}) ∈ Fin) |
118 | | hashcl 13936 |
. . . . . . . . . . . . 13
⊢ ((𝑣 ∖ {𝑧}) ∈ Fin → (♯‘(𝑣 ∖ {𝑧})) ∈
ℕ0) |
119 | 117, 118 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (♯‘(𝑣 ∖ {𝑧})) ∈
ℕ0) |
120 | 119 | nn0cnd 12165 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (♯‘(𝑣 ∖ {𝑧})) ∈ ℂ) |
121 | | pncan 11097 |
. . . . . . . . . . 11
⊢
(((♯‘(𝑣
∖ {𝑧})) ∈
ℂ ∧ 1 ∈ ℂ) → (((♯‘(𝑣 ∖ {𝑧})) + 1) − 1) = (♯‘(𝑣 ∖ {𝑧}))) |
122 | 120, 90, 121 | sylancl 589 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (((♯‘(𝑣 ∖ {𝑧})) + 1) − 1) = (♯‘(𝑣 ∖ {𝑧}))) |
123 | | undif1 4399 |
. . . . . . . . . . . . . 14
⊢ ((𝑣 ∖ {𝑧}) ∪ {𝑧}) = (𝑣 ∪ {𝑧}) |
124 | | simprrl 781 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → 𝑧 ∈ 𝑣) |
125 | 124 | snssd 4731 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → {𝑧} ⊆ 𝑣) |
126 | | ssequn2 4106 |
. . . . . . . . . . . . . . 15
⊢ ({𝑧} ⊆ 𝑣 ↔ (𝑣 ∪ {𝑧}) = 𝑣) |
127 | 125, 126 | sylib 221 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑣 ∪ {𝑧}) = 𝑣) |
128 | 123, 127 | eqtrid 2790 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → ((𝑣 ∖ {𝑧}) ∪ {𝑧}) = 𝑣) |
129 | 128 | fveq2d 6730 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (♯‘((𝑣 ∖ {𝑧}) ∪ {𝑧})) = (♯‘𝑣)) |
130 | 52 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → {𝑧} ∈ Fin) |
131 | | disjdifr 4396 |
. . . . . . . . . . . . . . 15
⊢ ((𝑣 ∖ {𝑧}) ∩ {𝑧}) = ∅ |
132 | 131 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → ((𝑣 ∖ {𝑧}) ∩ {𝑧}) = ∅) |
133 | | hashun 13962 |
. . . . . . . . . . . . . 14
⊢ (((𝑣 ∖ {𝑧}) ∈ Fin ∧ {𝑧} ∈ Fin ∧ ((𝑣 ∖ {𝑧}) ∩ {𝑧}) = ∅) → (♯‘((𝑣 ∖ {𝑧}) ∪ {𝑧})) = ((♯‘(𝑣 ∖ {𝑧})) + (♯‘{𝑧}))) |
134 | 117, 130,
132, 133 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (♯‘((𝑣 ∖ {𝑧}) ∪ {𝑧})) = ((♯‘(𝑣 ∖ {𝑧})) + (♯‘{𝑧}))) |
135 | 85 | oveq2i 7233 |
. . . . . . . . . . . . 13
⊢
((♯‘(𝑣
∖ {𝑧})) +
(♯‘{𝑧})) =
((♯‘(𝑣 ∖
{𝑧})) + 1) |
136 | 134, 135 | eqtrdi 2795 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (♯‘((𝑣 ∖ {𝑧}) ∪ {𝑧})) = ((♯‘(𝑣 ∖ {𝑧})) + 1)) |
137 | | simprrr 782 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (♯‘𝑣) = 𝐾) |
138 | 129, 136,
137 | 3eqtr3d 2786 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → ((♯‘(𝑣 ∖ {𝑧})) + 1) = 𝐾) |
139 | 138 | oveq1d 7237 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (((♯‘(𝑣 ∖ {𝑧})) + 1) − 1) = (𝐾 − 1)) |
140 | 122, 139 | eqtr3d 2780 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (♯‘(𝑣 ∖ {𝑧})) = (𝐾 − 1)) |
141 | 106, 115,
140 | elrabd 3611 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑣 ∖ {𝑧}) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)}) |
142 | 141 | ex 416 |
. . . . . . 7
⊢ (𝜑 → ((𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾)) → (𝑣 ∖ {𝑧}) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)})) |
143 | 105, 142 | syl5bi 245 |
. . . . . 6
⊢ (𝜑 → (𝑣 ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} → (𝑣 ∖ {𝑧}) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)})) |
144 | 61, 105 | anbi12i 630 |
. . . . . . 7
⊢ ((𝑢 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ∧ 𝑣 ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) ↔ ((𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾)))) |
145 | | simp3rl 1248 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → 𝑧 ∈ 𝑣) |
146 | 145 | snssd 4731 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → {𝑧} ⊆ 𝑣) |
147 | | incom 4124 |
. . . . . . . . . . . 12
⊢ ({𝑧} ∩ 𝑢) = (𝑢 ∩ {𝑧}) |
148 | 80 | 3adant3 1134 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑢 ∩ {𝑧}) = ∅) |
149 | 147, 148 | eqtrid 2790 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → ({𝑧} ∩ 𝑢) = ∅) |
150 | | uneqdifeq 4413 |
. . . . . . . . . . 11
⊢ (({𝑧} ⊆ 𝑣 ∧ ({𝑧} ∩ 𝑢) = ∅) → (({𝑧} ∪ 𝑢) = 𝑣 ↔ (𝑣 ∖ {𝑧}) = 𝑢)) |
151 | 146, 149,
150 | syl2anc 587 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (({𝑧} ∪ 𝑢) = 𝑣 ↔ (𝑣 ∖ {𝑧}) = 𝑢)) |
152 | 151 | bicomd 226 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → ((𝑣 ∖ {𝑧}) = 𝑢 ↔ ({𝑧} ∪ 𝑢) = 𝑣)) |
153 | | eqcom 2745 |
. . . . . . . . 9
⊢ (𝑢 = (𝑣 ∖ {𝑧}) ↔ (𝑣 ∖ {𝑧}) = 𝑢) |
154 | | eqcom 2745 |
. . . . . . . . . 10
⊢ (𝑣 = (𝑢 ∪ {𝑧}) ↔ (𝑢 ∪ {𝑧}) = 𝑣) |
155 | | uncom 4076 |
. . . . . . . . . . 11
⊢ (𝑢 ∪ {𝑧}) = ({𝑧} ∪ 𝑢) |
156 | 155 | eqeq1i 2743 |
. . . . . . . . . 10
⊢ ((𝑢 ∪ {𝑧}) = 𝑣 ↔ ({𝑧} ∪ 𝑢) = 𝑣) |
157 | 154, 156 | bitri 278 |
. . . . . . . . 9
⊢ (𝑣 = (𝑢 ∪ {𝑧}) ↔ ({𝑧} ∪ 𝑢) = 𝑣) |
158 | 152, 153,
157 | 3bitr4g 317 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑢 = (𝑣 ∖ {𝑧}) ↔ 𝑣 = (𝑢 ∪ {𝑧}))) |
159 | 158 | 3expib 1124 |
. . . . . . 7
⊢ (𝜑 → (((𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑢 = (𝑣 ∖ {𝑧}) ↔ 𝑣 = (𝑢 ∪ {𝑧})))) |
160 | 144, 159 | syl5bi 245 |
. . . . . 6
⊢ (𝜑 → ((𝑢 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ∧ 𝑣 ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) → (𝑢 = (𝑣 ∖ {𝑧}) ↔ 𝑣 = (𝑢 ∪ {𝑧})))) |
161 | 51, 59, 101, 143, 160 | en3d 8676 |
. . . . 5
⊢ (𝜑 → {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ≈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) |
162 | | ssrab2 4002 |
. . . . . . 7
⊢ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ⊆ 𝒫 𝐴 |
163 | | ssfi 8862 |
. . . . . . 7
⊢
((𝒫 𝐴 ∈
Fin ∧ {𝑥 ∈
𝒫 𝐴 ∣
(♯‘𝑥) = (𝐾 − 1)} ⊆ 𝒫
𝐴) → {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ∈ Fin) |
164 | 49, 162, 163 | sylancl 589 |
. . . . . 6
⊢ (𝜑 → {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ∈ Fin) |
165 | | hashen 13926 |
. . . . . 6
⊢ (({𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ∈ Fin ∧ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ Fin) → ((♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)}) = (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) ↔ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ≈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)})) |
166 | 164, 59, 165 | syl2anc 587 |
. . . . 5
⊢ (𝜑 → ((♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)}) = (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) ↔ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ≈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)})) |
167 | 161, 166 | mpbird 260 |
. . . 4
⊢ (𝜑 → (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)}) = (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)})) |
168 | 46, 167 | eqtrd 2778 |
. . 3
⊢ (𝜑 → ((♯‘𝐴)C(𝐾 − 1)) = (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)})) |
169 | 38, 168 | oveq12d 7240 |
. 2
⊢ (𝜑 → (((♯‘𝐴)C𝐾) + ((♯‘𝐴)C(𝐾 − 1))) = ((♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) + (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}))) |
170 | 52 | a1i 11 |
. . . . . 6
⊢ (𝜑 → {𝑧} ∈ Fin) |
171 | | disjsn 4636 |
. . . . . . 7
⊢ ((𝐴 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝐴) |
172 | 13, 171 | sylibr 237 |
. . . . . 6
⊢ (𝜑 → (𝐴 ∩ {𝑧}) = ∅) |
173 | | hashun 13962 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ {𝑧} ∈ Fin ∧ (𝐴 ∩ {𝑧}) = ∅) → (♯‘(𝐴 ∪ {𝑧})) = ((♯‘𝐴) + (♯‘{𝑧}))) |
174 | 47, 170, 172, 173 | syl3anc 1373 |
. . . . 5
⊢ (𝜑 → (♯‘(𝐴 ∪ {𝑧})) = ((♯‘𝐴) + (♯‘{𝑧}))) |
175 | 85 | oveq2i 7233 |
. . . . 5
⊢
((♯‘𝐴) +
(♯‘{𝑧})) =
((♯‘𝐴) +
1) |
176 | 174, 175 | eqtrdi 2795 |
. . . 4
⊢ (𝜑 → (♯‘(𝐴 ∪ {𝑧})) = ((♯‘𝐴) + 1)) |
177 | 176 | oveq1d 7237 |
. . 3
⊢ (𝜑 → ((♯‘(𝐴 ∪ {𝑧}))C𝐾) = (((♯‘𝐴) + 1)C𝐾)) |
178 | | hashcl 13936 |
. . . . 5
⊢ (𝐴 ∈ Fin →
(♯‘𝐴) ∈
ℕ0) |
179 | 47, 178 | syl 17 |
. . . 4
⊢ (𝜑 → (♯‘𝐴) ∈
ℕ0) |
180 | | bcpasc 13900 |
. . . 4
⊢
(((♯‘𝐴)
∈ ℕ0 ∧ 𝐾 ∈ ℤ) →
(((♯‘𝐴)C𝐾) + ((♯‘𝐴)C(𝐾 − 1))) = (((♯‘𝐴) + 1)C𝐾)) |
181 | 179, 7, 180 | syl2anc 587 |
. . 3
⊢ (𝜑 → (((♯‘𝐴)C𝐾) + ((♯‘𝐴)C(𝐾 − 1))) = (((♯‘𝐴) + 1)C𝐾)) |
182 | 177, 181 | eqtr4d 2781 |
. 2
⊢ (𝜑 → ((♯‘(𝐴 ∪ {𝑧}))C𝐾) = (((♯‘𝐴)C𝐾) + ((♯‘𝐴)C(𝐾 − 1)))) |
183 | | pm2.1 897 |
. . . . . . . 8
⊢ (¬
𝑧 ∈ 𝑥 ∨ 𝑧 ∈ 𝑥) |
184 | 183 | biantrur 534 |
. . . . . . 7
⊢
((♯‘𝑥) =
𝐾 ↔ ((¬ 𝑧 ∈ 𝑥 ∨ 𝑧 ∈ 𝑥) ∧ (♯‘𝑥) = 𝐾)) |
185 | | andir 1009 |
. . . . . . 7
⊢ (((¬
𝑧 ∈ 𝑥 ∨ 𝑧 ∈ 𝑥) ∧ (♯‘𝑥) = 𝐾) ↔ ((¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ∨ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾))) |
186 | 184, 185 | bitri 278 |
. . . . . 6
⊢
((♯‘𝑥) =
𝐾 ↔ ((¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ∨ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾))) |
187 | 186 | rabbii 3390 |
. . . . 5
⊢ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (♯‘𝑥) = 𝐾} = {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ∨ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾))} |
188 | | unrab 4229 |
. . . . 5
⊢ ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) = {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ∨ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾))} |
189 | 187, 188 | eqtr4i 2769 |
. . . 4
⊢ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (♯‘𝑥) = 𝐾} = ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) |
190 | 189 | fveq2i 6729 |
. . 3
⊢
(♯‘{𝑥
∈ 𝒫 (𝐴 ∪
{𝑧}) ∣
(♯‘𝑥) = 𝐾}) = (♯‘({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)})) |
191 | | ssrab2 4002 |
. . . . 5
⊢ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ⊆ 𝒫 (𝐴 ∪ {𝑧}) |
192 | | ssfi 8862 |
. . . . 5
⊢
((𝒫 (𝐴 ∪
{𝑧}) ∈ Fin ∧
{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ⊆ 𝒫 (𝐴 ∪ {𝑧})) → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ Fin) |
193 | 56, 191, 192 | sylancl 589 |
. . . 4
⊢ (𝜑 → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ Fin) |
194 | | inrab 4230 |
. . . . . 6
⊢ ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∩ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) = {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾))} |
195 | | simprl 771 |
. . . . . . . . 9
⊢ (((¬
𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)) → 𝑧 ∈ 𝑥) |
196 | | simpll 767 |
. . . . . . . . 9
⊢ (((¬
𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)) → ¬ 𝑧 ∈ 𝑥) |
197 | 195, 196 | pm2.65i 197 |
. . . . . . . 8
⊢ ¬
((¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)) |
198 | 197 | rgenw 3074 |
. . . . . . 7
⊢
∀𝑥 ∈
𝒫 (𝐴 ∪ {𝑧}) ¬ ((¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)) |
199 | | rabeq0 4308 |
. . . . . . 7
⊢ ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾))} = ∅ ↔ ∀𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ¬ ((¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾))) |
200 | 198, 199 | mpbir 234 |
. . . . . 6
⊢ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾))} = ∅ |
201 | 194, 200 | eqtri 2766 |
. . . . 5
⊢ ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∩ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) = ∅ |
202 | 201 | a1i 11 |
. . . 4
⊢ (𝜑 → ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∩ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) = ∅) |
203 | | hashun 13962 |
. . . 4
⊢ (({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ Fin ∧ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ Fin ∧ ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∩ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) = ∅) → (♯‘({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)})) = ((♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) + (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}))) |
204 | 193, 59, 202, 203 | syl3anc 1373 |
. . 3
⊢ (𝜑 → (♯‘({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)})) = ((♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) + (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}))) |
205 | 190, 204 | eqtrid 2790 |
. 2
⊢ (𝜑 → (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (♯‘𝑥) = 𝐾}) = ((♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) + (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}))) |
206 | 169, 182,
205 | 3eqtr4d 2788 |
1
⊢ (𝜑 → ((♯‘(𝐴 ∪ {𝑧}))C𝐾) = (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (♯‘𝑥) = 𝐾})) |