| Step | Hyp | Ref
| Expression |
| 1 | | oveq2 7439 |
. . . . . 6
⊢ (𝑗 = 𝐾 → ((♯‘𝐴)C𝑗) = ((♯‘𝐴)C𝐾)) |
| 2 | | eqeq2 2749 |
. . . . . . . 8
⊢ (𝑗 = 𝐾 → ((♯‘𝑥) = 𝑗 ↔ (♯‘𝑥) = 𝐾)) |
| 3 | 2 | rabbidv 3444 |
. . . . . . 7
⊢ (𝑗 = 𝐾 → {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑗} = {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝐾}) |
| 4 | 3 | fveq2d 6910 |
. . . . . 6
⊢ (𝑗 = 𝐾 → (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑗}) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝐾})) |
| 5 | 1, 4 | eqeq12d 2753 |
. . . . 5
⊢ (𝑗 = 𝐾 → (((♯‘𝐴)C𝑗) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑗}) ↔ ((♯‘𝐴)C𝐾) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝐾}))) |
| 6 | | hashbc.3 |
. . . . 5
⊢ (𝜑 → ∀𝑗 ∈ ℤ ((♯‘𝐴)C𝑗) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑗})) |
| 7 | | hashbc.4 |
. . . . 5
⊢ (𝜑 → 𝐾 ∈ ℤ) |
| 8 | 5, 6, 7 | rspcdva 3623 |
. . . 4
⊢ (𝜑 → ((♯‘𝐴)C𝐾) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝐾})) |
| 9 | | ssun1 4178 |
. . . . . . . . . . . . 13
⊢ 𝐴 ⊆ (𝐴 ∪ {𝑧}) |
| 10 | 9 | sspwi 4612 |
. . . . . . . . . . . 12
⊢ 𝒫
𝐴 ⊆ 𝒫 (𝐴 ∪ {𝑧}) |
| 11 | 10 | sseli 3979 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧})) |
| 12 | 11 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝐴) → 𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧})) |
| 13 | | hashbc.2 |
. . . . . . . . . . 11
⊢ (𝜑 → ¬ 𝑧 ∈ 𝐴) |
| 14 | | elpwi 4607 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝒫 𝐴 → 𝑥 ⊆ 𝐴) |
| 15 | 14 | ssneld 3985 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝒫 𝐴 → (¬ 𝑧 ∈ 𝐴 → ¬ 𝑧 ∈ 𝑥)) |
| 16 | 13, 15 | mpan9 506 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝐴) → ¬ 𝑧 ∈ 𝑥) |
| 17 | 12, 16 | jca 511 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝐴) → (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥)) |
| 18 | | elpwi 4607 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) → 𝑥 ⊆ (𝐴 ∪ {𝑧})) |
| 19 | | uncom 4158 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∪ {𝑧}) = ({𝑧} ∪ 𝐴) |
| 20 | 18, 19 | sseqtrdi 4024 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) → 𝑥 ⊆ ({𝑧} ∪ 𝐴)) |
| 21 | 20 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥) → 𝑥 ⊆ ({𝑧} ∪ 𝐴)) |
| 22 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥) → ¬ 𝑧 ∈ 𝑥) |
| 23 | | disjsn 4711 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑥) |
| 24 | 22, 23 | sylibr 234 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥) → (𝑥 ∩ {𝑧}) = ∅) |
| 25 | | disjssun 4468 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∩ {𝑧}) = ∅ → (𝑥 ⊆ ({𝑧} ∪ 𝐴) ↔ 𝑥 ⊆ 𝐴)) |
| 26 | 24, 25 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥) → (𝑥 ⊆ ({𝑧} ∪ 𝐴) ↔ 𝑥 ⊆ 𝐴)) |
| 27 | 21, 26 | mpbid 232 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥) → 𝑥 ⊆ 𝐴) |
| 28 | | vex 3484 |
. . . . . . . . . . . 12
⊢ 𝑥 ∈ V |
| 29 | 28 | elpw 4604 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴) |
| 30 | 27, 29 | sylibr 234 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥) → 𝑥 ∈ 𝒫 𝐴) |
| 31 | 30 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥)) → 𝑥 ∈ 𝒫 𝐴) |
| 32 | 17, 31 | impbida 801 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝒫 𝐴 ↔ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥))) |
| 33 | 32 | anbi1d 631 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ 𝒫 𝐴 ∧ (♯‘𝑥) = 𝐾) ↔ ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥) ∧ (♯‘𝑥) = 𝐾))) |
| 34 | | anass 468 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥) ∧ (♯‘𝑥) = 𝐾) ↔ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾))) |
| 35 | 33, 34 | bitrdi 287 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ 𝒫 𝐴 ∧ (♯‘𝑥) = 𝐾) ↔ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)))) |
| 36 | 35 | rabbidva2 3438 |
. . . . 5
⊢ (𝜑 → {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝐾} = {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) |
| 37 | 36 | fveq2d 6910 |
. . . 4
⊢ (𝜑 → (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝐾}) = (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)})) |
| 38 | 8, 37 | eqtrd 2777 |
. . 3
⊢ (𝜑 → ((♯‘𝐴)C𝐾) = (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)})) |
| 39 | | oveq2 7439 |
. . . . . 6
⊢ (𝑗 = (𝐾 − 1) → ((♯‘𝐴)C𝑗) = ((♯‘𝐴)C(𝐾 − 1))) |
| 40 | | eqeq2 2749 |
. . . . . . . 8
⊢ (𝑗 = (𝐾 − 1) → ((♯‘𝑥) = 𝑗 ↔ (♯‘𝑥) = (𝐾 − 1))) |
| 41 | 40 | rabbidv 3444 |
. . . . . . 7
⊢ (𝑗 = (𝐾 − 1) → {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑗} = {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)}) |
| 42 | 41 | fveq2d 6910 |
. . . . . 6
⊢ (𝑗 = (𝐾 − 1) → (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑗}) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)})) |
| 43 | 39, 42 | eqeq12d 2753 |
. . . . 5
⊢ (𝑗 = (𝐾 − 1) → (((♯‘𝐴)C𝑗) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑗}) ↔ ((♯‘𝐴)C(𝐾 − 1)) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)}))) |
| 44 | | peano2zm 12660 |
. . . . . 6
⊢ (𝐾 ∈ ℤ → (𝐾 − 1) ∈
ℤ) |
| 45 | 7, 44 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐾 − 1) ∈ ℤ) |
| 46 | 43, 6, 45 | rspcdva 3623 |
. . . 4
⊢ (𝜑 → ((♯‘𝐴)C(𝐾 − 1)) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)})) |
| 47 | | hashbc.1 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ Fin) |
| 48 | | pwfi 9357 |
. . . . . . . 8
⊢ (𝐴 ∈ Fin ↔ 𝒫
𝐴 ∈
Fin) |
| 49 | 47, 48 | sylib 218 |
. . . . . . 7
⊢ (𝜑 → 𝒫 𝐴 ∈ Fin) |
| 50 | | rabexg 5337 |
. . . . . . 7
⊢
(𝒫 𝐴 ∈
Fin → {𝑥 ∈
𝒫 𝐴 ∣
(♯‘𝑥) = (𝐾 − 1)} ∈
V) |
| 51 | 49, 50 | syl 17 |
. . . . . 6
⊢ (𝜑 → {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ∈ V) |
| 52 | | snfi 9083 |
. . . . . . . . 9
⊢ {𝑧} ∈ Fin |
| 53 | | unfi 9211 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Fin ∧ {𝑧} ∈ Fin) → (𝐴 ∪ {𝑧}) ∈ Fin) |
| 54 | 47, 52, 53 | sylancl 586 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 ∪ {𝑧}) ∈ Fin) |
| 55 | | pwfi 9357 |
. . . . . . . 8
⊢ ((𝐴 ∪ {𝑧}) ∈ Fin ↔ 𝒫 (𝐴 ∪ {𝑧}) ∈ Fin) |
| 56 | 54, 55 | sylib 218 |
. . . . . . 7
⊢ (𝜑 → 𝒫 (𝐴 ∪ {𝑧}) ∈ Fin) |
| 57 | | ssrab2 4080 |
. . . . . . 7
⊢ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ⊆ 𝒫 (𝐴 ∪ {𝑧}) |
| 58 | | ssfi 9213 |
. . . . . . 7
⊢
((𝒫 (𝐴 ∪
{𝑧}) ∈ Fin ∧
{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ⊆ 𝒫 (𝐴 ∪ {𝑧})) → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ Fin) |
| 59 | 56, 57, 58 | sylancl 586 |
. . . . . 6
⊢ (𝜑 → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ Fin) |
| 60 | | fveqeq2 6915 |
. . . . . . . 8
⊢ (𝑥 = 𝑢 → ((♯‘𝑥) = (𝐾 − 1) ↔ (♯‘𝑢) = (𝐾 − 1))) |
| 61 | 60 | elrab 3692 |
. . . . . . 7
⊢ (𝑢 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ↔ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) |
| 62 | | eleq2 2830 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑢 ∪ {𝑧}) → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ (𝑢 ∪ {𝑧}))) |
| 63 | | fveqeq2 6915 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑢 ∪ {𝑧}) → ((♯‘𝑥) = 𝐾 ↔ (♯‘(𝑢 ∪ {𝑧})) = 𝐾)) |
| 64 | 62, 63 | anbi12d 632 |
. . . . . . . . 9
⊢ (𝑥 = (𝑢 ∪ {𝑧}) → ((𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ↔ (𝑧 ∈ (𝑢 ∪ {𝑧}) ∧ (♯‘(𝑢 ∪ {𝑧})) = 𝐾))) |
| 65 | | elpwi 4607 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ 𝒫 𝐴 → 𝑢 ⊆ 𝐴) |
| 66 | 65 | ad2antrl 728 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → 𝑢 ⊆ 𝐴) |
| 67 | | unss1 4185 |
. . . . . . . . . . 11
⊢ (𝑢 ⊆ 𝐴 → (𝑢 ∪ {𝑧}) ⊆ (𝐴 ∪ {𝑧})) |
| 68 | 66, 67 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (𝑢 ∪ {𝑧}) ⊆ (𝐴 ∪ {𝑧})) |
| 69 | | vex 3484 |
. . . . . . . . . . . 12
⊢ 𝑢 ∈ V |
| 70 | | vsnex 5434 |
. . . . . . . . . . . 12
⊢ {𝑧} ∈ V |
| 71 | 69, 70 | unex 7764 |
. . . . . . . . . . 11
⊢ (𝑢 ∪ {𝑧}) ∈ V |
| 72 | 71 | elpw 4604 |
. . . . . . . . . 10
⊢ ((𝑢 ∪ {𝑧}) ∈ 𝒫 (𝐴 ∪ {𝑧}) ↔ (𝑢 ∪ {𝑧}) ⊆ (𝐴 ∪ {𝑧})) |
| 73 | 68, 72 | sylibr 234 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (𝑢 ∪ {𝑧}) ∈ 𝒫 (𝐴 ∪ {𝑧})) |
| 74 | 47 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → 𝐴 ∈ Fin) |
| 75 | 74, 66 | ssfid 9301 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → 𝑢 ∈ Fin) |
| 76 | 52 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → {𝑧} ∈ Fin) |
| 77 | 13 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → ¬ 𝑧 ∈ 𝐴) |
| 78 | 66, 77 | ssneldd 3986 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → ¬ 𝑧 ∈ 𝑢) |
| 79 | | disjsn 4711 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑢) |
| 80 | 78, 79 | sylibr 234 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (𝑢 ∩ {𝑧}) = ∅) |
| 81 | | hashun 14421 |
. . . . . . . . . . . 12
⊢ ((𝑢 ∈ Fin ∧ {𝑧} ∈ Fin ∧ (𝑢 ∩ {𝑧}) = ∅) → (♯‘(𝑢 ∪ {𝑧})) = ((♯‘𝑢) + (♯‘{𝑧}))) |
| 82 | 75, 76, 80, 81 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (♯‘(𝑢 ∪ {𝑧})) = ((♯‘𝑢) + (♯‘{𝑧}))) |
| 83 | | simprr 773 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (♯‘𝑢) = (𝐾 − 1)) |
| 84 | | hashsng 14408 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ V →
(♯‘{𝑧}) =
1) |
| 85 | 84 | elv 3485 |
. . . . . . . . . . . . 13
⊢
(♯‘{𝑧})
= 1 |
| 86 | 85 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (♯‘{𝑧}) = 1) |
| 87 | 83, 86 | oveq12d 7449 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → ((♯‘𝑢) + (♯‘{𝑧})) = ((𝐾 − 1) + 1)) |
| 88 | 7 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → 𝐾 ∈ ℤ) |
| 89 | 88 | zcnd 12723 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → 𝐾 ∈ ℂ) |
| 90 | | ax-1cn 11213 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℂ |
| 91 | | npcan 11517 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝐾 −
1) + 1) = 𝐾) |
| 92 | 89, 90, 91 | sylancl 586 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → ((𝐾 − 1) + 1) = 𝐾) |
| 93 | 82, 87, 92 | 3eqtrd 2781 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (♯‘(𝑢 ∪ {𝑧})) = 𝐾) |
| 94 | | ssun2 4179 |
. . . . . . . . . . 11
⊢ {𝑧} ⊆ (𝑢 ∪ {𝑧}) |
| 95 | | vex 3484 |
. . . . . . . . . . . 12
⊢ 𝑧 ∈ V |
| 96 | 95 | snss 4785 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ (𝑢 ∪ {𝑧}) ↔ {𝑧} ⊆ (𝑢 ∪ {𝑧})) |
| 97 | 94, 96 | mpbir 231 |
. . . . . . . . . 10
⊢ 𝑧 ∈ (𝑢 ∪ {𝑧}) |
| 98 | 93, 97 | jctil 519 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (𝑧 ∈ (𝑢 ∪ {𝑧}) ∧ (♯‘(𝑢 ∪ {𝑧})) = 𝐾)) |
| 99 | 64, 73, 98 | elrabd 3694 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (𝑢 ∪ {𝑧}) ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) |
| 100 | 99 | ex 412 |
. . . . . . 7
⊢ (𝜑 → ((𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) → (𝑢 ∪ {𝑧}) ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)})) |
| 101 | 61, 100 | biimtrid 242 |
. . . . . 6
⊢ (𝜑 → (𝑢 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} → (𝑢 ∪ {𝑧}) ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)})) |
| 102 | | eleq2 2830 |
. . . . . . . . 9
⊢ (𝑥 = 𝑣 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑣)) |
| 103 | | fveqeq2 6915 |
. . . . . . . . 9
⊢ (𝑥 = 𝑣 → ((♯‘𝑥) = 𝐾 ↔ (♯‘𝑣) = 𝐾)) |
| 104 | 102, 103 | anbi12d 632 |
. . . . . . . 8
⊢ (𝑥 = 𝑣 → ((𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ↔ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) |
| 105 | 104 | elrab 3692 |
. . . . . . 7
⊢ (𝑣 ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ↔ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) |
| 106 | | fveqeq2 6915 |
. . . . . . . . 9
⊢ (𝑥 = (𝑣 ∖ {𝑧}) → ((♯‘𝑥) = (𝐾 − 1) ↔ (♯‘(𝑣 ∖ {𝑧})) = (𝐾 − 1))) |
| 107 | | elpwi 4607 |
. . . . . . . . . . . . 13
⊢ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) → 𝑣 ⊆ (𝐴 ∪ {𝑧})) |
| 108 | 107 | ad2antrl 728 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → 𝑣 ⊆ (𝐴 ∪ {𝑧})) |
| 109 | 108, 19 | sseqtrdi 4024 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → 𝑣 ⊆ ({𝑧} ∪ 𝐴)) |
| 110 | | ssundif 4488 |
. . . . . . . . . . 11
⊢ (𝑣 ⊆ ({𝑧} ∪ 𝐴) ↔ (𝑣 ∖ {𝑧}) ⊆ 𝐴) |
| 111 | 109, 110 | sylib 218 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑣 ∖ {𝑧}) ⊆ 𝐴) |
| 112 | | vex 3484 |
. . . . . . . . . . . 12
⊢ 𝑣 ∈ V |
| 113 | 112 | difexi 5330 |
. . . . . . . . . . 11
⊢ (𝑣 ∖ {𝑧}) ∈ V |
| 114 | 113 | elpw 4604 |
. . . . . . . . . 10
⊢ ((𝑣 ∖ {𝑧}) ∈ 𝒫 𝐴 ↔ (𝑣 ∖ {𝑧}) ⊆ 𝐴) |
| 115 | 111, 114 | sylibr 234 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑣 ∖ {𝑧}) ∈ 𝒫 𝐴) |
| 116 | 47 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → 𝐴 ∈ Fin) |
| 117 | 116, 111 | ssfid 9301 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑣 ∖ {𝑧}) ∈ Fin) |
| 118 | | hashcl 14395 |
. . . . . . . . . . . . 13
⊢ ((𝑣 ∖ {𝑧}) ∈ Fin → (♯‘(𝑣 ∖ {𝑧})) ∈
ℕ0) |
| 119 | 117, 118 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (♯‘(𝑣 ∖ {𝑧})) ∈
ℕ0) |
| 120 | 119 | nn0cnd 12589 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (♯‘(𝑣 ∖ {𝑧})) ∈ ℂ) |
| 121 | | pncan 11514 |
. . . . . . . . . . 11
⊢
(((♯‘(𝑣
∖ {𝑧})) ∈
ℂ ∧ 1 ∈ ℂ) → (((♯‘(𝑣 ∖ {𝑧})) + 1) − 1) = (♯‘(𝑣 ∖ {𝑧}))) |
| 122 | 120, 90, 121 | sylancl 586 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (((♯‘(𝑣 ∖ {𝑧})) + 1) − 1) = (♯‘(𝑣 ∖ {𝑧}))) |
| 123 | | undif1 4476 |
. . . . . . . . . . . . . 14
⊢ ((𝑣 ∖ {𝑧}) ∪ {𝑧}) = (𝑣 ∪ {𝑧}) |
| 124 | | simprrl 781 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → 𝑧 ∈ 𝑣) |
| 125 | 124 | snssd 4809 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → {𝑧} ⊆ 𝑣) |
| 126 | | ssequn2 4189 |
. . . . . . . . . . . . . . 15
⊢ ({𝑧} ⊆ 𝑣 ↔ (𝑣 ∪ {𝑧}) = 𝑣) |
| 127 | 125, 126 | sylib 218 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑣 ∪ {𝑧}) = 𝑣) |
| 128 | 123, 127 | eqtrid 2789 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → ((𝑣 ∖ {𝑧}) ∪ {𝑧}) = 𝑣) |
| 129 | 128 | fveq2d 6910 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (♯‘((𝑣 ∖ {𝑧}) ∪ {𝑧})) = (♯‘𝑣)) |
| 130 | 52 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → {𝑧} ∈ Fin) |
| 131 | | disjdifr 4473 |
. . . . . . . . . . . . . . 15
⊢ ((𝑣 ∖ {𝑧}) ∩ {𝑧}) = ∅ |
| 132 | 131 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → ((𝑣 ∖ {𝑧}) ∩ {𝑧}) = ∅) |
| 133 | | hashun 14421 |
. . . . . . . . . . . . . 14
⊢ (((𝑣 ∖ {𝑧}) ∈ Fin ∧ {𝑧} ∈ Fin ∧ ((𝑣 ∖ {𝑧}) ∩ {𝑧}) = ∅) → (♯‘((𝑣 ∖ {𝑧}) ∪ {𝑧})) = ((♯‘(𝑣 ∖ {𝑧})) + (♯‘{𝑧}))) |
| 134 | 117, 130,
132, 133 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (♯‘((𝑣 ∖ {𝑧}) ∪ {𝑧})) = ((♯‘(𝑣 ∖ {𝑧})) + (♯‘{𝑧}))) |
| 135 | 85 | oveq2i 7442 |
. . . . . . . . . . . . 13
⊢
((♯‘(𝑣
∖ {𝑧})) +
(♯‘{𝑧})) =
((♯‘(𝑣 ∖
{𝑧})) + 1) |
| 136 | 134, 135 | eqtrdi 2793 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (♯‘((𝑣 ∖ {𝑧}) ∪ {𝑧})) = ((♯‘(𝑣 ∖ {𝑧})) + 1)) |
| 137 | | simprrr 782 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (♯‘𝑣) = 𝐾) |
| 138 | 129, 136,
137 | 3eqtr3d 2785 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → ((♯‘(𝑣 ∖ {𝑧})) + 1) = 𝐾) |
| 139 | 138 | oveq1d 7446 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (((♯‘(𝑣 ∖ {𝑧})) + 1) − 1) = (𝐾 − 1)) |
| 140 | 122, 139 | eqtr3d 2779 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (♯‘(𝑣 ∖ {𝑧})) = (𝐾 − 1)) |
| 141 | 106, 115,
140 | elrabd 3694 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑣 ∖ {𝑧}) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)}) |
| 142 | 141 | ex 412 |
. . . . . . 7
⊢ (𝜑 → ((𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾)) → (𝑣 ∖ {𝑧}) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)})) |
| 143 | 105, 142 | biimtrid 242 |
. . . . . 6
⊢ (𝜑 → (𝑣 ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} → (𝑣 ∖ {𝑧}) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)})) |
| 144 | 61, 105 | anbi12i 628 |
. . . . . . 7
⊢ ((𝑢 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ∧ 𝑣 ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) ↔ ((𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾)))) |
| 145 | | simp3rl 1247 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → 𝑧 ∈ 𝑣) |
| 146 | 145 | snssd 4809 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → {𝑧} ⊆ 𝑣) |
| 147 | | incom 4209 |
. . . . . . . . . . . 12
⊢ ({𝑧} ∩ 𝑢) = (𝑢 ∩ {𝑧}) |
| 148 | 80 | 3adant3 1133 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑢 ∩ {𝑧}) = ∅) |
| 149 | 147, 148 | eqtrid 2789 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → ({𝑧} ∩ 𝑢) = ∅) |
| 150 | | uneqdifeq 4493 |
. . . . . . . . . . 11
⊢ (({𝑧} ⊆ 𝑣 ∧ ({𝑧} ∩ 𝑢) = ∅) → (({𝑧} ∪ 𝑢) = 𝑣 ↔ (𝑣 ∖ {𝑧}) = 𝑢)) |
| 151 | 146, 149,
150 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (({𝑧} ∪ 𝑢) = 𝑣 ↔ (𝑣 ∖ {𝑧}) = 𝑢)) |
| 152 | 151 | bicomd 223 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → ((𝑣 ∖ {𝑧}) = 𝑢 ↔ ({𝑧} ∪ 𝑢) = 𝑣)) |
| 153 | | eqcom 2744 |
. . . . . . . . 9
⊢ (𝑢 = (𝑣 ∖ {𝑧}) ↔ (𝑣 ∖ {𝑧}) = 𝑢) |
| 154 | | eqcom 2744 |
. . . . . . . . . 10
⊢ (𝑣 = (𝑢 ∪ {𝑧}) ↔ (𝑢 ∪ {𝑧}) = 𝑣) |
| 155 | | uncom 4158 |
. . . . . . . . . . 11
⊢ (𝑢 ∪ {𝑧}) = ({𝑧} ∪ 𝑢) |
| 156 | 155 | eqeq1i 2742 |
. . . . . . . . . 10
⊢ ((𝑢 ∪ {𝑧}) = 𝑣 ↔ ({𝑧} ∪ 𝑢) = 𝑣) |
| 157 | 154, 156 | bitri 275 |
. . . . . . . . 9
⊢ (𝑣 = (𝑢 ∪ {𝑧}) ↔ ({𝑧} ∪ 𝑢) = 𝑣) |
| 158 | 152, 153,
157 | 3bitr4g 314 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑢 = (𝑣 ∖ {𝑧}) ↔ 𝑣 = (𝑢 ∪ {𝑧}))) |
| 159 | 158 | 3expib 1123 |
. . . . . . 7
⊢ (𝜑 → (((𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑢 = (𝑣 ∖ {𝑧}) ↔ 𝑣 = (𝑢 ∪ {𝑧})))) |
| 160 | 144, 159 | biimtrid 242 |
. . . . . 6
⊢ (𝜑 → ((𝑢 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ∧ 𝑣 ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) → (𝑢 = (𝑣 ∖ {𝑧}) ↔ 𝑣 = (𝑢 ∪ {𝑧})))) |
| 161 | 51, 59, 101, 143, 160 | en3d 9029 |
. . . . 5
⊢ (𝜑 → {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ≈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) |
| 162 | | ssrab2 4080 |
. . . . . . 7
⊢ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ⊆ 𝒫 𝐴 |
| 163 | | ssfi 9213 |
. . . . . . 7
⊢
((𝒫 𝐴 ∈
Fin ∧ {𝑥 ∈
𝒫 𝐴 ∣
(♯‘𝑥) = (𝐾 − 1)} ⊆ 𝒫
𝐴) → {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ∈ Fin) |
| 164 | 49, 162, 163 | sylancl 586 |
. . . . . 6
⊢ (𝜑 → {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ∈ Fin) |
| 165 | | hashen 14386 |
. . . . . 6
⊢ (({𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ∈ Fin ∧ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ Fin) → ((♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)}) = (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) ↔ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ≈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)})) |
| 166 | 164, 59, 165 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → ((♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)}) = (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) ↔ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ≈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)})) |
| 167 | 161, 166 | mpbird 257 |
. . . 4
⊢ (𝜑 → (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)}) = (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)})) |
| 168 | 46, 167 | eqtrd 2777 |
. . 3
⊢ (𝜑 → ((♯‘𝐴)C(𝐾 − 1)) = (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)})) |
| 169 | 38, 168 | oveq12d 7449 |
. 2
⊢ (𝜑 → (((♯‘𝐴)C𝐾) + ((♯‘𝐴)C(𝐾 − 1))) = ((♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) + (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}))) |
| 170 | 52 | a1i 11 |
. . . . . 6
⊢ (𝜑 → {𝑧} ∈ Fin) |
| 171 | | disjsn 4711 |
. . . . . . 7
⊢ ((𝐴 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝐴) |
| 172 | 13, 171 | sylibr 234 |
. . . . . 6
⊢ (𝜑 → (𝐴 ∩ {𝑧}) = ∅) |
| 173 | | hashun 14421 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ {𝑧} ∈ Fin ∧ (𝐴 ∩ {𝑧}) = ∅) → (♯‘(𝐴 ∪ {𝑧})) = ((♯‘𝐴) + (♯‘{𝑧}))) |
| 174 | 47, 170, 172, 173 | syl3anc 1373 |
. . . . 5
⊢ (𝜑 → (♯‘(𝐴 ∪ {𝑧})) = ((♯‘𝐴) + (♯‘{𝑧}))) |
| 175 | 85 | oveq2i 7442 |
. . . . 5
⊢
((♯‘𝐴) +
(♯‘{𝑧})) =
((♯‘𝐴) +
1) |
| 176 | 174, 175 | eqtrdi 2793 |
. . . 4
⊢ (𝜑 → (♯‘(𝐴 ∪ {𝑧})) = ((♯‘𝐴) + 1)) |
| 177 | 176 | oveq1d 7446 |
. . 3
⊢ (𝜑 → ((♯‘(𝐴 ∪ {𝑧}))C𝐾) = (((♯‘𝐴) + 1)C𝐾)) |
| 178 | | hashcl 14395 |
. . . . 5
⊢ (𝐴 ∈ Fin →
(♯‘𝐴) ∈
ℕ0) |
| 179 | 47, 178 | syl 17 |
. . . 4
⊢ (𝜑 → (♯‘𝐴) ∈
ℕ0) |
| 180 | | bcpasc 14360 |
. . . 4
⊢
(((♯‘𝐴)
∈ ℕ0 ∧ 𝐾 ∈ ℤ) →
(((♯‘𝐴)C𝐾) + ((♯‘𝐴)C(𝐾 − 1))) = (((♯‘𝐴) + 1)C𝐾)) |
| 181 | 179, 7, 180 | syl2anc 584 |
. . 3
⊢ (𝜑 → (((♯‘𝐴)C𝐾) + ((♯‘𝐴)C(𝐾 − 1))) = (((♯‘𝐴) + 1)C𝐾)) |
| 182 | 177, 181 | eqtr4d 2780 |
. 2
⊢ (𝜑 → ((♯‘(𝐴 ∪ {𝑧}))C𝐾) = (((♯‘𝐴)C𝐾) + ((♯‘𝐴)C(𝐾 − 1)))) |
| 183 | | pm2.1 897 |
. . . . . . . 8
⊢ (¬
𝑧 ∈ 𝑥 ∨ 𝑧 ∈ 𝑥) |
| 184 | 183 | biantrur 530 |
. . . . . . 7
⊢
((♯‘𝑥) =
𝐾 ↔ ((¬ 𝑧 ∈ 𝑥 ∨ 𝑧 ∈ 𝑥) ∧ (♯‘𝑥) = 𝐾)) |
| 185 | | andir 1011 |
. . . . . . 7
⊢ (((¬
𝑧 ∈ 𝑥 ∨ 𝑧 ∈ 𝑥) ∧ (♯‘𝑥) = 𝐾) ↔ ((¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ∨ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾))) |
| 186 | 184, 185 | bitri 275 |
. . . . . 6
⊢
((♯‘𝑥) =
𝐾 ↔ ((¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ∨ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾))) |
| 187 | 186 | rabbii 3442 |
. . . . 5
⊢ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (♯‘𝑥) = 𝐾} = {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ∨ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾))} |
| 188 | | unrab 4315 |
. . . . 5
⊢ ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) = {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ∨ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾))} |
| 189 | 187, 188 | eqtr4i 2768 |
. . . 4
⊢ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (♯‘𝑥) = 𝐾} = ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) |
| 190 | 189 | fveq2i 6909 |
. . 3
⊢
(♯‘{𝑥
∈ 𝒫 (𝐴 ∪
{𝑧}) ∣
(♯‘𝑥) = 𝐾}) = (♯‘({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)})) |
| 191 | | ssrab2 4080 |
. . . . 5
⊢ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ⊆ 𝒫 (𝐴 ∪ {𝑧}) |
| 192 | | ssfi 9213 |
. . . . 5
⊢
((𝒫 (𝐴 ∪
{𝑧}) ∈ Fin ∧
{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ⊆ 𝒫 (𝐴 ∪ {𝑧})) → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ Fin) |
| 193 | 56, 191, 192 | sylancl 586 |
. . . 4
⊢ (𝜑 → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ Fin) |
| 194 | | inrab 4316 |
. . . . . 6
⊢ ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∩ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) = {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾))} |
| 195 | | simprl 771 |
. . . . . . . . 9
⊢ (((¬
𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)) → 𝑧 ∈ 𝑥) |
| 196 | | simpll 767 |
. . . . . . . . 9
⊢ (((¬
𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)) → ¬ 𝑧 ∈ 𝑥) |
| 197 | 195, 196 | pm2.65i 194 |
. . . . . . . 8
⊢ ¬
((¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)) |
| 198 | 197 | rgenw 3065 |
. . . . . . 7
⊢
∀𝑥 ∈
𝒫 (𝐴 ∪ {𝑧}) ¬ ((¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)) |
| 199 | | rabeq0 4388 |
. . . . . . 7
⊢ ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾))} = ∅ ↔ ∀𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ¬ ((¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾))) |
| 200 | 198, 199 | mpbir 231 |
. . . . . 6
⊢ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾))} = ∅ |
| 201 | 194, 200 | eqtri 2765 |
. . . . 5
⊢ ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∩ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) = ∅ |
| 202 | 201 | a1i 11 |
. . . 4
⊢ (𝜑 → ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∩ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) = ∅) |
| 203 | | hashun 14421 |
. . . 4
⊢ (({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ Fin ∧ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ Fin ∧ ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∩ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) = ∅) → (♯‘({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)})) = ((♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) + (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}))) |
| 204 | 193, 59, 202, 203 | syl3anc 1373 |
. . 3
⊢ (𝜑 → (♯‘({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)})) = ((♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) + (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}))) |
| 205 | 190, 204 | eqtrid 2789 |
. 2
⊢ (𝜑 → (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (♯‘𝑥) = 𝐾}) = ((♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) + (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}))) |
| 206 | 169, 182,
205 | 3eqtr4d 2787 |
1
⊢ (𝜑 → ((♯‘(𝐴 ∪ {𝑧}))C𝐾) = (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (♯‘𝑥) = 𝐾})) |