Step | Hyp | Ref
| Expression |
1 | | pwundif 4945 |
. 2
⊢ 𝒫
(𝑏 ∪ {𝑥}) = ((𝒫 (𝑏 ∪ {𝑥}) ∖ 𝒫 𝑏) ∪ 𝒫 𝑏) |
2 | | vex 3176 |
. . . . . . . . 9
⊢ 𝑐 ∈ V |
3 | | snex 4835 |
. . . . . . . . 9
⊢ {𝑥} ∈ V |
4 | 2, 3 | unex 6854 |
. . . . . . . 8
⊢ (𝑐 ∪ {𝑥}) ∈ V |
5 | | pwfilem.1 |
. . . . . . . 8
⊢ 𝐹 = (𝑐 ∈ 𝒫 𝑏 ↦ (𝑐 ∪ {𝑥})) |
6 | 4, 5 | fnmpti 5935 |
. . . . . . 7
⊢ 𝐹 Fn 𝒫 𝑏 |
7 | | dffn4 6034 |
. . . . . . 7
⊢ (𝐹 Fn 𝒫 𝑏 ↔ 𝐹:𝒫 𝑏–onto→ran 𝐹) |
8 | 6, 7 | mpbi 219 |
. . . . . 6
⊢ 𝐹:𝒫 𝑏–onto→ran 𝐹 |
9 | | fodomfi 8124 |
. . . . . 6
⊢
((𝒫 𝑏 ∈
Fin ∧ 𝐹:𝒫 𝑏–onto→ran 𝐹) → ran 𝐹 ≼ 𝒫 𝑏) |
10 | 8, 9 | mpan2 703 |
. . . . 5
⊢
(𝒫 𝑏 ∈
Fin → ran 𝐹 ≼
𝒫 𝑏) |
11 | | domfi 8066 |
. . . . 5
⊢
((𝒫 𝑏 ∈
Fin ∧ ran 𝐹 ≼
𝒫 𝑏) → ran
𝐹 ∈
Fin) |
12 | 10, 11 | mpdan 699 |
. . . 4
⊢
(𝒫 𝑏 ∈
Fin → ran 𝐹 ∈
Fin) |
13 | | eldifi 3694 |
. . . . . . . . 9
⊢ (𝑑 ∈ (𝒫 (𝑏 ∪ {𝑥}) ∖ 𝒫 𝑏) → 𝑑 ∈ 𝒫 (𝑏 ∪ {𝑥})) |
14 | 3 | elpwun 6869 |
. . . . . . . . 9
⊢ (𝑑 ∈ 𝒫 (𝑏 ∪ {𝑥}) ↔ (𝑑 ∖ {𝑥}) ∈ 𝒫 𝑏) |
15 | 13, 14 | sylib 207 |
. . . . . . . 8
⊢ (𝑑 ∈ (𝒫 (𝑏 ∪ {𝑥}) ∖ 𝒫 𝑏) → (𝑑 ∖ {𝑥}) ∈ 𝒫 𝑏) |
16 | | undif1 3995 |
. . . . . . . . 9
⊢ ((𝑑 ∖ {𝑥}) ∪ {𝑥}) = (𝑑 ∪ {𝑥}) |
17 | | elpwunsn 4171 |
. . . . . . . . . . 11
⊢ (𝑑 ∈ (𝒫 (𝑏 ∪ {𝑥}) ∖ 𝒫 𝑏) → 𝑥 ∈ 𝑑) |
18 | 17 | snssd 4281 |
. . . . . . . . . 10
⊢ (𝑑 ∈ (𝒫 (𝑏 ∪ {𝑥}) ∖ 𝒫 𝑏) → {𝑥} ⊆ 𝑑) |
19 | | ssequn2 3748 |
. . . . . . . . . 10
⊢ ({𝑥} ⊆ 𝑑 ↔ (𝑑 ∪ {𝑥}) = 𝑑) |
20 | 18, 19 | sylib 207 |
. . . . . . . . 9
⊢ (𝑑 ∈ (𝒫 (𝑏 ∪ {𝑥}) ∖ 𝒫 𝑏) → (𝑑 ∪ {𝑥}) = 𝑑) |
21 | 16, 20 | syl5req 2657 |
. . . . . . . 8
⊢ (𝑑 ∈ (𝒫 (𝑏 ∪ {𝑥}) ∖ 𝒫 𝑏) → 𝑑 = ((𝑑 ∖ {𝑥}) ∪ {𝑥})) |
22 | | uneq1 3722 |
. . . . . . . . . 10
⊢ (𝑐 = (𝑑 ∖ {𝑥}) → (𝑐 ∪ {𝑥}) = ((𝑑 ∖ {𝑥}) ∪ {𝑥})) |
23 | 22 | eqeq2d 2620 |
. . . . . . . . 9
⊢ (𝑐 = (𝑑 ∖ {𝑥}) → (𝑑 = (𝑐 ∪ {𝑥}) ↔ 𝑑 = ((𝑑 ∖ {𝑥}) ∪ {𝑥}))) |
24 | 23 | rspcev 3282 |
. . . . . . . 8
⊢ (((𝑑 ∖ {𝑥}) ∈ 𝒫 𝑏 ∧ 𝑑 = ((𝑑 ∖ {𝑥}) ∪ {𝑥})) → ∃𝑐 ∈ 𝒫 𝑏𝑑 = (𝑐 ∪ {𝑥})) |
25 | 15, 21, 24 | syl2anc 691 |
. . . . . . 7
⊢ (𝑑 ∈ (𝒫 (𝑏 ∪ {𝑥}) ∖ 𝒫 𝑏) → ∃𝑐 ∈ 𝒫 𝑏𝑑 = (𝑐 ∪ {𝑥})) |
26 | 5, 4 | elrnmpti 5297 |
. . . . . . 7
⊢ (𝑑 ∈ ran 𝐹 ↔ ∃𝑐 ∈ 𝒫 𝑏𝑑 = (𝑐 ∪ {𝑥})) |
27 | 25, 26 | sylibr 223 |
. . . . . 6
⊢ (𝑑 ∈ (𝒫 (𝑏 ∪ {𝑥}) ∖ 𝒫 𝑏) → 𝑑 ∈ ran 𝐹) |
28 | 27 | ssriv 3572 |
. . . . 5
⊢
(𝒫 (𝑏 ∪
{𝑥}) ∖ 𝒫
𝑏) ⊆ ran 𝐹 |
29 | | ssdomg 7887 |
. . . . 5
⊢ (ran
𝐹 ∈ Fin →
((𝒫 (𝑏 ∪ {𝑥}) ∖ 𝒫 𝑏) ⊆ ran 𝐹 → (𝒫 (𝑏 ∪ {𝑥}) ∖ 𝒫 𝑏) ≼ ran 𝐹)) |
30 | 12, 28, 29 | mpisyl 21 |
. . . 4
⊢
(𝒫 𝑏 ∈
Fin → (𝒫 (𝑏
∪ {𝑥}) ∖
𝒫 𝑏) ≼ ran
𝐹) |
31 | | domfi 8066 |
. . . 4
⊢ ((ran
𝐹 ∈ Fin ∧
(𝒫 (𝑏 ∪ {𝑥}) ∖ 𝒫 𝑏) ≼ ran 𝐹) → (𝒫 (𝑏 ∪ {𝑥}) ∖ 𝒫 𝑏) ∈ Fin) |
32 | 12, 30, 31 | syl2anc 691 |
. . 3
⊢
(𝒫 𝑏 ∈
Fin → (𝒫 (𝑏
∪ {𝑥}) ∖
𝒫 𝑏) ∈
Fin) |
33 | | unfi 8112 |
. . 3
⊢
(((𝒫 (𝑏
∪ {𝑥}) ∖
𝒫 𝑏) ∈ Fin
∧ 𝒫 𝑏 ∈
Fin) → ((𝒫 (𝑏
∪ {𝑥}) ∖
𝒫 𝑏) ∪
𝒫 𝑏) ∈
Fin) |
34 | 32, 33 | mpancom 700 |
. 2
⊢
(𝒫 𝑏 ∈
Fin → ((𝒫 (𝑏
∪ {𝑥}) ∖
𝒫 𝑏) ∪
𝒫 𝑏) ∈
Fin) |
35 | 1, 34 | syl5eqel 2692 |
1
⊢
(𝒫 𝑏 ∈
Fin → 𝒫 (𝑏
∪ {𝑥}) ∈
Fin) |