Step |
Hyp |
Ref |
Expression |
1 |
|
rabssab |
⊢ { 𝑦 ∈ Top ∣ 𝐴 = ∪ 𝑦 } ⊆ { 𝑦 ∣ 𝐴 = ∪ 𝑦 } |
2 |
|
eqcom |
⊢ ( 𝐴 = ∪ 𝑦 ↔ ∪ 𝑦 = 𝐴 ) |
3 |
2
|
abbii |
⊢ { 𝑦 ∣ 𝐴 = ∪ 𝑦 } = { 𝑦 ∣ ∪ 𝑦 = 𝐴 } |
4 |
1 3
|
sseqtri |
⊢ { 𝑦 ∈ Top ∣ 𝐴 = ∪ 𝑦 } ⊆ { 𝑦 ∣ ∪ 𝑦 = 𝐴 } |
5 |
|
pwpwssunieq |
⊢ { 𝑦 ∣ ∪ 𝑦 = 𝐴 } ⊆ 𝒫 𝒫 𝐴 |
6 |
4 5
|
sstri |
⊢ { 𝑦 ∈ Top ∣ 𝐴 = ∪ 𝑦 } ⊆ 𝒫 𝒫 𝐴 |
7 |
|
pwexg |
⊢ ( 𝐴 ∈ V → 𝒫 𝐴 ∈ V ) |
8 |
7
|
pwexd |
⊢ ( 𝐴 ∈ V → 𝒫 𝒫 𝐴 ∈ V ) |
9 |
|
ssexg |
⊢ ( ( { 𝑦 ∈ Top ∣ 𝐴 = ∪ 𝑦 } ⊆ 𝒫 𝒫 𝐴 ∧ 𝒫 𝒫 𝐴 ∈ V ) → { 𝑦 ∈ Top ∣ 𝐴 = ∪ 𝑦 } ∈ V ) |
10 |
6 8 9
|
sylancr |
⊢ ( 𝐴 ∈ V → { 𝑦 ∈ Top ∣ 𝐴 = ∪ 𝑦 } ∈ V ) |
11 |
|
eqeq1 |
⊢ ( 𝑥 = 𝐴 → ( 𝑥 = ∪ 𝑦 ↔ 𝐴 = ∪ 𝑦 ) ) |
12 |
11
|
rabbidv |
⊢ ( 𝑥 = 𝐴 → { 𝑦 ∈ Top ∣ 𝑥 = ∪ 𝑦 } = { 𝑦 ∈ Top ∣ 𝐴 = ∪ 𝑦 } ) |
13 |
|
df-topon |
⊢ TopOn = ( 𝑥 ∈ V ↦ { 𝑦 ∈ Top ∣ 𝑥 = ∪ 𝑦 } ) |
14 |
12 13
|
fvmptg |
⊢ ( ( 𝐴 ∈ V ∧ { 𝑦 ∈ Top ∣ 𝐴 = ∪ 𝑦 } ∈ V ) → ( TopOn ‘ 𝐴 ) = { 𝑦 ∈ Top ∣ 𝐴 = ∪ 𝑦 } ) |
15 |
10 14
|
mpdan |
⊢ ( 𝐴 ∈ V → ( TopOn ‘ 𝐴 ) = { 𝑦 ∈ Top ∣ 𝐴 = ∪ 𝑦 } ) |
16 |
15 6
|
eqsstrdi |
⊢ ( 𝐴 ∈ V → ( TopOn ‘ 𝐴 ) ⊆ 𝒫 𝒫 𝐴 ) |
17 |
|
fvprc |
⊢ ( ¬ 𝐴 ∈ V → ( TopOn ‘ 𝐴 ) = ∅ ) |
18 |
|
0ss |
⊢ ∅ ⊆ 𝒫 𝒫 𝐴 |
19 |
17 18
|
eqsstrdi |
⊢ ( ¬ 𝐴 ∈ V → ( TopOn ‘ 𝐴 ) ⊆ 𝒫 𝒫 𝐴 ) |
20 |
16 19
|
pm2.61i |
⊢ ( TopOn ‘ 𝐴 ) ⊆ 𝒫 𝒫 𝐴 |