Theorem 0cld

Description: The empty set is closed. Part of Theorem 6.1(1) of Munkres p. 93. (Contributed by NM, 4-Oct-2006)

	Ref	Expression
Assertion	0cld	$$⊢J\in \mathrm{Top}\to \varnothing \in \mathrm{Clsd}\left(J\right)$$

Proof

Step	Hyp	Ref	Expression
1		dif0	$$⊢\bigcup J\setminus \varnothing =\bigcup J$$
2	1	topopn	$$⊢J\in \mathrm{Top}\to \bigcup J\setminus \varnothing \in J$$
3		0ss	$$⊢\varnothing \subseteq \bigcup J$$
4		eqid	$$⊢\bigcup J=\bigcup J$$
5	4	iscld2	$$⊢\left(J\in \mathrm{Top}\wedge \varnothing \subseteq \bigcup J\right)\to \left(\varnothing \in \mathrm{Clsd}\left(J\right)\leftrightarrow \bigcup J\setminus \varnothing \in J\right)$$
6	3 5	mpan2	$$⊢J\in \mathrm{Top}\to \left(\varnothing \in \mathrm{Clsd}\left(J\right)\leftrightarrow \bigcup J\setminus \varnothing \in J\right)$$
7	2 6	mpbird	$$⊢J\in \mathrm{Top}\to \varnothing \in \mathrm{Clsd}\left(J\right)$$