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 ‘ { ∅ } ) = { ∅ }