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

Metamath Proof Explorer

Theorem sn0cld

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

		Ref	Expression
	Assertion	sn0cld	$⊢ Clsd (\{\emptyset\}) = \{\emptyset\}$

Step	Hyp	Ref	Expression
1		0ex	$⊢ \emptyset \in V$
2		discld	$⊢ \emptyset \in V \to Clsd (𝒫 \emptyset) = 𝒫 \emptyset$
3	1 2	ax-mp	$⊢ Clsd (𝒫 \emptyset) = 𝒫 \emptyset$
4		pw0	$⊢ 𝒫 \emptyset = \{\emptyset\}$
5	4	fveq2i	$⊢ Clsd (𝒫 \emptyset) = Clsd (\{\emptyset\})$
6	3 5 4	3eqtr3i	$⊢ Clsd (\{\emptyset\}) = \{\emptyset\}$