Theorem topcld

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

	Ref	Expression
Hypothesis	iscld.1	$$⊢X=\bigcup J$$
Assertion	topcld	$$⊢J\in \mathrm{Top}\to X\in \mathrm{Clsd}\left(J\right)$$

Proof

Step	Hyp	Ref	Expression
1		iscld.1	$$⊢X=\bigcup J$$
2		difid	$$⊢X\setminus X=\varnothing$$
3		0opn	$$⊢J\in \mathrm{Top}\to \varnothing \in J$$
4	2 3	eqeltrid	$$⊢J\in \mathrm{Top}\to X\setminus X\in J$$
5		ssid	$$⊢X\subseteq X$$
6	4 5	jctil	$$⊢J\in \mathrm{Top}\to \left(X\subseteq X\wedge X\setminus X\in J\right)$$
7	1	iscld	$$⊢J\in \mathrm{Top}\to \left(X\in \mathrm{Clsd}\left(J\right)\leftrightarrow \left(X\subseteq X\wedge X\setminus X\in J\right)\right)$$
8	6 7	mpbird	$$⊢J\in \mathrm{Top}\to X\in \mathrm{Clsd}\left(J\right)$$