| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | sseq2 4010 | . . . . . . . 8
⊢ (𝑥 = ∪
𝐴 → (𝑦 ⊆ 𝑥 ↔ 𝑦 ⊆ ∪ 𝐴)) | 
| 2 | 1 | biimprcd 250 | . . . . . . 7
⊢ (𝑦 ⊆ ∪ 𝐴
→ (𝑥 = ∪ 𝐴
→ 𝑦 ⊆ 𝑥)) | 
| 3 | 2 | reximdv 3170 | . . . . . 6
⊢ (𝑦 ⊆ ∪ 𝐴
→ (∃𝑥 ∈
𝐴 𝑥 = ∪ 𝐴 → ∃𝑥 ∈ 𝐴 𝑦 ⊆ 𝑥)) | 
| 4 | 3 | com12 32 | . . . . 5
⊢
(∃𝑥 ∈
𝐴 𝑥 = ∪ 𝐴 → (𝑦 ⊆ ∪ 𝐴 → ∃𝑥 ∈ 𝐴 𝑦 ⊆ 𝑥)) | 
| 5 |  | ssiun 5046 | . . . . . 6
⊢
(∃𝑥 ∈
𝐴 𝑦 ⊆ 𝑥 → 𝑦 ⊆ ∪
𝑥 ∈ 𝐴 𝑥) | 
| 6 |  | uniiun 5058 | . . . . . 6
⊢ ∪ 𝐴 =
∪ 𝑥 ∈ 𝐴 𝑥 | 
| 7 | 5, 6 | sseqtrrdi 4025 | . . . . 5
⊢
(∃𝑥 ∈
𝐴 𝑦 ⊆ 𝑥 → 𝑦 ⊆ ∪ 𝐴) | 
| 8 | 4, 7 | impbid1 225 | . . . 4
⊢
(∃𝑥 ∈
𝐴 𝑥 = ∪ 𝐴 → (𝑦 ⊆ ∪ 𝐴 ↔ ∃𝑥 ∈ 𝐴 𝑦 ⊆ 𝑥)) | 
| 9 |  | velpw 4605 | . . . 4
⊢ (𝑦 ∈ 𝒫 ∪ 𝐴
↔ 𝑦 ⊆ ∪ 𝐴) | 
| 10 |  | eliun 4995 | . . . . 5
⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝒫 𝑥 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝒫 𝑥) | 
| 11 |  | velpw 4605 | . . . . . 6
⊢ (𝑦 ∈ 𝒫 𝑥 ↔ 𝑦 ⊆ 𝑥) | 
| 12 | 11 | rexbii 3094 | . . . . 5
⊢
(∃𝑥 ∈
𝐴 𝑦 ∈ 𝒫 𝑥 ↔ ∃𝑥 ∈ 𝐴 𝑦 ⊆ 𝑥) | 
| 13 | 10, 12 | bitri 275 | . . . 4
⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝒫 𝑥 ↔ ∃𝑥 ∈ 𝐴 𝑦 ⊆ 𝑥) | 
| 14 | 8, 9, 13 | 3bitr4g 314 | . . 3
⊢
(∃𝑥 ∈
𝐴 𝑥 = ∪ 𝐴 → (𝑦 ∈ 𝒫 ∪ 𝐴
↔ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝒫 𝑥)) | 
| 15 | 14 | eqrdv 2735 | . 2
⊢
(∃𝑥 ∈
𝐴 𝑥 = ∪ 𝐴 → 𝒫 ∪ 𝐴 =
∪ 𝑥 ∈ 𝐴 𝒫 𝑥) | 
| 16 |  | ssid 4006 | . . . . 5
⊢ ∪ 𝐴
⊆ ∪ 𝐴 | 
| 17 |  | iunpw.1 | . . . . . . . 8
⊢ 𝐴 ∈ V | 
| 18 | 17 | uniex 7761 | . . . . . . 7
⊢ ∪ 𝐴
∈ V | 
| 19 | 18 | elpw 4604 | . . . . . 6
⊢ (∪ 𝐴
∈ 𝒫 ∪ 𝐴 ↔ ∪ 𝐴 ⊆ ∪ 𝐴) | 
| 20 |  | eleq2 2830 | . . . . . 6
⊢
(𝒫 ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 𝒫 𝑥 → (∪ 𝐴 ∈ 𝒫 ∪ 𝐴
↔ ∪ 𝐴 ∈ ∪
𝑥 ∈ 𝐴 𝒫 𝑥)) | 
| 21 | 19, 20 | bitr3id 285 | . . . . 5
⊢
(𝒫 ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 𝒫 𝑥 → (∪ 𝐴 ⊆ ∪ 𝐴
↔ ∪ 𝐴 ∈ ∪
𝑥 ∈ 𝐴 𝒫 𝑥)) | 
| 22 | 16, 21 | mpbii 233 | . . . 4
⊢
(𝒫 ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 𝒫 𝑥 → ∪ 𝐴 ∈ ∪ 𝑥 ∈ 𝐴 𝒫 𝑥) | 
| 23 |  | eliun 4995 | . . . 4
⊢ (∪ 𝐴
∈ ∪ 𝑥 ∈ 𝐴 𝒫 𝑥 ↔ ∃𝑥 ∈ 𝐴 ∪ 𝐴 ∈ 𝒫 𝑥) | 
| 24 | 22, 23 | sylib 218 | . . 3
⊢
(𝒫 ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 𝒫 𝑥 → ∃𝑥 ∈ 𝐴 ∪ 𝐴 ∈ 𝒫 𝑥) | 
| 25 |  | elssuni 4937 | . . . . . . 7
⊢ (𝑥 ∈ 𝐴 → 𝑥 ⊆ ∪ 𝐴) | 
| 26 |  | elpwi 4607 | . . . . . . 7
⊢ (∪ 𝐴
∈ 𝒫 𝑥 →
∪ 𝐴 ⊆ 𝑥) | 
| 27 | 25, 26 | anim12i 613 | . . . . . 6
⊢ ((𝑥 ∈ 𝐴 ∧ ∪ 𝐴 ∈ 𝒫 𝑥) → (𝑥 ⊆ ∪ 𝐴 ∧ ∪ 𝐴
⊆ 𝑥)) | 
| 28 |  | eqss 3999 | . . . . . 6
⊢ (𝑥 = ∪
𝐴 ↔ (𝑥 ⊆ ∪ 𝐴
∧ ∪ 𝐴 ⊆ 𝑥)) | 
| 29 | 27, 28 | sylibr 234 | . . . . 5
⊢ ((𝑥 ∈ 𝐴 ∧ ∪ 𝐴 ∈ 𝒫 𝑥) → 𝑥 = ∪ 𝐴) | 
| 30 | 29 | ex 412 | . . . 4
⊢ (𝑥 ∈ 𝐴 → (∪ 𝐴 ∈ 𝒫 𝑥 → 𝑥 = ∪ 𝐴)) | 
| 31 | 30 | reximia 3081 | . . 3
⊢
(∃𝑥 ∈
𝐴 ∪ 𝐴
∈ 𝒫 𝑥 →
∃𝑥 ∈ 𝐴 𝑥 = ∪ 𝐴) | 
| 32 | 24, 31 | syl 17 | . 2
⊢
(𝒫 ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 𝒫 𝑥 → ∃𝑥 ∈ 𝐴 𝑥 = ∪ 𝐴) | 
| 33 | 15, 32 | impbii 209 | 1
⊢
(∃𝑥 ∈
𝐴 𝑥 = ∪ 𝐴 ↔ 𝒫 ∪ 𝐴 =
∪ 𝑥 ∈ 𝐴 𝒫 𝑥) |