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