Step | Hyp | Ref
| Expression |
1 | | oveq2 7143 |
. . . . . 6
⊢ (𝑗 = 𝐾 → ((♯‘𝐴)C𝑗) = ((♯‘𝐴)C𝐾)) |
2 | | eqeq2 2810 |
. . . . . . . 8
⊢ (𝑗 = 𝐾 → ((♯‘𝑥) = 𝑗 ↔ (♯‘𝑥) = 𝐾)) |
3 | 2 | rabbidv 3427 |
. . . . . . 7
⊢ (𝑗 = 𝐾 → {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑗} = {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝐾}) |
4 | 3 | fveq2d 6649 |
. . . . . 6
⊢ (𝑗 = 𝐾 → (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑗}) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝐾})) |
5 | 1, 4 | eqeq12d 2814 |
. . . . 5
⊢ (𝑗 = 𝐾 → (((♯‘𝐴)C𝑗) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑗}) ↔ ((♯‘𝐴)C𝐾) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝐾}))) |
6 | | hashbc.3 |
. . . . 5
⊢ (𝜑 → ∀𝑗 ∈ ℤ ((♯‘𝐴)C𝑗) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑗})) |
7 | | hashbc.4 |
. . . . 5
⊢ (𝜑 → 𝐾 ∈ ℤ) |
8 | 5, 6, 7 | rspcdva 3573 |
. . . 4
⊢ (𝜑 → ((♯‘𝐴)C𝐾) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝐾})) |
9 | | ssun1 4099 |
. . . . . . . . . . . . 13
⊢ 𝐴 ⊆ (𝐴 ∪ {𝑧}) |
10 | 9 | sspwi 4511 |
. . . . . . . . . . . 12
⊢ 𝒫
𝐴 ⊆ 𝒫 (𝐴 ∪ {𝑧}) |
11 | 10 | sseli 3911 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧})) |
12 | 11 | adantl 485 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝐴) → 𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧})) |
13 | | hashbc.2 |
. . . . . . . . . . 11
⊢ (𝜑 → ¬ 𝑧 ∈ 𝐴) |
14 | | elpwi 4506 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝒫 𝐴 → 𝑥 ⊆ 𝐴) |
15 | 14 | ssneld 3917 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝒫 𝐴 → (¬ 𝑧 ∈ 𝐴 → ¬ 𝑧 ∈ 𝑥)) |
16 | 13, 15 | mpan9 510 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝐴) → ¬ 𝑧 ∈ 𝑥) |
17 | 12, 16 | jca 515 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝐴) → (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥)) |
18 | | elpwi 4506 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) → 𝑥 ⊆ (𝐴 ∪ {𝑧})) |
19 | | uncom 4080 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∪ {𝑧}) = ({𝑧} ∪ 𝐴) |
20 | 18, 19 | sseqtrdi 3965 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) → 𝑥 ⊆ ({𝑧} ∪ 𝐴)) |
21 | 20 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥) → 𝑥 ⊆ ({𝑧} ∪ 𝐴)) |
22 | | simpr 488 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥) → ¬ 𝑧 ∈ 𝑥) |
23 | | disjsn 4607 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑥) |
24 | 22, 23 | sylibr 237 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥) → (𝑥 ∩ {𝑧}) = ∅) |
25 | | disjssun 4375 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∩ {𝑧}) = ∅ → (𝑥 ⊆ ({𝑧} ∪ 𝐴) ↔ 𝑥 ⊆ 𝐴)) |
26 | 24, 25 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥) → (𝑥 ⊆ ({𝑧} ∪ 𝐴) ↔ 𝑥 ⊆ 𝐴)) |
27 | 21, 26 | mpbid 235 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥) → 𝑥 ⊆ 𝐴) |
28 | | vex 3444 |
. . . . . . . . . . . 12
⊢ 𝑥 ∈ V |
29 | 28 | elpw 4501 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴) |
30 | 27, 29 | sylibr 237 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥) → 𝑥 ∈ 𝒫 𝐴) |
31 | 30 | adantl 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥)) → 𝑥 ∈ 𝒫 𝐴) |
32 | 17, 31 | impbida 800 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝒫 𝐴 ↔ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥))) |
33 | 32 | anbi1d 632 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ 𝒫 𝐴 ∧ (♯‘𝑥) = 𝐾) ↔ ((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥) ∧ (♯‘𝑥) = 𝐾))) |
34 | | anass 472 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ ¬ 𝑧 ∈ 𝑥) ∧ (♯‘𝑥) = 𝐾) ↔ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾))) |
35 | 33, 34 | syl6bb 290 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ 𝒫 𝐴 ∧ (♯‘𝑥) = 𝐾) ↔ (𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)))) |
36 | 35 | rabbidva2 3423 |
. . . . 5
⊢ (𝜑 → {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝐾} = {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) |
37 | 36 | fveq2d 6649 |
. . . 4
⊢ (𝜑 → (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝐾}) = (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)})) |
38 | 8, 37 | eqtrd 2833 |
. . 3
⊢ (𝜑 → ((♯‘𝐴)C𝐾) = (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)})) |
39 | | oveq2 7143 |
. . . . . 6
⊢ (𝑗 = (𝐾 − 1) → ((♯‘𝐴)C𝑗) = ((♯‘𝐴)C(𝐾 − 1))) |
40 | | eqeq2 2810 |
. . . . . . . 8
⊢ (𝑗 = (𝐾 − 1) → ((♯‘𝑥) = 𝑗 ↔ (♯‘𝑥) = (𝐾 − 1))) |
41 | 40 | rabbidv 3427 |
. . . . . . 7
⊢ (𝑗 = (𝐾 − 1) → {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑗} = {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)}) |
42 | 41 | fveq2d 6649 |
. . . . . 6
⊢ (𝑗 = (𝐾 − 1) → (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑗}) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)})) |
43 | 39, 42 | eqeq12d 2814 |
. . . . 5
⊢ (𝑗 = (𝐾 − 1) → (((♯‘𝐴)C𝑗) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = 𝑗}) ↔ ((♯‘𝐴)C(𝐾 − 1)) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)}))) |
44 | | peano2zm 12013 |
. . . . . 6
⊢ (𝐾 ∈ ℤ → (𝐾 − 1) ∈
ℤ) |
45 | 7, 44 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐾 − 1) ∈ ℤ) |
46 | 43, 6, 45 | rspcdva 3573 |
. . . 4
⊢ (𝜑 → ((♯‘𝐴)C(𝐾 − 1)) = (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)})) |
47 | | hashbc.1 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ Fin) |
48 | | pwfi 8803 |
. . . . . . . 8
⊢ (𝐴 ∈ Fin ↔ 𝒫
𝐴 ∈
Fin) |
49 | 47, 48 | sylib 221 |
. . . . . . 7
⊢ (𝜑 → 𝒫 𝐴 ∈ Fin) |
50 | | rabexg 5198 |
. . . . . . 7
⊢
(𝒫 𝐴 ∈
Fin → {𝑥 ∈
𝒫 𝐴 ∣
(♯‘𝑥) = (𝐾 − 1)} ∈
V) |
51 | 49, 50 | syl 17 |
. . . . . 6
⊢ (𝜑 → {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ∈ V) |
52 | | snfi 8577 |
. . . . . . . . . 10
⊢ {𝑧} ∈ Fin |
53 | | unfi 8769 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ Fin ∧ {𝑧} ∈ Fin) → (𝐴 ∪ {𝑧}) ∈ Fin) |
54 | 47, 52, 53 | sylancl 589 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 ∪ {𝑧}) ∈ Fin) |
55 | | pwfi 8803 |
. . . . . . . . 9
⊢ ((𝐴 ∪ {𝑧}) ∈ Fin ↔ 𝒫 (𝐴 ∪ {𝑧}) ∈ Fin) |
56 | 54, 55 | sylib 221 |
. . . . . . . 8
⊢ (𝜑 → 𝒫 (𝐴 ∪ {𝑧}) ∈ Fin) |
57 | | ssrab2 4007 |
. . . . . . . 8
⊢ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ⊆ 𝒫 (𝐴 ∪ {𝑧}) |
58 | | ssfi 8722 |
. . . . . . . 8
⊢
((𝒫 (𝐴 ∪
{𝑧}) ∈ Fin ∧
{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ⊆ 𝒫 (𝐴 ∪ {𝑧})) → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ Fin) |
59 | 56, 57, 58 | sylancl 589 |
. . . . . . 7
⊢ (𝜑 → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ Fin) |
60 | 59 | elexd 3461 |
. . . . . 6
⊢ (𝜑 → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ V) |
61 | | fveqeq2 6654 |
. . . . . . . 8
⊢ (𝑥 = 𝑢 → ((♯‘𝑥) = (𝐾 − 1) ↔ (♯‘𝑢) = (𝐾 − 1))) |
62 | 61 | elrab 3628 |
. . . . . . 7
⊢ (𝑢 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ↔ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) |
63 | | eleq2 2878 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑢 ∪ {𝑧}) → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ (𝑢 ∪ {𝑧}))) |
64 | | fveqeq2 6654 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑢 ∪ {𝑧}) → ((♯‘𝑥) = 𝐾 ↔ (♯‘(𝑢 ∪ {𝑧})) = 𝐾)) |
65 | 63, 64 | anbi12d 633 |
. . . . . . . . 9
⊢ (𝑥 = (𝑢 ∪ {𝑧}) → ((𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ↔ (𝑧 ∈ (𝑢 ∪ {𝑧}) ∧ (♯‘(𝑢 ∪ {𝑧})) = 𝐾))) |
66 | | elpwi 4506 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ 𝒫 𝐴 → 𝑢 ⊆ 𝐴) |
67 | 66 | ad2antrl 727 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → 𝑢 ⊆ 𝐴) |
68 | | unss1 4106 |
. . . . . . . . . . 11
⊢ (𝑢 ⊆ 𝐴 → (𝑢 ∪ {𝑧}) ⊆ (𝐴 ∪ {𝑧})) |
69 | 67, 68 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (𝑢 ∪ {𝑧}) ⊆ (𝐴 ∪ {𝑧})) |
70 | | vex 3444 |
. . . . . . . . . . . 12
⊢ 𝑢 ∈ V |
71 | | snex 5297 |
. . . . . . . . . . . 12
⊢ {𝑧} ∈ V |
72 | 70, 71 | unex 7449 |
. . . . . . . . . . 11
⊢ (𝑢 ∪ {𝑧}) ∈ V |
73 | 72 | elpw 4501 |
. . . . . . . . . 10
⊢ ((𝑢 ∪ {𝑧}) ∈ 𝒫 (𝐴 ∪ {𝑧}) ↔ (𝑢 ∪ {𝑧}) ⊆ (𝐴 ∪ {𝑧})) |
74 | 69, 73 | sylibr 237 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (𝑢 ∪ {𝑧}) ∈ 𝒫 (𝐴 ∪ {𝑧})) |
75 | 47 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → 𝐴 ∈ Fin) |
76 | 75, 67 | ssfid 8725 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → 𝑢 ∈ Fin) |
77 | 52 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → {𝑧} ∈ Fin) |
78 | 13 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → ¬ 𝑧 ∈ 𝐴) |
79 | 67, 78 | ssneldd 3918 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → ¬ 𝑧 ∈ 𝑢) |
80 | | disjsn 4607 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑢) |
81 | 79, 80 | sylibr 237 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (𝑢 ∩ {𝑧}) = ∅) |
82 | | hashun 13739 |
. . . . . . . . . . . 12
⊢ ((𝑢 ∈ Fin ∧ {𝑧} ∈ Fin ∧ (𝑢 ∩ {𝑧}) = ∅) → (♯‘(𝑢 ∪ {𝑧})) = ((♯‘𝑢) + (♯‘{𝑧}))) |
83 | 76, 77, 81, 82 | syl3anc 1368 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (♯‘(𝑢 ∪ {𝑧})) = ((♯‘𝑢) + (♯‘{𝑧}))) |
84 | | simprr 772 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (♯‘𝑢) = (𝐾 − 1)) |
85 | | hashsng 13726 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ V →
(♯‘{𝑧}) =
1) |
86 | 85 | elv 3446 |
. . . . . . . . . . . . 13
⊢
(♯‘{𝑧})
= 1 |
87 | 86 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (♯‘{𝑧}) = 1) |
88 | 84, 87 | oveq12d 7153 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → ((♯‘𝑢) + (♯‘{𝑧})) = ((𝐾 − 1) + 1)) |
89 | 7 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → 𝐾 ∈ ℤ) |
90 | 89 | zcnd 12076 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → 𝐾 ∈ ℂ) |
91 | | ax-1cn 10584 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℂ |
92 | | npcan 10884 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝐾 −
1) + 1) = 𝐾) |
93 | 90, 91, 92 | sylancl 589 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → ((𝐾 − 1) + 1) = 𝐾) |
94 | 83, 88, 93 | 3eqtrd 2837 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (♯‘(𝑢 ∪ {𝑧})) = 𝐾) |
95 | | ssun2 4100 |
. . . . . . . . . . 11
⊢ {𝑧} ⊆ (𝑢 ∪ {𝑧}) |
96 | | vex 3444 |
. . . . . . . . . . . 12
⊢ 𝑧 ∈ V |
97 | 96 | snss 4679 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ (𝑢 ∪ {𝑧}) ↔ {𝑧} ⊆ (𝑢 ∪ {𝑧})) |
98 | 95, 97 | mpbir 234 |
. . . . . . . . . 10
⊢ 𝑧 ∈ (𝑢 ∪ {𝑧}) |
99 | 94, 98 | jctil 523 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (𝑧 ∈ (𝑢 ∪ {𝑧}) ∧ (♯‘(𝑢 ∪ {𝑧})) = 𝐾)) |
100 | 65, 74, 99 | elrabd 3630 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1))) → (𝑢 ∪ {𝑧}) ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) |
101 | 100 | ex 416 |
. . . . . . 7
⊢ (𝜑 → ((𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) → (𝑢 ∪ {𝑧}) ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)})) |
102 | 62, 101 | syl5bi 245 |
. . . . . 6
⊢ (𝜑 → (𝑢 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} → (𝑢 ∪ {𝑧}) ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)})) |
103 | | eleq2 2878 |
. . . . . . . . 9
⊢ (𝑥 = 𝑣 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑣)) |
104 | | fveqeq2 6654 |
. . . . . . . . 9
⊢ (𝑥 = 𝑣 → ((♯‘𝑥) = 𝐾 ↔ (♯‘𝑣) = 𝐾)) |
105 | 103, 104 | anbi12d 633 |
. . . . . . . 8
⊢ (𝑥 = 𝑣 → ((𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ↔ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) |
106 | 105 | elrab 3628 |
. . . . . . 7
⊢ (𝑣 ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ↔ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) |
107 | | fveqeq2 6654 |
. . . . . . . . 9
⊢ (𝑥 = (𝑣 ∖ {𝑧}) → ((♯‘𝑥) = (𝐾 − 1) ↔ (♯‘(𝑣 ∖ {𝑧})) = (𝐾 − 1))) |
108 | | elpwi 4506 |
. . . . . . . . . . . . 13
⊢ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) → 𝑣 ⊆ (𝐴 ∪ {𝑧})) |
109 | 108 | ad2antrl 727 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → 𝑣 ⊆ (𝐴 ∪ {𝑧})) |
110 | 109, 19 | sseqtrdi 3965 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → 𝑣 ⊆ ({𝑧} ∪ 𝐴)) |
111 | | ssundif 4391 |
. . . . . . . . . . 11
⊢ (𝑣 ⊆ ({𝑧} ∪ 𝐴) ↔ (𝑣 ∖ {𝑧}) ⊆ 𝐴) |
112 | 110, 111 | sylib 221 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑣 ∖ {𝑧}) ⊆ 𝐴) |
113 | | vex 3444 |
. . . . . . . . . . . 12
⊢ 𝑣 ∈ V |
114 | 113 | difexi 5196 |
. . . . . . . . . . 11
⊢ (𝑣 ∖ {𝑧}) ∈ V |
115 | 114 | elpw 4501 |
. . . . . . . . . 10
⊢ ((𝑣 ∖ {𝑧}) ∈ 𝒫 𝐴 ↔ (𝑣 ∖ {𝑧}) ⊆ 𝐴) |
116 | 112, 115 | sylibr 237 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑣 ∖ {𝑧}) ∈ 𝒫 𝐴) |
117 | 47 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → 𝐴 ∈ Fin) |
118 | 117, 112 | ssfid 8725 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑣 ∖ {𝑧}) ∈ Fin) |
119 | | hashcl 13713 |
. . . . . . . . . . . . 13
⊢ ((𝑣 ∖ {𝑧}) ∈ Fin → (♯‘(𝑣 ∖ {𝑧})) ∈
ℕ0) |
120 | 118, 119 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (♯‘(𝑣 ∖ {𝑧})) ∈
ℕ0) |
121 | 120 | nn0cnd 11945 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (♯‘(𝑣 ∖ {𝑧})) ∈ ℂ) |
122 | | pncan 10881 |
. . . . . . . . . . 11
⊢
(((♯‘(𝑣
∖ {𝑧})) ∈
ℂ ∧ 1 ∈ ℂ) → (((♯‘(𝑣 ∖ {𝑧})) + 1) − 1) = (♯‘(𝑣 ∖ {𝑧}))) |
123 | 121, 91, 122 | sylancl 589 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (((♯‘(𝑣 ∖ {𝑧})) + 1) − 1) = (♯‘(𝑣 ∖ {𝑧}))) |
124 | | undif1 4382 |
. . . . . . . . . . . . . 14
⊢ ((𝑣 ∖ {𝑧}) ∪ {𝑧}) = (𝑣 ∪ {𝑧}) |
125 | | simprrl 780 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → 𝑧 ∈ 𝑣) |
126 | 125 | snssd 4702 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → {𝑧} ⊆ 𝑣) |
127 | | ssequn2 4110 |
. . . . . . . . . . . . . . 15
⊢ ({𝑧} ⊆ 𝑣 ↔ (𝑣 ∪ {𝑧}) = 𝑣) |
128 | 126, 127 | sylib 221 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑣 ∪ {𝑧}) = 𝑣) |
129 | 124, 128 | syl5eq 2845 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → ((𝑣 ∖ {𝑧}) ∪ {𝑧}) = 𝑣) |
130 | 129 | fveq2d 6649 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (♯‘((𝑣 ∖ {𝑧}) ∪ {𝑧})) = (♯‘𝑣)) |
131 | 52 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → {𝑧} ∈ Fin) |
132 | | incom 4128 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑣 ∖ {𝑧}) ∩ {𝑧}) = ({𝑧} ∩ (𝑣 ∖ {𝑧})) |
133 | | disjdif 4379 |
. . . . . . . . . . . . . . . 16
⊢ ({𝑧} ∩ (𝑣 ∖ {𝑧})) = ∅ |
134 | 132, 133 | eqtri 2821 |
. . . . . . . . . . . . . . 15
⊢ ((𝑣 ∖ {𝑧}) ∩ {𝑧}) = ∅ |
135 | 134 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → ((𝑣 ∖ {𝑧}) ∩ {𝑧}) = ∅) |
136 | | hashun 13739 |
. . . . . . . . . . . . . 14
⊢ (((𝑣 ∖ {𝑧}) ∈ Fin ∧ {𝑧} ∈ Fin ∧ ((𝑣 ∖ {𝑧}) ∩ {𝑧}) = ∅) → (♯‘((𝑣 ∖ {𝑧}) ∪ {𝑧})) = ((♯‘(𝑣 ∖ {𝑧})) + (♯‘{𝑧}))) |
137 | 118, 131,
135, 136 | syl3anc 1368 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (♯‘((𝑣 ∖ {𝑧}) ∪ {𝑧})) = ((♯‘(𝑣 ∖ {𝑧})) + (♯‘{𝑧}))) |
138 | 86 | oveq2i 7146 |
. . . . . . . . . . . . 13
⊢
((♯‘(𝑣
∖ {𝑧})) +
(♯‘{𝑧})) =
((♯‘(𝑣 ∖
{𝑧})) + 1) |
139 | 137, 138 | eqtrdi 2849 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (♯‘((𝑣 ∖ {𝑧}) ∪ {𝑧})) = ((♯‘(𝑣 ∖ {𝑧})) + 1)) |
140 | | simprrr 781 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (♯‘𝑣) = 𝐾) |
141 | 130, 139,
140 | 3eqtr3d 2841 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → ((♯‘(𝑣 ∖ {𝑧})) + 1) = 𝐾) |
142 | 141 | oveq1d 7150 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (((♯‘(𝑣 ∖ {𝑧})) + 1) − 1) = (𝐾 − 1)) |
143 | 123, 142 | eqtr3d 2835 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (♯‘(𝑣 ∖ {𝑧})) = (𝐾 − 1)) |
144 | 107, 116,
143 | elrabd 3630 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑣 ∖ {𝑧}) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)}) |
145 | 144 | ex 416 |
. . . . . . 7
⊢ (𝜑 → ((𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾)) → (𝑣 ∖ {𝑧}) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)})) |
146 | 106, 145 | syl5bi 245 |
. . . . . 6
⊢ (𝜑 → (𝑣 ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} → (𝑣 ∖ {𝑧}) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)})) |
147 | 62, 106 | anbi12i 629 |
. . . . . . 7
⊢ ((𝑢 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ∧ 𝑣 ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) ↔ ((𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾)))) |
148 | | simp3rl 1243 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → 𝑧 ∈ 𝑣) |
149 | 148 | snssd 4702 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → {𝑧} ⊆ 𝑣) |
150 | | incom 4128 |
. . . . . . . . . . . 12
⊢ ({𝑧} ∩ 𝑢) = (𝑢 ∩ {𝑧}) |
151 | 81 | 3adant3 1129 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑢 ∩ {𝑧}) = ∅) |
152 | 150, 151 | syl5eq 2845 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → ({𝑧} ∩ 𝑢) = ∅) |
153 | | uneqdifeq 4396 |
. . . . . . . . . . 11
⊢ (({𝑧} ⊆ 𝑣 ∧ ({𝑧} ∩ 𝑢) = ∅) → (({𝑧} ∪ 𝑢) = 𝑣 ↔ (𝑣 ∖ {𝑧}) = 𝑢)) |
154 | 149, 152,
153 | syl2anc 587 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (({𝑧} ∪ 𝑢) = 𝑣 ↔ (𝑣 ∖ {𝑧}) = 𝑢)) |
155 | 154 | bicomd 226 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → ((𝑣 ∖ {𝑧}) = 𝑢 ↔ ({𝑧} ∪ 𝑢) = 𝑣)) |
156 | | eqcom 2805 |
. . . . . . . . 9
⊢ (𝑢 = (𝑣 ∖ {𝑧}) ↔ (𝑣 ∖ {𝑧}) = 𝑢) |
157 | | eqcom 2805 |
. . . . . . . . . 10
⊢ (𝑣 = (𝑢 ∪ {𝑧}) ↔ (𝑢 ∪ {𝑧}) = 𝑣) |
158 | | uncom 4080 |
. . . . . . . . . . 11
⊢ (𝑢 ∪ {𝑧}) = ({𝑧} ∪ 𝑢) |
159 | 158 | eqeq1i 2803 |
. . . . . . . . . 10
⊢ ((𝑢 ∪ {𝑧}) = 𝑣 ↔ ({𝑧} ∪ 𝑢) = 𝑣) |
160 | 157, 159 | bitri 278 |
. . . . . . . . 9
⊢ (𝑣 = (𝑢 ∪ {𝑧}) ↔ ({𝑧} ∪ 𝑢) = 𝑣) |
161 | 155, 156,
160 | 3bitr4g 317 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑢 = (𝑣 ∖ {𝑧}) ↔ 𝑣 = (𝑢 ∪ {𝑧}))) |
162 | 161 | 3expib 1119 |
. . . . . . 7
⊢ (𝜑 → (((𝑢 ∈ 𝒫 𝐴 ∧ (♯‘𝑢) = (𝐾 − 1)) ∧ (𝑣 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∧ (𝑧 ∈ 𝑣 ∧ (♯‘𝑣) = 𝐾))) → (𝑢 = (𝑣 ∖ {𝑧}) ↔ 𝑣 = (𝑢 ∪ {𝑧})))) |
163 | 147, 162 | syl5bi 245 |
. . . . . 6
⊢ (𝜑 → ((𝑢 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ∧ 𝑣 ∈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) → (𝑢 = (𝑣 ∖ {𝑧}) ↔ 𝑣 = (𝑢 ∪ {𝑧})))) |
164 | 51, 60, 102, 146, 163 | en3d 8529 |
. . . . 5
⊢ (𝜑 → {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ≈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) |
165 | | ssrab2 4007 |
. . . . . . 7
⊢ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ⊆ 𝒫 𝐴 |
166 | | ssfi 8722 |
. . . . . . 7
⊢
((𝒫 𝐴 ∈
Fin ∧ {𝑥 ∈
𝒫 𝐴 ∣
(♯‘𝑥) = (𝐾 − 1)} ⊆ 𝒫
𝐴) → {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ∈ Fin) |
167 | 49, 165, 166 | sylancl 589 |
. . . . . 6
⊢ (𝜑 → {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ∈ Fin) |
168 | | hashen 13703 |
. . . . . 6
⊢ (({𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ∈ Fin ∧ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ Fin) → ((♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)}) = (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) ↔ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ≈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)})) |
169 | 167, 59, 168 | syl2anc 587 |
. . . . 5
⊢ (𝜑 → ((♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)}) = (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) ↔ {𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)} ≈ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)})) |
170 | 164, 169 | mpbird 260 |
. . . 4
⊢ (𝜑 → (♯‘{𝑥 ∈ 𝒫 𝐴 ∣ (♯‘𝑥) = (𝐾 − 1)}) = (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)})) |
171 | 46, 170 | eqtrd 2833 |
. . 3
⊢ (𝜑 → ((♯‘𝐴)C(𝐾 − 1)) = (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)})) |
172 | 38, 171 | oveq12d 7153 |
. 2
⊢ (𝜑 → (((♯‘𝐴)C𝐾) + ((♯‘𝐴)C(𝐾 − 1))) = ((♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) + (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}))) |
173 | 52 | a1i 11 |
. . . . . 6
⊢ (𝜑 → {𝑧} ∈ Fin) |
174 | | disjsn 4607 |
. . . . . . 7
⊢ ((𝐴 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝐴) |
175 | 13, 174 | sylibr 237 |
. . . . . 6
⊢ (𝜑 → (𝐴 ∩ {𝑧}) = ∅) |
176 | | hashun 13739 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ {𝑧} ∈ Fin ∧ (𝐴 ∩ {𝑧}) = ∅) → (♯‘(𝐴 ∪ {𝑧})) = ((♯‘𝐴) + (♯‘{𝑧}))) |
177 | 47, 173, 175, 176 | syl3anc 1368 |
. . . . 5
⊢ (𝜑 → (♯‘(𝐴 ∪ {𝑧})) = ((♯‘𝐴) + (♯‘{𝑧}))) |
178 | 86 | oveq2i 7146 |
. . . . 5
⊢
((♯‘𝐴) +
(♯‘{𝑧})) =
((♯‘𝐴) +
1) |
179 | 177, 178 | eqtrdi 2849 |
. . . 4
⊢ (𝜑 → (♯‘(𝐴 ∪ {𝑧})) = ((♯‘𝐴) + 1)) |
180 | 179 | oveq1d 7150 |
. . 3
⊢ (𝜑 → ((♯‘(𝐴 ∪ {𝑧}))C𝐾) = (((♯‘𝐴) + 1)C𝐾)) |
181 | | hashcl 13713 |
. . . . 5
⊢ (𝐴 ∈ Fin →
(♯‘𝐴) ∈
ℕ0) |
182 | 47, 181 | syl 17 |
. . . 4
⊢ (𝜑 → (♯‘𝐴) ∈
ℕ0) |
183 | | bcpasc 13677 |
. . . 4
⊢
(((♯‘𝐴)
∈ ℕ0 ∧ 𝐾 ∈ ℤ) →
(((♯‘𝐴)C𝐾) + ((♯‘𝐴)C(𝐾 − 1))) = (((♯‘𝐴) + 1)C𝐾)) |
184 | 182, 7, 183 | syl2anc 587 |
. . 3
⊢ (𝜑 → (((♯‘𝐴)C𝐾) + ((♯‘𝐴)C(𝐾 − 1))) = (((♯‘𝐴) + 1)C𝐾)) |
185 | 180, 184 | eqtr4d 2836 |
. 2
⊢ (𝜑 → ((♯‘(𝐴 ∪ {𝑧}))C𝐾) = (((♯‘𝐴)C𝐾) + ((♯‘𝐴)C(𝐾 − 1)))) |
186 | | pm2.1 894 |
. . . . . . . 8
⊢ (¬
𝑧 ∈ 𝑥 ∨ 𝑧 ∈ 𝑥) |
187 | 186 | biantrur 534 |
. . . . . . 7
⊢
((♯‘𝑥) =
𝐾 ↔ ((¬ 𝑧 ∈ 𝑥 ∨ 𝑧 ∈ 𝑥) ∧ (♯‘𝑥) = 𝐾)) |
188 | | andir 1006 |
. . . . . . 7
⊢ (((¬
𝑧 ∈ 𝑥 ∨ 𝑧 ∈ 𝑥) ∧ (♯‘𝑥) = 𝐾) ↔ ((¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ∨ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾))) |
189 | 187, 188 | bitri 278 |
. . . . . 6
⊢
((♯‘𝑥) =
𝐾 ↔ ((¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ∨ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾))) |
190 | 189 | rabbii 3420 |
. . . . 5
⊢ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (♯‘𝑥) = 𝐾} = {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ∨ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾))} |
191 | | unrab 4226 |
. . . . 5
⊢ ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) = {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ∨ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾))} |
192 | 190, 191 | eqtr4i 2824 |
. . . 4
⊢ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (♯‘𝑥) = 𝐾} = ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) |
193 | 192 | fveq2i 6648 |
. . 3
⊢
(♯‘{𝑥
∈ 𝒫 (𝐴 ∪
{𝑧}) ∣
(♯‘𝑥) = 𝐾}) = (♯‘({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)})) |
194 | | ssrab2 4007 |
. . . . 5
⊢ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ⊆ 𝒫 (𝐴 ∪ {𝑧}) |
195 | | ssfi 8722 |
. . . . 5
⊢
((𝒫 (𝐴 ∪
{𝑧}) ∈ Fin ∧
{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ⊆ 𝒫 (𝐴 ∪ {𝑧})) → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ Fin) |
196 | 56, 194, 195 | sylancl 589 |
. . . 4
⊢ (𝜑 → {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ Fin) |
197 | | inrab 4227 |
. . . . . 6
⊢ ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∩ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) = {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾))} |
198 | | simprl 770 |
. . . . . . . . 9
⊢ (((¬
𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)) → 𝑧 ∈ 𝑥) |
199 | | simpll 766 |
. . . . . . . . 9
⊢ (((¬
𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)) → ¬ 𝑧 ∈ 𝑥) |
200 | 198, 199 | pm2.65i 197 |
. . . . . . . 8
⊢ ¬
((¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)) |
201 | 200 | rgenw 3118 |
. . . . . . 7
⊢
∀𝑥 ∈
𝒫 (𝐴 ∪ {𝑧}) ¬ ((¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)) |
202 | | rabeq0 4292 |
. . . . . . 7
⊢ ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾))} = ∅ ↔ ∀𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ¬ ((¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾))) |
203 | 201, 202 | mpbir 234 |
. . . . . 6
⊢ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ ((¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾) ∧ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾))} = ∅ |
204 | 197, 203 | eqtri 2821 |
. . . . 5
⊢ ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∩ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) = ∅ |
205 | 204 | a1i 11 |
. . . 4
⊢ (𝜑 → ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∩ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) = ∅) |
206 | | hashun 13739 |
. . . 4
⊢ (({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ Fin ∧ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∈ Fin ∧ ({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∩ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) = ∅) → (♯‘({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)})) = ((♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) + (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}))) |
207 | 196, 59, 205, 206 | syl3anc 1368 |
. . 3
⊢ (𝜑 → (♯‘({𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)} ∪ {𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)})) = ((♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) + (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}))) |
208 | 193, 207 | syl5eq 2845 |
. 2
⊢ (𝜑 → (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (♯‘𝑥) = 𝐾}) = ((♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (¬ 𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}) + (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (𝑧 ∈ 𝑥 ∧ (♯‘𝑥) = 𝐾)}))) |
209 | 172, 185,
208 | 3eqtr4d 2843 |
1
⊢ (𝜑 → ((♯‘(𝐴 ∪ {𝑧}))C𝐾) = (♯‘{𝑥 ∈ 𝒫 (𝐴 ∪ {𝑧}) ∣ (♯‘𝑥) = 𝐾})) |