Step | Hyp | Ref
| Expression |
1 | | oveq2 6821 |
. . . . . 6
⊢ (𝑗 = 𝐾 → ((♯‘𝐴)C𝑗) = ((♯‘𝐴)C𝐾)) |
2 | | eqeq2 2771 |
. . . . . . . 8
⊢ (𝑗 = 𝐾 → ((♯‘𝑥) = 𝑗 ↔ (♯‘𝑥) = 𝐾)) |
3 | 2 | rabbidv 3329 |
. . . . . . 7
⊢ (𝑗 = 𝐾 → {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑗} = {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝐾}) |
4 | 3 | fveq2d 6356 |
. . . . . 6
⊢ (𝑗 = 𝐾 → (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑗}) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝐾})) |
5 | 1, 4 | eqeq12d 2775 |
. . . . 5
⊢ (𝑗 = 𝐾 → (((♯‘𝐴)C𝑗) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑗}) ↔ ((♯‘𝐴)C𝐾) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝐾}))) |
6 | | hashbc.3 |
. . . . 5
⊢ (𝜑 → ∀𝑗 ∈ ℤ ((♯‘𝐴)C𝑗) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑗})) |
7 | | hashbc.4 |
. . . . 5
⊢ (𝜑 → 𝐾 ∈ ℤ) |
8 | 5, 6, 7 | rspcdva 3455 |
. . . 4
⊢ (𝜑 → ((♯‘𝐴)C𝐾) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝐾})) |
9 | | ssun1 3919 |
. . . . . . . . . . . . 13
⊢ 𝐴 ⊆ (𝐴 ∪ {𝑧}) |
10 | | sspwb 5066 |
. . . . . . . . . . . . 13
⊢ (𝐴 ⊆ (𝐴 ∪ {𝑧}) ↔ 𝒫 𝐴 ⊆ 𝒫 (𝐴 ∪ {𝑧})) |
11 | 9, 10 | mpbi 220 |
. . . . . . . . . . . 12
⊢ 𝒫
𝐴 ⊆ 𝒫 (𝐴 ∪ {𝑧}) |
12 | 11 | sseli 3740 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧})) |
13 | 12 | adantl 473 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝐴) → 𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧})) |
14 | | hashbc.2 |
. . . . . . . . . . 11
⊢ (𝜑 → ¬ 𝑧 ∈ 𝐴) |
15 | | elpwi 4312 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝒫 𝐴 → 𝑥 ⊆ 𝐴) |
16 | 15 | ssneld 3746 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝒫 𝐴 → (¬ 𝑧 ∈ 𝐴 → ¬ 𝑧 ∈ 𝑥)) |
17 | 14, 16 | mpan9 487 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝐴) → ¬ 𝑧 ∈ 𝑥) |
18 | 13, 17 | jca 555 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝐴) → (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥)) |
19 | | elpwi 4312 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) → 𝑥 ⊆ (𝐴 ∪ {𝑧})) |
20 | | uncom 3900 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∪ {𝑧}) = ({𝑧} ∪ 𝐴) |
21 | 19, 20 | syl6sseq 3792 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) → 𝑥 ⊆ ({𝑧} ∪ 𝐴)) |
22 | 21 | adantr 472 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥) → 𝑥 ⊆ ({𝑧} ∪ 𝐴)) |
23 | | simpr 479 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥) → ¬ 𝑧 ∈ 𝑥) |
24 | | disjsn 4390 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑥) |
25 | 23, 24 | sylibr 224 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥) → (𝑥 ∩ {𝑧}) = ∅) |
26 | | disjssun 4180 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∩ {𝑧}) = ∅ → (𝑥 ⊆ ({𝑧} ∪ 𝐴) ↔ 𝑥 ⊆ 𝐴)) |
27 | 25, 26 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥) → (𝑥 ⊆ ({𝑧} ∪ 𝐴) ↔ 𝑥 ⊆ 𝐴)) |
28 | 22, 27 | mpbid 222 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥) → 𝑥 ⊆ 𝐴) |
29 | | vex 3343 |
. . . . . . . . . . . 12
⊢ 𝑥 ∈ V |
30 | 29 | elpw 4308 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴) |
31 | 28, 30 | sylibr 224 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥) → 𝑥 ∈ 𝒫 𝐴) |
32 | 31 | adantl 473 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥)) → 𝑥 ∈ 𝒫 𝐴) |
33 | 18, 32 | impbida 913 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝒫 𝐴 ↔ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥))) |
34 | 33 | anbi1d 743 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ 𝒫 𝐴 ∧ (♯‘𝑥) = 𝐾) ↔ ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥) ∧ (♯‘𝑥) = 𝐾))) |
35 | | anass 684 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥) ∧ (♯‘𝑥) = 𝐾) ↔ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾))) |
36 | 34, 35 | syl6bb 276 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ 𝒫 𝐴 ∧ (♯‘𝑥) = 𝐾) ↔ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)))) |
37 | 36 | rabbidva2 3326 |
. . . . 5
⊢ (𝜑 → {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝐾} = {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) |
38 | 37 | fveq2d 6356 |
. . . 4
⊢ (𝜑 → (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝐾}) = (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)})) |
39 | 8, 38 | eqtrd 2794 |
. . 3
⊢ (𝜑 → ((♯‘𝐴)C𝐾) = (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)})) |
40 | | oveq2 6821 |
. . . . . 6
⊢ (𝑗 = (𝐾 − 1) → ((♯‘𝐴)C𝑗) = ((♯‘𝐴)C(𝐾 − 1))) |
41 | | eqeq2 2771 |
. . . . . . . 8
⊢ (𝑗 = (𝐾 − 1) → ((♯‘𝑥) = 𝑗 ↔ (♯‘𝑥) = (𝐾 − 1))) |
42 | 41 | rabbidv 3329 |
. . . . . . 7
⊢ (𝑗 = (𝐾 − 1) → {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑗} = {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)}) |
43 | 42 | fveq2d 6356 |
. . . . . 6
⊢ (𝑗 = (𝐾 − 1) → (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑗}) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)})) |
44 | 40, 43 | eqeq12d 2775 |
. . . . 5
⊢ (𝑗 = (𝐾 − 1) → (((♯‘𝐴)C𝑗) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑗}) ↔ ((♯‘𝐴)C(𝐾 − 1)) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)}))) |
45 | | peano2zm 11612 |
. . . . . 6
⊢ (𝐾 ∈ ℤ → (𝐾 − 1) ∈
ℤ) |
46 | 7, 45 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐾 − 1) ∈ ℤ) |
47 | 44, 6, 46 | rspcdva 3455 |
. . . 4
⊢ (𝜑 → ((♯‘𝐴)C(𝐾 − 1)) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)})) |
48 | | hashbc.1 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ Fin) |
49 | | pwfi 8426 |
. . . . . . . 8
⊢ (𝐴 ∈ Fin ↔ 𝒫
𝐴 ∈
Fin) |
50 | 48, 49 | sylib 208 |
. . . . . . 7
⊢ (𝜑 → 𝒫 𝐴 ∈ Fin) |
51 | | rabexg 4963 |
. . . . . . 7
⊢
(𝒫 𝐴 ∈
Fin → {𝑥 ∈
𝒫 𝐴 ∣
(♯‘𝑥) = (𝐾 − 1)} ∈
V) |
52 | 50, 51 | syl 17 |
. . . . . 6
⊢ (𝜑 → {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ∈ V) |
53 | | snfi 8203 |
. . . . . . . . . 10
⊢ {𝑧} ∈ Fin |
54 | | unfi 8392 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ Fin ∧ {𝑧} ∈ Fin) → (𝐴 ∪ {𝑧}) ∈ Fin) |
55 | 48, 53, 54 | sylancl 697 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 ∪ {𝑧}) ∈ Fin) |
56 | | pwfi 8426 |
. . . . . . . . 9
⊢ ((𝐴 ∪ {𝑧}) ∈ Fin ↔ 𝒫 (𝐴 ∪ {𝑧}) ∈ Fin) |
57 | 55, 56 | sylib 208 |
. . . . . . . 8
⊢ (𝜑 → 𝒫 (𝐴 ∪ {𝑧}) ∈ Fin) |
58 | | ssrab2 3828 |
. . . . . . . 8
⊢ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ⊆ 𝒫 (𝐴 ∪ {𝑧}) |
59 | | ssfi 8345 |
. . . . . . . 8
⊢
((𝒫 (𝐴 ∪
{𝑧}) ∈ Fin ∧
{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ⊆ 𝒫 (𝐴 ∪ {𝑧})) → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ Fin) |
60 | 57, 58, 59 | sylancl 697 |
. . . . . . 7
⊢ (𝜑 → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ Fin) |
61 | | elex 3352 |
. . . . . . 7
⊢ ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ Fin → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ V) |
62 | 60, 61 | syl 17 |
. . . . . 6
⊢ (𝜑 → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ V) |
63 | | fveq2 6352 |
. . . . . . . . 9
⊢ (𝑥 = 𝑢 → (♯‘𝑥) = (♯‘𝑢)) |
64 | 63 | eqeq1d 2762 |
. . . . . . . 8
⊢ (𝑥 = 𝑢 → ((♯‘𝑥) = (𝐾 − 1) ↔ (♯‘𝑢) = (𝐾 − 1))) |
65 | 64 | elrab 3504 |
. . . . . . 7
⊢ (𝑢 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ↔ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) |
66 | | elpwi 4312 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ 𝒫 𝐴 → 𝑢 ⊆ 𝐴) |
67 | 66 | ad2antrl 766 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → 𝑢 ⊆ 𝐴) |
68 | | unss1 3925 |
. . . . . . . . . . 11
⊢ (𝑢 ⊆ 𝐴 → (𝑢 ∪ {𝑧}) ⊆ (𝐴 ∪ {𝑧})) |
69 | 67, 68 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (𝑢 ∪ {𝑧}) ⊆ (𝐴 ∪ {𝑧})) |
70 | | vex 3343 |
. . . . . . . . . . . 12
⊢ 𝑢 ∈ V |
71 | | snex 5057 |
. . . . . . . . . . . 12
⊢ {𝑧} ∈ V |
72 | 70, 71 | unex 7121 |
. . . . . . . . . . 11
⊢ (𝑢 ∪ {𝑧}) ∈ V |
73 | 72 | elpw 4308 |
. . . . . . . . . 10
⊢ ((𝑢 ∪ {𝑧}) ∈ 𝒫 (𝐴 ∪ {𝑧}) ↔ (𝑢 ∪ {𝑧}) ⊆ (𝐴 ∪ {𝑧})) |
74 | 69, 73 | sylibr 224 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (𝑢 ∪ {𝑧}) ∈ 𝒫 (𝐴 ∪ {𝑧})) |
75 | 48 | adantr 472 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → 𝐴 ∈ Fin) |
76 | | ssfi 8345 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ Fin ∧ 𝑢 ⊆ 𝐴) → 𝑢 ∈ Fin) |
77 | 75, 67, 76 | syl2anc 696 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → 𝑢 ∈ Fin) |
78 | 53 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → {𝑧} ∈ Fin) |
79 | 14 | adantr 472 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → ¬ 𝑧 ∈ 𝐴) |
80 | 67, 79 | ssneldd 3747 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → ¬ 𝑧 ∈ 𝑢) |
81 | | disjsn 4390 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑢) |
82 | 80, 81 | sylibr 224 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (𝑢 ∩ {𝑧}) = ∅) |
83 | | hashun 13363 |
. . . . . . . . . . . 12
⊢ ((𝑢 ∈ Fin ∧ {𝑧} ∈ Fin ∧ (𝑢 ∩ {𝑧}) = ∅) → (♯‘(𝑢 ∪ {𝑧})) = ((♯‘𝑢) + (♯‘{𝑧}))) |
84 | 77, 78, 82, 83 | syl3anc 1477 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (♯‘(𝑢 ∪ {𝑧})) = ((♯‘𝑢) + (♯‘{𝑧}))) |
85 | | simprr 813 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (♯‘𝑢) = (𝐾 − 1)) |
86 | | vex 3343 |
. . . . . . . . . . . . . 14
⊢ 𝑧 ∈ V |
87 | | hashsng 13351 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ V →
(♯‘{𝑧}) =
1) |
88 | 86, 87 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
(♯‘{𝑧})
= 1 |
89 | 88 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (♯‘{𝑧}) = 1) |
90 | 85, 89 | oveq12d 6831 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → ((♯‘𝑢) + (♯‘{𝑧})) = ((𝐾 − 1) + 1)) |
91 | 7 | adantr 472 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → 𝐾 ∈ ℤ) |
92 | 91 | zcnd 11675 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → 𝐾 ∈ ℂ) |
93 | | ax-1cn 10186 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℂ |
94 | | npcan 10482 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝐾 −
1) + 1) = 𝐾) |
95 | 92, 93, 94 | sylancl 697 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → ((𝐾 − 1) + 1) = 𝐾) |
96 | 84, 90, 95 | 3eqtrd 2798 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (♯‘(𝑢 ∪ {𝑧})) = 𝐾) |
97 | | ssun2 3920 |
. . . . . . . . . . 11
⊢ {𝑧} ⊆ (𝑢 ∪ {𝑧}) |
98 | 86 | snss 4460 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ (𝑢 ∪ {𝑧}) ↔ {𝑧} ⊆ (𝑢 ∪ {𝑧})) |
99 | 97, 98 | mpbir 221 |
. . . . . . . . . 10
⊢ 𝑧 ∈ (𝑢 ∪ {𝑧}) |
100 | 96, 99 | jctil 561 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (𝑧 ∈ (𝑢 ∪ {𝑧}) ∧ (♯‘(𝑢 ∪ {𝑧})) = 𝐾)) |
101 | | eleq2 2828 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑢 ∪ {𝑧}) → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ (𝑢 ∪ {𝑧}))) |
102 | | fveq2 6352 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑢 ∪ {𝑧}) → (♯‘𝑥) = (♯‘(𝑢 ∪ {𝑧}))) |
103 | 102 | eqeq1d 2762 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑢 ∪ {𝑧}) → ((♯‘𝑥) = 𝐾 ↔ (♯‘(𝑢 ∪ {𝑧})) = 𝐾)) |
104 | 101, 103 | anbi12d 749 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑢 ∪ {𝑧}) → ((𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ↔ (𝑧 ∈ (𝑢 ∪ {𝑧}) ∧ (♯‘(𝑢 ∪ {𝑧})) = 𝐾))) |
105 | 104 | elrab 3504 |
. . . . . . . . 9
⊢ ((𝑢 ∪ {𝑧}) ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ↔ ((𝑢 ∪ {𝑧}) ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ (𝑢 ∪ {𝑧}) ∧ (♯‘(𝑢 ∪ {𝑧})) = 𝐾))) |
106 | 74, 100, 105 | sylanbrc 701 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (𝑢 ∪ {𝑧}) ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) |
107 | 106 | ex 449 |
. . . . . . 7
⊢ (𝜑 → ((𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) → (𝑢 ∪ {𝑧}) ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)})) |
108 | 65, 107 | syl5bi 232 |
. . . . . 6
⊢ (𝜑 → (𝑢 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} → (𝑢 ∪ {𝑧}) ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)})) |
109 | | eleq2 2828 |
. . . . . . . . 9
⊢ (𝑥 = 𝑣 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑣)) |
110 | | fveq2 6352 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑣 → (♯‘𝑥) = (♯‘𝑣)) |
111 | 110 | eqeq1d 2762 |
. . . . . . . . 9
⊢ (𝑥 = 𝑣 → ((♯‘𝑥) = 𝐾 ↔ (♯‘𝑣) = 𝐾)) |
112 | 109, 111 | anbi12d 749 |
. . . . . . . 8
⊢ (𝑥 = 𝑣 → ((𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ↔ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) |
113 | 112 | elrab 3504 |
. . . . . . 7
⊢ (𝑣 ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ↔ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) |
114 | | elpwi 4312 |
. . . . . . . . . . . . 13
⊢ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) → 𝑣 ⊆ (𝐴 ∪ {𝑧})) |
115 | 114 | ad2antrl 766 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → 𝑣 ⊆ (𝐴 ∪ {𝑧})) |
116 | 115, 20 | syl6sseq 3792 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → 𝑣 ⊆ ({𝑧} ∪ 𝐴)) |
117 | | ssundif 4196 |
. . . . . . . . . . 11
⊢ (𝑣 ⊆ ({𝑧} ∪ 𝐴) ↔ (𝑣 ∖ {𝑧}) ⊆ 𝐴) |
118 | 116, 117 | sylib 208 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑣 ∖ {𝑧}) ⊆ 𝐴) |
119 | | vex 3343 |
. . . . . . . . . . . 12
⊢ 𝑣 ∈ V |
120 | | difexg 4960 |
. . . . . . . . . . . 12
⊢ (𝑣 ∈ V → (𝑣 ∖ {𝑧}) ∈ V) |
121 | 119, 120 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (𝑣 ∖ {𝑧}) ∈ V |
122 | 121 | elpw 4308 |
. . . . . . . . . 10
⊢ ((𝑣 ∖ {𝑧}) ∈ 𝒫 𝐴 ↔ (𝑣 ∖ {𝑧}) ⊆ 𝐴) |
123 | 118, 122 | sylibr 224 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑣 ∖ {𝑧}) ∈ 𝒫 𝐴) |
124 | 48 | adantr 472 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → 𝐴 ∈ Fin) |
125 | | ssfi 8345 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ Fin ∧ (𝑣 ∖ {𝑧}) ⊆ 𝐴) → (𝑣 ∖ {𝑧}) ∈ Fin) |
126 | 124, 118,
125 | syl2anc 696 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑣 ∖ {𝑧}) ∈ Fin) |
127 | | hashcl 13339 |
. . . . . . . . . . . . 13
⊢ ((𝑣 ∖ {𝑧}) ∈ Fin → (♯‘(𝑣 ∖ {𝑧})) ∈
ℕ0) |
128 | 126, 127 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (♯‘(𝑣 ∖ {𝑧})) ∈
ℕ0) |
129 | 128 | nn0cnd 11545 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (♯‘(𝑣 ∖ {𝑧})) ∈ ℂ) |
130 | | pncan 10479 |
. . . . . . . . . . 11
⊢
(((♯‘(𝑣
∖ {𝑧})) ∈
ℂ ∧ 1 ∈ ℂ) → (((♯‘(𝑣 ∖ {𝑧})) + 1) − 1) = (♯‘(𝑣 ∖ {𝑧}))) |
131 | 129, 93, 130 | sylancl 697 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (((♯‘(𝑣 ∖ {𝑧})) + 1) − 1) = (♯‘(𝑣 ∖ {𝑧}))) |
132 | | undif1 4187 |
. . . . . . . . . . . . . 14
⊢ ((𝑣 ∖ {𝑧}) ∪ {𝑧}) = (𝑣 ∪ {𝑧}) |
133 | | simprrl 823 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → 𝑧 ∈ 𝑣) |
134 | 133 | snssd 4485 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → {𝑧} ⊆ 𝑣) |
135 | | ssequn2 3929 |
. . . . . . . . . . . . . . 15
⊢ ({𝑧} ⊆ 𝑣 ↔ (𝑣 ∪ {𝑧}) = 𝑣) |
136 | 134, 135 | sylib 208 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑣 ∪ {𝑧}) = 𝑣) |
137 | 132, 136 | syl5eq 2806 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → ((𝑣 ∖ {𝑧}) ∪ {𝑧}) = 𝑣) |
138 | 137 | fveq2d 6356 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (♯‘((𝑣 ∖ {𝑧}) ∪ {𝑧})) = (♯‘𝑣)) |
139 | 53 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → {𝑧} ∈ Fin) |
140 | | incom 3948 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑣 ∖ {𝑧}) ∩ {𝑧}) = ({𝑧} ∩ (𝑣 ∖ {𝑧})) |
141 | | disjdif 4184 |
. . . . . . . . . . . . . . . 16
⊢ ({𝑧} ∩ (𝑣 ∖ {𝑧})) = ∅ |
142 | 140, 141 | eqtri 2782 |
. . . . . . . . . . . . . . 15
⊢ ((𝑣 ∖ {𝑧}) ∩ {𝑧}) = ∅ |
143 | 142 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → ((𝑣 ∖ {𝑧}) ∩ {𝑧}) = ∅) |
144 | | hashun 13363 |
. . . . . . . . . . . . . 14
⊢ (((𝑣 ∖ {𝑧}) ∈ Fin ∧ {𝑧} ∈ Fin ∧ ((𝑣 ∖ {𝑧}) ∩ {𝑧}) = ∅) → (♯‘((𝑣 ∖ {𝑧}) ∪ {𝑧})) = ((♯‘(𝑣 ∖ {𝑧})) + (♯‘{𝑧}))) |
145 | 126, 139,
143, 144 | syl3anc 1477 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (♯‘((𝑣 ∖ {𝑧}) ∪ {𝑧})) = ((♯‘(𝑣 ∖ {𝑧})) + (♯‘{𝑧}))) |
146 | 88 | oveq2i 6824 |
. . . . . . . . . . . . 13
⊢
((♯‘(𝑣
∖ {𝑧})) +
(♯‘{𝑧})) =
((♯‘(𝑣 ∖
{𝑧})) + 1) |
147 | 145, 146 | syl6eq 2810 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (♯‘((𝑣 ∖ {𝑧}) ∪ {𝑧})) = ((♯‘(𝑣 ∖ {𝑧})) + 1)) |
148 | | simprrr 824 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (♯‘𝑣) = 𝐾) |
149 | 138, 147,
148 | 3eqtr3d 2802 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → ((♯‘(𝑣 ∖ {𝑧})) + 1) = 𝐾) |
150 | 149 | oveq1d 6828 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (((♯‘(𝑣 ∖ {𝑧})) + 1) − 1) = (𝐾 − 1)) |
151 | 131, 150 | eqtr3d 2796 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (♯‘(𝑣 ∖ {𝑧})) = (𝐾 − 1)) |
152 | | fveq2 6352 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑣 ∖ {𝑧}) → (♯‘𝑥) = (♯‘(𝑣 ∖ {𝑧}))) |
153 | 152 | eqeq1d 2762 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑣 ∖ {𝑧}) → ((♯‘𝑥) = (𝐾 − 1) ↔ (♯‘(𝑣 ∖ {𝑧})) = (𝐾 − 1))) |
154 | 153 | elrab 3504 |
. . . . . . . . 9
⊢ ((𝑣 ∖ {𝑧}) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ↔ ((𝑣 ∖ {𝑧}) ∈ 𝒫 𝐴 ∧ (♯‘(𝑣 ∖ {𝑧})) = (𝐾 − 1))) |
155 | 123, 151,
154 | sylanbrc 701 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑣 ∖ {𝑧}) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)}) |
156 | 155 | ex 449 |
. . . . . . 7
⊢ (𝜑 → ((𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾)) → (𝑣 ∖ {𝑧}) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)})) |
157 | 113, 156 | syl5bi 232 |
. . . . . 6
⊢ (𝜑 → (𝑣 ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} → (𝑣 ∖ {𝑧}) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)})) |
158 | 65, 113 | anbi12i 735 |
. . . . . . 7
⊢ ((𝑢 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ∧ 𝑣 ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) ↔ ((𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾)))) |
159 | | simp3rl 1313 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → 𝑧 ∈ 𝑣) |
160 | 159 | snssd 4485 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → {𝑧} ⊆ 𝑣) |
161 | | incom 3948 |
. . . . . . . . . . . 12
⊢ ({𝑧} ∩ 𝑢) = (𝑢 ∩ {𝑧}) |
162 | 82 | 3adant3 1127 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑢 ∩ {𝑧}) = ∅) |
163 | 161, 162 | syl5eq 2806 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → ({𝑧} ∩ 𝑢) = ∅) |
164 | | uneqdifeq 4201 |
. . . . . . . . . . 11
⊢ (({𝑧} ⊆ 𝑣 ∧ ({𝑧} ∩ 𝑢) = ∅) → (({𝑧} ∪ 𝑢) = 𝑣 ↔ (𝑣 ∖ {𝑧}) = 𝑢)) |
165 | 160, 163,
164 | syl2anc 696 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (({𝑧} ∪ 𝑢) = 𝑣 ↔ (𝑣 ∖ {𝑧}) = 𝑢)) |
166 | 165 | bicomd 213 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → ((𝑣 ∖ {𝑧}) = 𝑢 ↔ ({𝑧} ∪ 𝑢) = 𝑣)) |
167 | | eqcom 2767 |
. . . . . . . . 9
⊢ (𝑢 = (𝑣 ∖ {𝑧}) ↔ (𝑣 ∖ {𝑧}) = 𝑢) |
168 | | eqcom 2767 |
. . . . . . . . . 10
⊢ (𝑣 = (𝑢 ∪ {𝑧}) ↔ (𝑢 ∪ {𝑧}) = 𝑣) |
169 | | uncom 3900 |
. . . . . . . . . . 11
⊢ (𝑢 ∪ {𝑧}) = ({𝑧} ∪ 𝑢) |
170 | 169 | eqeq1i 2765 |
. . . . . . . . . 10
⊢ ((𝑢 ∪ {𝑧}) = 𝑣 ↔ ({𝑧} ∪ 𝑢) = 𝑣) |
171 | 168, 170 | bitri 264 |
. . . . . . . . 9
⊢ (𝑣 = (𝑢 ∪ {𝑧}) ↔ ({𝑧} ∪ 𝑢) = 𝑣) |
172 | 166, 167,
171 | 3bitr4g 303 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑢 = (𝑣 ∖ {𝑧}) ↔ 𝑣 = (𝑢 ∪ {𝑧}))) |
173 | 172 | 3expib 1117 |
. . . . . . 7
⊢ (𝜑 → (((𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑢 = (𝑣 ∖ {𝑧}) ↔ 𝑣 = (𝑢 ∪ {𝑧})))) |
174 | 158, 173 | syl5bi 232 |
. . . . . 6
⊢ (𝜑 → ((𝑢 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ∧ 𝑣 ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) → (𝑢 = (𝑣 ∖ {𝑧}) ↔ 𝑣 = (𝑢 ∪ {𝑧})))) |
175 | 52, 62, 108, 157, 174 | en3d 8158 |
. . . . 5
⊢ (𝜑 → {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ≈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) |
176 | | ssrab2 3828 |
. . . . . . 7
⊢ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ⊆ 𝒫 𝐴 |
177 | | ssfi 8345 |
. . . . . . 7
⊢
((𝒫 𝐴 ∈
Fin ∧ {𝑥 ∈
𝒫 𝐴 ∣
(♯‘𝑥) = (𝐾 − 1)} ⊆ 𝒫
𝐴) → {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ∈ Fin) |
178 | 50, 176, 177 | sylancl 697 |
. . . . . 6
⊢ (𝜑 → {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ∈ Fin) |
179 | | hashen 13329 |
. . . . . 6
⊢ (({𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ∈ Fin ∧ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ Fin) → ((♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)}) = (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) ↔ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ≈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)})) |
180 | 178, 60, 179 | syl2anc 696 |
. . . . 5
⊢ (𝜑 → ((♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)}) = (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) ↔ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ≈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)})) |
181 | 175, 180 | mpbird 247 |
. . . 4
⊢ (𝜑 → (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)}) = (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)})) |
182 | 47, 181 | eqtrd 2794 |
. . 3
⊢ (𝜑 → ((♯‘𝐴)C(𝐾 − 1)) = (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)})) |
183 | 39, 182 | oveq12d 6831 |
. 2
⊢ (𝜑 → (((♯‘𝐴)C𝐾) + ((♯‘𝐴)C(𝐾 − 1))) = ((♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) + (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}))) |
184 | 53 | a1i 11 |
. . . . . 6
⊢ (𝜑 → {𝑧} ∈ Fin) |
185 | | disjsn 4390 |
. . . . . . 7
⊢ ((𝐴 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝐴) |
186 | 14, 185 | sylibr 224 |
. . . . . 6
⊢ (𝜑 → (𝐴 ∩ {𝑧}) = ∅) |
187 | | hashun 13363 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ {𝑧} ∈ Fin ∧ (𝐴 ∩ {𝑧}) = ∅) → (♯‘(𝐴 ∪ {𝑧})) = ((♯‘𝐴) + (♯‘{𝑧}))) |
188 | 48, 184, 186, 187 | syl3anc 1477 |
. . . . 5
⊢ (𝜑 → (♯‘(𝐴 ∪ {𝑧})) = ((♯‘𝐴) + (♯‘{𝑧}))) |
189 | 88 | oveq2i 6824 |
. . . . 5
⊢
((♯‘𝐴) +
(♯‘{𝑧})) =
((♯‘𝐴) +
1) |
190 | 188, 189 | syl6eq 2810 |
. . . 4
⊢ (𝜑 → (♯‘(𝐴 ∪ {𝑧})) = ((♯‘𝐴) + 1)) |
191 | 190 | oveq1d 6828 |
. . 3
⊢ (𝜑 → ((♯‘(𝐴 ∪ {𝑧}))C𝐾) = (((♯‘𝐴) + 1)C𝐾)) |
192 | | hashcl 13339 |
. . . . 5
⊢ (𝐴 ∈ Fin →
(♯‘𝐴) ∈
ℕ0) |
193 | 48, 192 | syl 17 |
. . . 4
⊢ (𝜑 → (♯‘𝐴) ∈
ℕ0) |
194 | | bcpasc 13302 |
. . . 4
⊢
(((♯‘𝐴)
∈ ℕ0 ∧ 𝐾 ∈ ℤ) →
(((♯‘𝐴)C𝐾) + ((♯‘𝐴)C(𝐾 − 1))) = (((♯‘𝐴) + 1)C𝐾)) |
195 | 193, 7, 194 | syl2anc 696 |
. . 3
⊢ (𝜑 → (((♯‘𝐴)C𝐾) + ((♯‘𝐴)C(𝐾 − 1))) = (((♯‘𝐴) + 1)C𝐾)) |
196 | 191, 195 | eqtr4d 2797 |
. 2
⊢ (𝜑 → ((♯‘(𝐴 ∪ {𝑧}))C𝐾) = (((♯‘𝐴)C𝐾) + ((♯‘𝐴)C(𝐾 − 1)))) |
197 | | pm2.1 432 |
. . . . . . . 8
⊢ (¬
𝑧 ∈ 𝑥 ∨ 𝑧 ∈ 𝑥) |
198 | 197 | biantrur 528 |
. . . . . . 7
⊢
((♯‘𝑥) =
𝐾 ↔ ((¬ 𝑧 ∈ 𝑥 ∨ 𝑧 ∈ 𝑥) ∧ (♯‘𝑥) = 𝐾)) |
199 | | andir 948 |
. . . . . . 7
⊢ (((¬
𝑧 ∈ 𝑥 ∨ 𝑧 ∈ 𝑥) ∧ (♯‘𝑥) = 𝐾) ↔ ((¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ∨ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾))) |
200 | 198, 199 | bitri 264 |
. . . . . 6
⊢
((♯‘𝑥) =
𝐾 ↔ ((¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ∨ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾))) |
201 | 200 | rabbii 3325 |
. . . . 5
⊢ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (♯‘𝑥) = 𝐾} = {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ∨ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾))} |
202 | | unrab 4041 |
. . . . 5
⊢ ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) = {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ∨ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾))} |
203 | 201, 202 | eqtr4i 2785 |
. . . 4
⊢ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (♯‘𝑥) = 𝐾} = ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) |
204 | 203 | fveq2i 6355 |
. . 3
⊢
(♯‘{𝑥
∈ 𝒫 (𝐴 ∪
{𝑧}) ∣
(♯‘𝑥) = 𝐾}) = (♯‘({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)})) |
205 | | ssrab2 3828 |
. . . . 5
⊢ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ⊆ 𝒫 (𝐴 ∪ {𝑧}) |
206 | | ssfi 8345 |
. . . . 5
⊢
((𝒫 (𝐴 ∪
{𝑧}) ∈ Fin ∧
{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ⊆ 𝒫 (𝐴 ∪ {𝑧})) → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ Fin) |
207 | 57, 205, 206 | sylancl 697 |
. . . 4
⊢ (𝜑 → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ Fin) |
208 | | inrab 4042 |
. . . . . 6
⊢ ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∩ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) = {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾))} |
209 | | simprl 811 |
. . . . . . . . 9
⊢ (((¬
𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)) → 𝑧 ∈ 𝑥) |
210 | | simpll 807 |
. . . . . . . . 9
⊢ (((¬
𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)) → ¬ 𝑧 ∈ 𝑥) |
211 | 209, 210 | pm2.65i 185 |
. . . . . . . 8
⊢ ¬
((¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)) |
212 | 211 | rgenw 3062 |
. . . . . . 7
⊢
∀𝑥 ∈
𝒫 (𝐴 ∪ {𝑧}) ¬ ((¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)) |
213 | | rabeq0 4100 |
. . . . . . 7
⊢ ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾))} = ∅ ↔ ∀𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ¬ ((¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾))) |
214 | 212, 213 | mpbir 221 |
. . . . . 6
⊢ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾))} = ∅ |
215 | 208, 214 | eqtri 2782 |
. . . . 5
⊢ ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∩ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) = ∅ |
216 | 215 | a1i 11 |
. . . 4
⊢ (𝜑 → ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∩ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) = ∅) |
217 | | hashun 13363 |
. . . 4
⊢ (({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ Fin ∧ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ Fin ∧ ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∩ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) = ∅) → (♯‘({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)})) = ((♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) + (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}))) |
218 | 207, 60, 216, 217 | syl3anc 1477 |
. . 3
⊢ (𝜑 → (♯‘({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)})) = ((♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) + (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}))) |
219 | 204, 218 | syl5eq 2806 |
. 2
⊢ (𝜑 → (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (♯‘𝑥) = 𝐾}) = ((♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) + (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}))) |
220 | 183, 196,
219 | 3eqtr4d 2804 |
1
⊢ (𝜑 → ((♯‘(𝐴 ∪ {𝑧}))C𝐾) = (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (♯‘𝑥) = 𝐾})) |