Step | Hyp | Ref
| Expression |
1 | | oveq2 6932 |
. . . . . 6
⊢ (𝑗 = 𝐾 → ((♯‘𝐴)C𝑗) = ((♯‘𝐴)C𝐾)) |
2 | | eqeq2 2789 |
. . . . . . . 8
⊢ (𝑗 = 𝐾 → ((♯‘𝑥) = 𝑗 ↔ (♯‘𝑥) = 𝐾)) |
3 | 2 | rabbidv 3386 |
. . . . . . 7
⊢ (𝑗 = 𝐾 → {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑗} = {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝐾}) |
4 | 3 | fveq2d 6452 |
. . . . . 6
⊢ (𝑗 = 𝐾 → (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑗}) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝐾})) |
5 | 1, 4 | eqeq12d 2793 |
. . . . 5
⊢ (𝑗 = 𝐾 → (((♯‘𝐴)C𝑗) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑗}) ↔ ((♯‘𝐴)C𝐾) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝐾}))) |
6 | | hashbc.3 |
. . . . 5
⊢ (𝜑 → ∀𝑗 ∈ ℤ ((♯‘𝐴)C𝑗) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑗})) |
7 | | hashbc.4 |
. . . . 5
⊢ (𝜑 → 𝐾 ∈ ℤ) |
8 | 5, 6, 7 | rspcdva 3517 |
. . . 4
⊢ (𝜑 → ((♯‘𝐴)C𝐾) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝐾})) |
9 | | ssun1 3999 |
. . . . . . . . . . . . 13
⊢ 𝐴 ⊆ (𝐴 ∪ {𝑧}) |
10 | | sspwb 5151 |
. . . . . . . . . . . . 13
⊢ (𝐴 ⊆ (𝐴 ∪ {𝑧}) ↔ 𝒫 𝐴 ⊆ 𝒫 (𝐴 ∪ {𝑧})) |
11 | 9, 10 | mpbi 222 |
. . . . . . . . . . . 12
⊢ 𝒫
𝐴 ⊆ 𝒫 (𝐴 ∪ {𝑧}) |
12 | 11 | sseli 3817 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧})) |
13 | 12 | adantl 475 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝐴) → 𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧})) |
14 | | hashbc.2 |
. . . . . . . . . . 11
⊢ (𝜑 → ¬ 𝑧 ∈ 𝐴) |
15 | | elpwi 4389 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝒫 𝐴 → 𝑥 ⊆ 𝐴) |
16 | 15 | ssneld 3823 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝒫 𝐴 → (¬ 𝑧 ∈ 𝐴 → ¬ 𝑧 ∈ 𝑥)) |
17 | 14, 16 | mpan9 502 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝐴) → ¬ 𝑧 ∈ 𝑥) |
18 | 13, 17 | jca 507 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝐴) → (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥)) |
19 | | elpwi 4389 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) → 𝑥 ⊆ (𝐴 ∪ {𝑧})) |
20 | | uncom 3980 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∪ {𝑧}) = ({𝑧} ∪ 𝐴) |
21 | 19, 20 | syl6sseq 3870 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) → 𝑥 ⊆ ({𝑧} ∪ 𝐴)) |
22 | 21 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥) → 𝑥 ⊆ ({𝑧} ∪ 𝐴)) |
23 | | simpr 479 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥) → ¬ 𝑧 ∈ 𝑥) |
24 | | disjsn 4478 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑥) |
25 | 23, 24 | sylibr 226 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥) → (𝑥 ∩ {𝑧}) = ∅) |
26 | | disjssun 4260 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∩ {𝑧}) = ∅ → (𝑥 ⊆ ({𝑧} ∪ 𝐴) ↔ 𝑥 ⊆ 𝐴)) |
27 | 25, 26 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥) → (𝑥 ⊆ ({𝑧} ∪ 𝐴) ↔ 𝑥 ⊆ 𝐴)) |
28 | 22, 27 | mpbid 224 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥) → 𝑥 ⊆ 𝐴) |
29 | | vex 3401 |
. . . . . . . . . . . 12
⊢ 𝑥 ∈ V |
30 | 29 | elpw 4385 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴) |
31 | 28, 30 | sylibr 226 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥) → 𝑥 ∈ 𝒫 𝐴) |
32 | 31 | adantl 475 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥)) → 𝑥 ∈ 𝒫 𝐴) |
33 | 18, 32 | impbida 791 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝒫 𝐴 ↔ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥))) |
34 | 33 | anbi1d 623 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ 𝒫 𝐴 ∧ (♯‘𝑥) = 𝐾) ↔ ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥) ∧ (♯‘𝑥) = 𝐾))) |
35 | | anass 462 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥) ∧ (♯‘𝑥) = 𝐾) ↔ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾))) |
36 | 34, 35 | syl6bb 279 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ 𝒫 𝐴 ∧ (♯‘𝑥) = 𝐾) ↔ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)))) |
37 | 36 | rabbidva2 3383 |
. . . . 5
⊢ (𝜑 → {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝐾} = {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) |
38 | 37 | fveq2d 6452 |
. . . 4
⊢ (𝜑 → (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝐾}) = (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)})) |
39 | 8, 38 | eqtrd 2814 |
. . 3
⊢ (𝜑 → ((♯‘𝐴)C𝐾) = (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)})) |
40 | | oveq2 6932 |
. . . . . 6
⊢ (𝑗 = (𝐾 − 1) → ((♯‘𝐴)C𝑗) = ((♯‘𝐴)C(𝐾 − 1))) |
41 | | eqeq2 2789 |
. . . . . . . 8
⊢ (𝑗 = (𝐾 − 1) → ((♯‘𝑥) = 𝑗 ↔ (♯‘𝑥) = (𝐾 − 1))) |
42 | 41 | rabbidv 3386 |
. . . . . . 7
⊢ (𝑗 = (𝐾 − 1) → {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑗} = {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)}) |
43 | 42 | fveq2d 6452 |
. . . . . 6
⊢ (𝑗 = (𝐾 − 1) → (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑗}) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)})) |
44 | 40, 43 | eqeq12d 2793 |
. . . . 5
⊢ (𝑗 = (𝐾 − 1) → (((♯‘𝐴)C𝑗) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑗}) ↔ ((♯‘𝐴)C(𝐾 − 1)) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)}))) |
45 | | peano2zm 11776 |
. . . . . 6
⊢ (𝐾 ∈ ℤ → (𝐾 − 1) ∈
ℤ) |
46 | 7, 45 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐾 − 1) ∈ ℤ) |
47 | 44, 6, 46 | rspcdva 3517 |
. . . 4
⊢ (𝜑 → ((♯‘𝐴)C(𝐾 − 1)) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)})) |
48 | | hashbc.1 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ Fin) |
49 | | pwfi 8551 |
. . . . . . . 8
⊢ (𝐴 ∈ Fin ↔ 𝒫
𝐴 ∈
Fin) |
50 | 48, 49 | sylib 210 |
. . . . . . 7
⊢ (𝜑 → 𝒫 𝐴 ∈ Fin) |
51 | | rabexg 5050 |
. . . . . . 7
⊢
(𝒫 𝐴 ∈
Fin → {𝑥 ∈
𝒫 𝐴 ∣
(♯‘𝑥) = (𝐾 − 1)} ∈
V) |
52 | 50, 51 | syl 17 |
. . . . . 6
⊢ (𝜑 → {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ∈ V) |
53 | | snfi 8328 |
. . . . . . . . . 10
⊢ {𝑧} ∈ Fin |
54 | | unfi 8517 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ Fin ∧ {𝑧} ∈ Fin) → (𝐴 ∪ {𝑧}) ∈ Fin) |
55 | 48, 53, 54 | sylancl 580 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 ∪ {𝑧}) ∈ Fin) |
56 | | pwfi 8551 |
. . . . . . . . 9
⊢ ((𝐴 ∪ {𝑧}) ∈ Fin ↔ 𝒫 (𝐴 ∪ {𝑧}) ∈ Fin) |
57 | 55, 56 | sylib 210 |
. . . . . . . 8
⊢ (𝜑 → 𝒫 (𝐴 ∪ {𝑧}) ∈ Fin) |
58 | | ssrab2 3908 |
. . . . . . . 8
⊢ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ⊆ 𝒫 (𝐴 ∪ {𝑧}) |
59 | | ssfi 8470 |
. . . . . . . 8
⊢
((𝒫 (𝐴 ∪
{𝑧}) ∈ Fin ∧
{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ⊆ 𝒫 (𝐴 ∪ {𝑧})) → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ Fin) |
60 | 57, 58, 59 | sylancl 580 |
. . . . . . 7
⊢ (𝜑 → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ Fin) |
61 | 60 | elexd 3416 |
. . . . . 6
⊢ (𝜑 → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ V) |
62 | | fveqeq2 6457 |
. . . . . . . 8
⊢ (𝑥 = 𝑢 → ((♯‘𝑥) = (𝐾 − 1) ↔ (♯‘𝑢) = (𝐾 − 1))) |
63 | 62 | elrab 3572 |
. . . . . . 7
⊢ (𝑢 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ↔ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) |
64 | | eleq2 2848 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑢 ∪ {𝑧}) → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ (𝑢 ∪ {𝑧}))) |
65 | | fveqeq2 6457 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑢 ∪ {𝑧}) → ((♯‘𝑥) = 𝐾 ↔ (♯‘(𝑢 ∪ {𝑧})) = 𝐾)) |
66 | 64, 65 | anbi12d 624 |
. . . . . . . . 9
⊢ (𝑥 = (𝑢 ∪ {𝑧}) → ((𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ↔ (𝑧 ∈ (𝑢 ∪ {𝑧}) ∧ (♯‘(𝑢 ∪ {𝑧})) = 𝐾))) |
67 | | elpwi 4389 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ 𝒫 𝐴 → 𝑢 ⊆ 𝐴) |
68 | 67 | ad2antrl 718 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → 𝑢 ⊆ 𝐴) |
69 | | unss1 4005 |
. . . . . . . . . . 11
⊢ (𝑢 ⊆ 𝐴 → (𝑢 ∪ {𝑧}) ⊆ (𝐴 ∪ {𝑧})) |
70 | 68, 69 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (𝑢 ∪ {𝑧}) ⊆ (𝐴 ∪ {𝑧})) |
71 | | vex 3401 |
. . . . . . . . . . . 12
⊢ 𝑢 ∈ V |
72 | | snex 5142 |
. . . . . . . . . . . 12
⊢ {𝑧} ∈ V |
73 | 71, 72 | unex 7235 |
. . . . . . . . . . 11
⊢ (𝑢 ∪ {𝑧}) ∈ V |
74 | 73 | elpw 4385 |
. . . . . . . . . 10
⊢ ((𝑢 ∪ {𝑧}) ∈ 𝒫 (𝐴 ∪ {𝑧}) ↔ (𝑢 ∪ {𝑧}) ⊆ (𝐴 ∪ {𝑧})) |
75 | 70, 74 | sylibr 226 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (𝑢 ∪ {𝑧}) ∈ 𝒫 (𝐴 ∪ {𝑧})) |
76 | 48 | adantr 474 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → 𝐴 ∈ Fin) |
77 | 76, 68 | ssfid 8473 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → 𝑢 ∈ Fin) |
78 | 53 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → {𝑧} ∈ Fin) |
79 | 14 | adantr 474 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → ¬ 𝑧 ∈ 𝐴) |
80 | 68, 79 | ssneldd 3824 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → ¬ 𝑧 ∈ 𝑢) |
81 | | disjsn 4478 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑢) |
82 | 80, 81 | sylibr 226 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (𝑢 ∩ {𝑧}) = ∅) |
83 | | hashun 13490 |
. . . . . . . . . . . 12
⊢ ((𝑢 ∈ Fin ∧ {𝑧} ∈ Fin ∧ (𝑢 ∩ {𝑧}) = ∅) → (♯‘(𝑢 ∪ {𝑧})) = ((♯‘𝑢) + (♯‘{𝑧}))) |
84 | 77, 78, 82, 83 | syl3anc 1439 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (♯‘(𝑢 ∪ {𝑧})) = ((♯‘𝑢) + (♯‘{𝑧}))) |
85 | | simprr 763 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (♯‘𝑢) = (𝐾 − 1)) |
86 | | hashsng 13478 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ V →
(♯‘{𝑧}) =
1) |
87 | 86 | elv 3402 |
. . . . . . . . . . . . 13
⊢
(♯‘{𝑧})
= 1 |
88 | 87 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (♯‘{𝑧}) = 1) |
89 | 85, 88 | oveq12d 6942 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → ((♯‘𝑢) + (♯‘{𝑧})) = ((𝐾 − 1) + 1)) |
90 | 7 | adantr 474 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → 𝐾 ∈ ℤ) |
91 | 90 | zcnd 11839 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → 𝐾 ∈ ℂ) |
92 | | ax-1cn 10332 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℂ |
93 | | npcan 10634 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝐾 −
1) + 1) = 𝐾) |
94 | 91, 92, 93 | sylancl 580 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → ((𝐾 − 1) + 1) = 𝐾) |
95 | 84, 89, 94 | 3eqtrd 2818 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (♯‘(𝑢 ∪ {𝑧})) = 𝐾) |
96 | | ssun2 4000 |
. . . . . . . . . . 11
⊢ {𝑧} ⊆ (𝑢 ∪ {𝑧}) |
97 | | vex 3401 |
. . . . . . . . . . . 12
⊢ 𝑧 ∈ V |
98 | 97 | snss 4549 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ (𝑢 ∪ {𝑧}) ↔ {𝑧} ⊆ (𝑢 ∪ {𝑧})) |
99 | 96, 98 | mpbir 223 |
. . . . . . . . . 10
⊢ 𝑧 ∈ (𝑢 ∪ {𝑧}) |
100 | 95, 99 | jctil 515 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (𝑧 ∈ (𝑢 ∪ {𝑧}) ∧ (♯‘(𝑢 ∪ {𝑧})) = 𝐾)) |
101 | 66, 75, 100 | elrabd 3575 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (𝑢 ∪ {𝑧}) ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) |
102 | 101 | ex 403 |
. . . . . . 7
⊢ (𝜑 → ((𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) → (𝑢 ∪ {𝑧}) ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)})) |
103 | 63, 102 | syl5bi 234 |
. . . . . 6
⊢ (𝜑 → (𝑢 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} → (𝑢 ∪ {𝑧}) ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)})) |
104 | | eleq2 2848 |
. . . . . . . . 9
⊢ (𝑥 = 𝑣 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑣)) |
105 | | fveqeq2 6457 |
. . . . . . . . 9
⊢ (𝑥 = 𝑣 → ((♯‘𝑥) = 𝐾 ↔ (♯‘𝑣) = 𝐾)) |
106 | 104, 105 | anbi12d 624 |
. . . . . . . 8
⊢ (𝑥 = 𝑣 → ((𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ↔ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) |
107 | 106 | elrab 3572 |
. . . . . . 7
⊢ (𝑣 ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ↔ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) |
108 | | fveqeq2 6457 |
. . . . . . . . 9
⊢ (𝑥 = (𝑣 ∖ {𝑧}) → ((♯‘𝑥) = (𝐾 − 1) ↔ (♯‘(𝑣 ∖ {𝑧})) = (𝐾 − 1))) |
109 | | elpwi 4389 |
. . . . . . . . . . . . 13
⊢ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) → 𝑣 ⊆ (𝐴 ∪ {𝑧})) |
110 | 109 | ad2antrl 718 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → 𝑣 ⊆ (𝐴 ∪ {𝑧})) |
111 | 110, 20 | syl6sseq 3870 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → 𝑣 ⊆ ({𝑧} ∪ 𝐴)) |
112 | | ssundif 4276 |
. . . . . . . . . . 11
⊢ (𝑣 ⊆ ({𝑧} ∪ 𝐴) ↔ (𝑣 ∖ {𝑧}) ⊆ 𝐴) |
113 | 111, 112 | sylib 210 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑣 ∖ {𝑧}) ⊆ 𝐴) |
114 | | vex 3401 |
. . . . . . . . . . . 12
⊢ 𝑣 ∈ V |
115 | 114 | difexi 5048 |
. . . . . . . . . . 11
⊢ (𝑣 ∖ {𝑧}) ∈ V |
116 | 115 | elpw 4385 |
. . . . . . . . . 10
⊢ ((𝑣 ∖ {𝑧}) ∈ 𝒫 𝐴 ↔ (𝑣 ∖ {𝑧}) ⊆ 𝐴) |
117 | 113, 116 | sylibr 226 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑣 ∖ {𝑧}) ∈ 𝒫 𝐴) |
118 | 48 | adantr 474 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → 𝐴 ∈ Fin) |
119 | 118, 113 | ssfid 8473 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑣 ∖ {𝑧}) ∈ Fin) |
120 | | hashcl 13466 |
. . . . . . . . . . . . 13
⊢ ((𝑣 ∖ {𝑧}) ∈ Fin → (♯‘(𝑣 ∖ {𝑧})) ∈
ℕ0) |
121 | 119, 120 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (♯‘(𝑣 ∖ {𝑧})) ∈
ℕ0) |
122 | 121 | nn0cnd 11708 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (♯‘(𝑣 ∖ {𝑧})) ∈ ℂ) |
123 | | pncan 10630 |
. . . . . . . . . . 11
⊢
(((♯‘(𝑣
∖ {𝑧})) ∈
ℂ ∧ 1 ∈ ℂ) → (((♯‘(𝑣 ∖ {𝑧})) + 1) − 1) = (♯‘(𝑣 ∖ {𝑧}))) |
124 | 122, 92, 123 | sylancl 580 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (((♯‘(𝑣 ∖ {𝑧})) + 1) − 1) = (♯‘(𝑣 ∖ {𝑧}))) |
125 | | undif1 4267 |
. . . . . . . . . . . . . 14
⊢ ((𝑣 ∖ {𝑧}) ∪ {𝑧}) = (𝑣 ∪ {𝑧}) |
126 | | simprrl 771 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → 𝑧 ∈ 𝑣) |
127 | 126 | snssd 4573 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → {𝑧} ⊆ 𝑣) |
128 | | ssequn2 4009 |
. . . . . . . . . . . . . . 15
⊢ ({𝑧} ⊆ 𝑣 ↔ (𝑣 ∪ {𝑧}) = 𝑣) |
129 | 127, 128 | sylib 210 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑣 ∪ {𝑧}) = 𝑣) |
130 | 125, 129 | syl5eq 2826 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → ((𝑣 ∖ {𝑧}) ∪ {𝑧}) = 𝑣) |
131 | 130 | fveq2d 6452 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (♯‘((𝑣 ∖ {𝑧}) ∪ {𝑧})) = (♯‘𝑣)) |
132 | 53 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → {𝑧} ∈ Fin) |
133 | | incom 4028 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑣 ∖ {𝑧}) ∩ {𝑧}) = ({𝑧} ∩ (𝑣 ∖ {𝑧})) |
134 | | disjdif 4264 |
. . . . . . . . . . . . . . . 16
⊢ ({𝑧} ∩ (𝑣 ∖ {𝑧})) = ∅ |
135 | 133, 134 | eqtri 2802 |
. . . . . . . . . . . . . . 15
⊢ ((𝑣 ∖ {𝑧}) ∩ {𝑧}) = ∅ |
136 | 135 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → ((𝑣 ∖ {𝑧}) ∩ {𝑧}) = ∅) |
137 | | hashun 13490 |
. . . . . . . . . . . . . 14
⊢ (((𝑣 ∖ {𝑧}) ∈ Fin ∧ {𝑧} ∈ Fin ∧ ((𝑣 ∖ {𝑧}) ∩ {𝑧}) = ∅) → (♯‘((𝑣 ∖ {𝑧}) ∪ {𝑧})) = ((♯‘(𝑣 ∖ {𝑧})) + (♯‘{𝑧}))) |
138 | 119, 132,
136, 137 | syl3anc 1439 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (♯‘((𝑣 ∖ {𝑧}) ∪ {𝑧})) = ((♯‘(𝑣 ∖ {𝑧})) + (♯‘{𝑧}))) |
139 | 87 | oveq2i 6935 |
. . . . . . . . . . . . 13
⊢
((♯‘(𝑣
∖ {𝑧})) +
(♯‘{𝑧})) =
((♯‘(𝑣 ∖
{𝑧})) + 1) |
140 | 138, 139 | syl6eq 2830 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (♯‘((𝑣 ∖ {𝑧}) ∪ {𝑧})) = ((♯‘(𝑣 ∖ {𝑧})) + 1)) |
141 | | simprrr 772 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (♯‘𝑣) = 𝐾) |
142 | 131, 140,
141 | 3eqtr3d 2822 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → ((♯‘(𝑣 ∖ {𝑧})) + 1) = 𝐾) |
143 | 142 | oveq1d 6939 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (((♯‘(𝑣 ∖ {𝑧})) + 1) − 1) = (𝐾 − 1)) |
144 | 124, 143 | eqtr3d 2816 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (♯‘(𝑣 ∖ {𝑧})) = (𝐾 − 1)) |
145 | 108, 117,
144 | elrabd 3575 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑣 ∖ {𝑧}) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)}) |
146 | 145 | ex 403 |
. . . . . . 7
⊢ (𝜑 → ((𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾)) → (𝑣 ∖ {𝑧}) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)})) |
147 | 107, 146 | syl5bi 234 |
. . . . . 6
⊢ (𝜑 → (𝑣 ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} → (𝑣 ∖ {𝑧}) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)})) |
148 | 63, 107 | anbi12i 620 |
. . . . . . 7
⊢ ((𝑢 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ∧ 𝑣 ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) ↔ ((𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾)))) |
149 | | simp3rl 1284 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → 𝑧 ∈ 𝑣) |
150 | 149 | snssd 4573 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → {𝑧} ⊆ 𝑣) |
151 | | incom 4028 |
. . . . . . . . . . . 12
⊢ ({𝑧} ∩ 𝑢) = (𝑢 ∩ {𝑧}) |
152 | 82 | 3adant3 1123 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑢 ∩ {𝑧}) = ∅) |
153 | 151, 152 | syl5eq 2826 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → ({𝑧} ∩ 𝑢) = ∅) |
154 | | uneqdifeq 4281 |
. . . . . . . . . . 11
⊢ (({𝑧} ⊆ 𝑣 ∧ ({𝑧} ∩ 𝑢) = ∅) → (({𝑧} ∪ 𝑢) = 𝑣 ↔ (𝑣 ∖ {𝑧}) = 𝑢)) |
155 | 150, 153,
154 | syl2anc 579 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (({𝑧} ∪ 𝑢) = 𝑣 ↔ (𝑣 ∖ {𝑧}) = 𝑢)) |
156 | 155 | bicomd 215 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → ((𝑣 ∖ {𝑧}) = 𝑢 ↔ ({𝑧} ∪ 𝑢) = 𝑣)) |
157 | | eqcom 2785 |
. . . . . . . . 9
⊢ (𝑢 = (𝑣 ∖ {𝑧}) ↔ (𝑣 ∖ {𝑧}) = 𝑢) |
158 | | eqcom 2785 |
. . . . . . . . . 10
⊢ (𝑣 = (𝑢 ∪ {𝑧}) ↔ (𝑢 ∪ {𝑧}) = 𝑣) |
159 | | uncom 3980 |
. . . . . . . . . . 11
⊢ (𝑢 ∪ {𝑧}) = ({𝑧} ∪ 𝑢) |
160 | 159 | eqeq1i 2783 |
. . . . . . . . . 10
⊢ ((𝑢 ∪ {𝑧}) = 𝑣 ↔ ({𝑧} ∪ 𝑢) = 𝑣) |
161 | 158, 160 | bitri 267 |
. . . . . . . . 9
⊢ (𝑣 = (𝑢 ∪ {𝑧}) ↔ ({𝑧} ∪ 𝑢) = 𝑣) |
162 | 156, 157,
161 | 3bitr4g 306 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑢 = (𝑣 ∖ {𝑧}) ↔ 𝑣 = (𝑢 ∪ {𝑧}))) |
163 | 162 | 3expib 1113 |
. . . . . . 7
⊢ (𝜑 → (((𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑢 = (𝑣 ∖ {𝑧}) ↔ 𝑣 = (𝑢 ∪ {𝑧})))) |
164 | 148, 163 | syl5bi 234 |
. . . . . 6
⊢ (𝜑 → ((𝑢 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ∧ 𝑣 ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) → (𝑢 = (𝑣 ∖ {𝑧}) ↔ 𝑣 = (𝑢 ∪ {𝑧})))) |
165 | 52, 61, 103, 147, 164 | en3d 8280 |
. . . . 5
⊢ (𝜑 → {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ≈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) |
166 | | ssrab2 3908 |
. . . . . . 7
⊢ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ⊆ 𝒫 𝐴 |
167 | | ssfi 8470 |
. . . . . . 7
⊢
((𝒫 𝐴 ∈
Fin ∧ {𝑥 ∈
𝒫 𝐴 ∣
(♯‘𝑥) = (𝐾 − 1)} ⊆ 𝒫
𝐴) → {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ∈ Fin) |
168 | 50, 166, 167 | sylancl 580 |
. . . . . 6
⊢ (𝜑 → {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ∈ Fin) |
169 | | hashen 13456 |
. . . . . 6
⊢ (({𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ∈ Fin ∧ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ Fin) → ((♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)}) = (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) ↔ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ≈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)})) |
170 | 168, 60, 169 | syl2anc 579 |
. . . . 5
⊢ (𝜑 → ((♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)}) = (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) ↔ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ≈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)})) |
171 | 165, 170 | mpbird 249 |
. . . 4
⊢ (𝜑 → (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)}) = (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)})) |
172 | 47, 171 | eqtrd 2814 |
. . 3
⊢ (𝜑 → ((♯‘𝐴)C(𝐾 − 1)) = (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)})) |
173 | 39, 172 | oveq12d 6942 |
. 2
⊢ (𝜑 → (((♯‘𝐴)C𝐾) + ((♯‘𝐴)C(𝐾 − 1))) = ((♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) + (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}))) |
174 | 53 | a1i 11 |
. . . . . 6
⊢ (𝜑 → {𝑧} ∈ Fin) |
175 | | disjsn 4478 |
. . . . . . 7
⊢ ((𝐴 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝐴) |
176 | 14, 175 | sylibr 226 |
. . . . . 6
⊢ (𝜑 → (𝐴 ∩ {𝑧}) = ∅) |
177 | | hashun 13490 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ {𝑧} ∈ Fin ∧ (𝐴 ∩ {𝑧}) = ∅) → (♯‘(𝐴 ∪ {𝑧})) = ((♯‘𝐴) + (♯‘{𝑧}))) |
178 | 48, 174, 176, 177 | syl3anc 1439 |
. . . . 5
⊢ (𝜑 → (♯‘(𝐴 ∪ {𝑧})) = ((♯‘𝐴) + (♯‘{𝑧}))) |
179 | 87 | oveq2i 6935 |
. . . . 5
⊢
((♯‘𝐴) +
(♯‘{𝑧})) =
((♯‘𝐴) +
1) |
180 | 178, 179 | syl6eq 2830 |
. . . 4
⊢ (𝜑 → (♯‘(𝐴 ∪ {𝑧})) = ((♯‘𝐴) + 1)) |
181 | 180 | oveq1d 6939 |
. . 3
⊢ (𝜑 → ((♯‘(𝐴 ∪ {𝑧}))C𝐾) = (((♯‘𝐴) + 1)C𝐾)) |
182 | | hashcl 13466 |
. . . . 5
⊢ (𝐴 ∈ Fin →
(♯‘𝐴) ∈
ℕ0) |
183 | 48, 182 | syl 17 |
. . . 4
⊢ (𝜑 → (♯‘𝐴) ∈
ℕ0) |
184 | | bcpasc 13430 |
. . . 4
⊢
(((♯‘𝐴)
∈ ℕ0 ∧ 𝐾 ∈ ℤ) →
(((♯‘𝐴)C𝐾) + ((♯‘𝐴)C(𝐾 − 1))) = (((♯‘𝐴) + 1)C𝐾)) |
185 | 183, 7, 184 | syl2anc 579 |
. . 3
⊢ (𝜑 → (((♯‘𝐴)C𝐾) + ((♯‘𝐴)C(𝐾 − 1))) = (((♯‘𝐴) + 1)C𝐾)) |
186 | 181, 185 | eqtr4d 2817 |
. 2
⊢ (𝜑 → ((♯‘(𝐴 ∪ {𝑧}))C𝐾) = (((♯‘𝐴)C𝐾) + ((♯‘𝐴)C(𝐾 − 1)))) |
187 | | pm2.1 883 |
. . . . . . . 8
⊢ (¬
𝑧 ∈ 𝑥 ∨ 𝑧 ∈ 𝑥) |
188 | 187 | biantrur 526 |
. . . . . . 7
⊢
((♯‘𝑥) =
𝐾 ↔ ((¬ 𝑧 ∈ 𝑥 ∨ 𝑧 ∈ 𝑥) ∧ (♯‘𝑥) = 𝐾)) |
189 | | andir 994 |
. . . . . . 7
⊢ (((¬
𝑧 ∈ 𝑥 ∨ 𝑧 ∈ 𝑥) ∧ (♯‘𝑥) = 𝐾) ↔ ((¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ∨ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾))) |
190 | 188, 189 | bitri 267 |
. . . . . 6
⊢
((♯‘𝑥) =
𝐾 ↔ ((¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ∨ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾))) |
191 | 190 | rabbii 3382 |
. . . . 5
⊢ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (♯‘𝑥) = 𝐾} = {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ∨ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾))} |
192 | | unrab 4124 |
. . . . 5
⊢ ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) = {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ∨ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾))} |
193 | 191, 192 | eqtr4i 2805 |
. . . 4
⊢ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (♯‘𝑥) = 𝐾} = ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) |
194 | 193 | fveq2i 6451 |
. . 3
⊢
(♯‘{𝑥
∈ 𝒫 (𝐴 ∪
{𝑧}) ∣
(♯‘𝑥) = 𝐾}) = (♯‘({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)})) |
195 | | ssrab2 3908 |
. . . . 5
⊢ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ⊆ 𝒫 (𝐴 ∪ {𝑧}) |
196 | | ssfi 8470 |
. . . . 5
⊢
((𝒫 (𝐴 ∪
{𝑧}) ∈ Fin ∧
{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ⊆ 𝒫 (𝐴 ∪ {𝑧})) → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ Fin) |
197 | 57, 195, 196 | sylancl 580 |
. . . 4
⊢ (𝜑 → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ Fin) |
198 | | inrab 4125 |
. . . . . 6
⊢ ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∩ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) = {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾))} |
199 | | simprl 761 |
. . . . . . . . 9
⊢ (((¬
𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)) → 𝑧 ∈ 𝑥) |
200 | | simpll 757 |
. . . . . . . . 9
⊢ (((¬
𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)) → ¬ 𝑧 ∈ 𝑥) |
201 | 199, 200 | pm2.65i 186 |
. . . . . . . 8
⊢ ¬
((¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)) |
202 | 201 | rgenw 3106 |
. . . . . . 7
⊢
∀𝑥 ∈
𝒫 (𝐴 ∪ {𝑧}) ¬ ((¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)) |
203 | | rabeq0 4187 |
. . . . . . 7
⊢ ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾))} = ∅ ↔ ∀𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ¬ ((¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾))) |
204 | 202, 203 | mpbir 223 |
. . . . . 6
⊢ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾))} = ∅ |
205 | 198, 204 | eqtri 2802 |
. . . . 5
⊢ ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∩ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) = ∅ |
206 | 205 | a1i 11 |
. . . 4
⊢ (𝜑 → ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∩ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) = ∅) |
207 | | hashun 13490 |
. . . 4
⊢ (({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ Fin ∧ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ Fin ∧ ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∩ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) = ∅) → (♯‘({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)})) = ((♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) + (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}))) |
208 | 197, 60, 206, 207 | syl3anc 1439 |
. . 3
⊢ (𝜑 → (♯‘({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)})) = ((♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) + (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}))) |
209 | 194, 208 | syl5eq 2826 |
. 2
⊢ (𝜑 → (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (♯‘𝑥) = 𝐾}) = ((♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) + (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}))) |
210 | 173, 186,
209 | 3eqtr4d 2824 |
1
⊢ (𝜑 → ((♯‘(𝐴 ∪ {𝑧}))C𝐾) = (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (♯‘𝑥) = 𝐾})) |