| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | pwundif 4624 | . 2
⊢ 𝒫
(𝑏 ∪ {𝑥}) = ((𝒫 (𝑏 ∪ {𝑥}) ∖ 𝒫 𝑏) ∪ 𝒫 𝑏) | 
| 2 |  | pwfilem.1 | . . . . . 6
⊢ 𝐹 = (𝑐 ∈ 𝒫 𝑏 ↦ (𝑐 ∪ {𝑥})) | 
| 3 | 2 | funmpt2 6605 | . . . . 5
⊢ Fun 𝐹 | 
| 4 |  | vex 3484 | . . . . . . . . . 10
⊢ 𝑐 ∈ V | 
| 5 |  | vsnex 5434 | . . . . . . . . . 10
⊢ {𝑥} ∈ V | 
| 6 | 4, 5 | unex 7764 | . . . . . . . . 9
⊢ (𝑐 ∪ {𝑥}) ∈ V | 
| 7 | 6, 2 | dmmpti 6712 | . . . . . . . 8
⊢ dom 𝐹 = 𝒫 𝑏 | 
| 8 | 7 | imaeq2i 6076 | . . . . . . 7
⊢ (𝐹 “ dom 𝐹) = (𝐹 “ 𝒫 𝑏) | 
| 9 |  | imadmrn 6088 | . . . . . . 7
⊢ (𝐹 “ dom 𝐹) = ran 𝐹 | 
| 10 | 8, 9 | eqtr3i 2767 | . . . . . 6
⊢ (𝐹 “ 𝒫 𝑏) = ran 𝐹 | 
| 11 |  | imafi 9353 | . . . . . 6
⊢ ((Fun
𝐹 ∧ 𝒫 𝑏 ∈ Fin) → (𝐹 “ 𝒫 𝑏) ∈ Fin) | 
| 12 | 10, 11 | eqeltrrid 2846 | . . . . 5
⊢ ((Fun
𝐹 ∧ 𝒫 𝑏 ∈ Fin) → ran 𝐹 ∈ Fin) | 
| 13 | 3, 12 | mpan 690 | . . . 4
⊢
(𝒫 𝑏 ∈
Fin → ran 𝐹 ∈
Fin) | 
| 14 |  | eldifi 4131 | . . . . . . . 8
⊢ (𝑑 ∈ (𝒫 (𝑏 ∪ {𝑥}) ∖ 𝒫 𝑏) → 𝑑 ∈ 𝒫 (𝑏 ∪ {𝑥})) | 
| 15 | 5 | elpwun 7789 | . . . . . . . 8
⊢ (𝑑 ∈ 𝒫 (𝑏 ∪ {𝑥}) ↔ (𝑑 ∖ {𝑥}) ∈ 𝒫 𝑏) | 
| 16 | 14, 15 | sylib 218 | . . . . . . 7
⊢ (𝑑 ∈ (𝒫 (𝑏 ∪ {𝑥}) ∖ 𝒫 𝑏) → (𝑑 ∖ {𝑥}) ∈ 𝒫 𝑏) | 
| 17 |  | undif1 4476 | . . . . . . . 8
⊢ ((𝑑 ∖ {𝑥}) ∪ {𝑥}) = (𝑑 ∪ {𝑥}) | 
| 18 |  | elpwunsn 4684 | . . . . . . . . . 10
⊢ (𝑑 ∈ (𝒫 (𝑏 ∪ {𝑥}) ∖ 𝒫 𝑏) → 𝑥 ∈ 𝑑) | 
| 19 | 18 | snssd 4809 | . . . . . . . . 9
⊢ (𝑑 ∈ (𝒫 (𝑏 ∪ {𝑥}) ∖ 𝒫 𝑏) → {𝑥} ⊆ 𝑑) | 
| 20 |  | ssequn2 4189 | . . . . . . . . 9
⊢ ({𝑥} ⊆ 𝑑 ↔ (𝑑 ∪ {𝑥}) = 𝑑) | 
| 21 | 19, 20 | sylib 218 | . . . . . . . 8
⊢ (𝑑 ∈ (𝒫 (𝑏 ∪ {𝑥}) ∖ 𝒫 𝑏) → (𝑑 ∪ {𝑥}) = 𝑑) | 
| 22 | 17, 21 | eqtr2id 2790 | . . . . . . 7
⊢ (𝑑 ∈ (𝒫 (𝑏 ∪ {𝑥}) ∖ 𝒫 𝑏) → 𝑑 = ((𝑑 ∖ {𝑥}) ∪ {𝑥})) | 
| 23 |  | uneq1 4161 | . . . . . . . 8
⊢ (𝑐 = (𝑑 ∖ {𝑥}) → (𝑐 ∪ {𝑥}) = ((𝑑 ∖ {𝑥}) ∪ {𝑥})) | 
| 24 | 23 | rspceeqv 3645 | . . . . . . 7
⊢ (((𝑑 ∖ {𝑥}) ∈ 𝒫 𝑏 ∧ 𝑑 = ((𝑑 ∖ {𝑥}) ∪ {𝑥})) → ∃𝑐 ∈ 𝒫 𝑏𝑑 = (𝑐 ∪ {𝑥})) | 
| 25 | 16, 22, 24 | syl2anc 584 | . . . . . 6
⊢ (𝑑 ∈ (𝒫 (𝑏 ∪ {𝑥}) ∖ 𝒫 𝑏) → ∃𝑐 ∈ 𝒫 𝑏𝑑 = (𝑐 ∪ {𝑥})) | 
| 26 | 2, 25, 14 | elrnmptd 5974 | . . . . 5
⊢ (𝑑 ∈ (𝒫 (𝑏 ∪ {𝑥}) ∖ 𝒫 𝑏) → 𝑑 ∈ ran 𝐹) | 
| 27 | 26 | ssriv 3987 | . . . 4
⊢
(𝒫 (𝑏 ∪
{𝑥}) ∖ 𝒫
𝑏) ⊆ ran 𝐹 | 
| 28 |  | ssfi 9213 | . . . 4
⊢ ((ran
𝐹 ∈ Fin ∧
(𝒫 (𝑏 ∪ {𝑥}) ∖ 𝒫 𝑏) ⊆ ran 𝐹) → (𝒫 (𝑏 ∪ {𝑥}) ∖ 𝒫 𝑏) ∈ Fin) | 
| 29 | 13, 27, 28 | sylancl 586 | . . 3
⊢
(𝒫 𝑏 ∈
Fin → (𝒫 (𝑏
∪ {𝑥}) ∖
𝒫 𝑏) ∈
Fin) | 
| 30 |  | unfi 9211 | . . 3
⊢
(((𝒫 (𝑏
∪ {𝑥}) ∖
𝒫 𝑏) ∈ Fin
∧ 𝒫 𝑏 ∈
Fin) → ((𝒫 (𝑏
∪ {𝑥}) ∖
𝒫 𝑏) ∪
𝒫 𝑏) ∈
Fin) | 
| 31 | 29, 30 | mpancom 688 | . 2
⊢
(𝒫 𝑏 ∈
Fin → ((𝒫 (𝑏
∪ {𝑥}) ∖
𝒫 𝑏) ∪
𝒫 𝑏) ∈
Fin) | 
| 32 | 1, 31 | eqeltrid 2845 | 1
⊢
(𝒫 𝑏 ∈
Fin → 𝒫 (𝑏
∪ {𝑥}) ∈
Fin) |