| Step | Hyp | Ref
| Expression |
| 1 | | uniss 4915 |
. . . . . 6
⊢ (𝑥 ⊆ 𝒫 𝐴 → ∪ 𝑥
⊆ ∪ 𝒫 𝐴) |
| 2 | | unipw 5455 |
. . . . . 6
⊢ ∪ 𝒫 𝐴 = 𝐴 |
| 3 | 1, 2 | sseqtrdi 4024 |
. . . . 5
⊢ (𝑥 ⊆ 𝒫 𝐴 → ∪ 𝑥
⊆ 𝐴) |
| 4 | | vuniex 7759 |
. . . . . 6
⊢ ∪ 𝑥
∈ V |
| 5 | 4 | elpw 4604 |
. . . . 5
⊢ (∪ 𝑥
∈ 𝒫 𝐴 ↔
∪ 𝑥 ⊆ 𝐴) |
| 6 | 3, 5 | sylibr 234 |
. . . 4
⊢ (𝑥 ⊆ 𝒫 𝐴 → ∪ 𝑥
∈ 𝒫 𝐴) |
| 7 | 6 | ax-gen 1795 |
. . 3
⊢
∀𝑥(𝑥 ⊆ 𝒫 𝐴 → ∪ 𝑥
∈ 𝒫 𝐴) |
| 8 | 7 | a1i 11 |
. 2
⊢ (𝐴 ∈ 𝑉 → ∀𝑥(𝑥 ⊆ 𝒫 𝐴 → ∪ 𝑥 ∈ 𝒫 𝐴)) |
| 9 | | velpw 4605 |
. . . . . 6
⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴) |
| 10 | | velpw 4605 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝒫 𝐴 ↔ 𝑦 ⊆ 𝐴) |
| 11 | | ssinss1 4246 |
. . . . . . . . . 10
⊢ (𝑥 ⊆ 𝐴 → (𝑥 ∩ 𝑦) ⊆ 𝐴) |
| 12 | 11 | a1i 11 |
. . . . . . . . 9
⊢ (𝑦 ⊆ 𝐴 → (𝑥 ⊆ 𝐴 → (𝑥 ∩ 𝑦) ⊆ 𝐴)) |
| 13 | | vex 3484 |
. . . . . . . . . . 11
⊢ 𝑦 ∈ V |
| 14 | 13 | inex2 5318 |
. . . . . . . . . 10
⊢ (𝑥 ∩ 𝑦) ∈ V |
| 15 | 14 | elpw 4604 |
. . . . . . . . 9
⊢ ((𝑥 ∩ 𝑦) ∈ 𝒫 𝐴 ↔ (𝑥 ∩ 𝑦) ⊆ 𝐴) |
| 16 | 12, 15 | imbitrrdi 252 |
. . . . . . . 8
⊢ (𝑦 ⊆ 𝐴 → (𝑥 ⊆ 𝐴 → (𝑥 ∩ 𝑦) ∈ 𝒫 𝐴)) |
| 17 | 10, 16 | sylbi 217 |
. . . . . . 7
⊢ (𝑦 ∈ 𝒫 𝐴 → (𝑥 ⊆ 𝐴 → (𝑥 ∩ 𝑦) ∈ 𝒫 𝐴)) |
| 18 | 17 | com12 32 |
. . . . . 6
⊢ (𝑥 ⊆ 𝐴 → (𝑦 ∈ 𝒫 𝐴 → (𝑥 ∩ 𝑦) ∈ 𝒫 𝐴)) |
| 19 | 9, 18 | sylbi 217 |
. . . . 5
⊢ (𝑥 ∈ 𝒫 𝐴 → (𝑦 ∈ 𝒫 𝐴 → (𝑥 ∩ 𝑦) ∈ 𝒫 𝐴)) |
| 20 | 19 | ralrimiv 3145 |
. . . 4
⊢ (𝑥 ∈ 𝒫 𝐴 → ∀𝑦 ∈ 𝒫 𝐴(𝑥 ∩ 𝑦) ∈ 𝒫 𝐴) |
| 21 | 20 | rgen 3063 |
. . 3
⊢
∀𝑥 ∈
𝒫 𝐴∀𝑦 ∈ 𝒫 𝐴(𝑥 ∩ 𝑦) ∈ 𝒫 𝐴 |
| 22 | 21 | a1i 11 |
. 2
⊢ (𝐴 ∈ 𝑉 → ∀𝑥 ∈ 𝒫 𝐴∀𝑦 ∈ 𝒫 𝐴(𝑥 ∩ 𝑦) ∈ 𝒫 𝐴) |
| 23 | | pwexg 5378 |
. . 3
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V) |
| 24 | | istopg 22901 |
. . 3
⊢
(𝒫 𝐴 ∈
V → (𝒫 𝐴
∈ Top ↔ (∀𝑥(𝑥 ⊆ 𝒫 𝐴 → ∪ 𝑥 ∈ 𝒫 𝐴) ∧ ∀𝑥 ∈ 𝒫 𝐴∀𝑦 ∈ 𝒫 𝐴(𝑥 ∩ 𝑦) ∈ 𝒫 𝐴))) |
| 25 | 23, 24 | syl 17 |
. 2
⊢ (𝐴 ∈ 𝑉 → (𝒫 𝐴 ∈ Top ↔ (∀𝑥(𝑥 ⊆ 𝒫 𝐴 → ∪ 𝑥 ∈ 𝒫 𝐴) ∧ ∀𝑥 ∈ 𝒫 𝐴∀𝑦 ∈ 𝒫 𝐴(𝑥 ∩ 𝑦) ∈ 𝒫 𝐴))) |
| 26 | 8, 22, 25 | mpbir2and 713 |
1
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ Top) |