Theorem unicls

Description: The union of the closed set is the underlying set of the topology. (Contributed by Thierry Arnoux, 21-Sep-2017)

	Ref	Expression
Hypotheses	unicls.1	$$⊢J\in \mathrm{Top}$$
	unicls.2	$$⊢X=\bigcup J$$
Assertion	unicls	$$⊢\bigcup \mathrm{Clsd}\left(J\right)=X$$

Proof

Step	Hyp	Ref	Expression
1		unicls.1	$$⊢J\in \mathrm{Top}$$
2		unicls.2	$$⊢X=\bigcup J$$
3	2	cldss2	$$⊢\mathrm{Clsd}\left(J\right)\subseteq 𝒫X$$
4		sspwuni	$$⊢\mathrm{Clsd}\left(J\right)\subseteq 𝒫X\leftrightarrow \bigcup \mathrm{Clsd}\left(J\right)\subseteq X$$
5	3 4	mpbi	$$⊢\bigcup \mathrm{Clsd}\left(J\right)\subseteq X$$
6	2	topcld	$$⊢J\in \mathrm{Top}\to X\in \mathrm{Clsd}\left(J\right)$$
7	1 6	ax-mp	$$⊢X\in \mathrm{Clsd}\left(J\right)$$
8		unissel	$$⊢\left(\bigcup \mathrm{Clsd}\left(J\right)\subseteq X\wedge X\in \mathrm{Clsd}\left(J\right)\right)\to \bigcup \mathrm{Clsd}\left(J\right)=X$$
9	5 7 8	mp2an	$$⊢\bigcup \mathrm{Clsd}\left(J\right)=X$$