Metamath Proof Explorer


Theorem sn0cld

Description: The closed sets of the topology { (/) } . (Contributed by FL, 5-Jan-2009)

Ref Expression
Assertion sn0cld ( Clsd ‘ { ∅ } ) = { ∅ }

Proof

Step Hyp Ref Expression
1 0ex ∅ ∈ V
2 discld ( ∅ ∈ V → ( Clsd ‘ 𝒫 ∅ ) = 𝒫 ∅ )
3 1 2 ax-mp ( Clsd ‘ 𝒫 ∅ ) = 𝒫 ∅
4 pw0 𝒫 ∅ = { ∅ }
5 4 fveq2i ( Clsd ‘ 𝒫 ∅ ) = ( Clsd ‘ { ∅ } )
6 3 5 4 3eqtr3i ( Clsd ‘ { ∅ } ) = { ∅ }