This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem toponsspwpw

Description: The set of topologies on a set is included in the double power set of that set. (Contributed by BJ, 29-Apr-2021)

Ref Expression
Assertion toponsspwpw ( TopOn ‘ 𝐴 ) ⊆ 𝒫 𝒫 𝐴

Proof

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 ‘ 𝐴 ) ⊆ 𝒫 𝒫 𝐴