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 =