Theorem clduni

Description: The union of closed sets is the underlying set of the topology (the union of open sets). (Contributed by Zhi Wang, 6-Sep-2024)

	Ref	Expression
Assertion	clduni	$$⊢J\in \mathrm{Top}\to \bigcup \mathrm{Clsd}\left(J\right)=\bigcup J$$

Proof

Step	Hyp	Ref	Expression
1		toptopon2	$$⊢J\in \mathrm{Top}\leftrightarrow J\in \mathrm{TopOn}\left(\bigcup J\right)$$
2	1	biimpi	$$⊢J\in \mathrm{Top}\to J\in \mathrm{TopOn}\left(\bigcup J\right)$$
3		cldmreon	$$⊢J\in \mathrm{TopOn}\left(\bigcup J\right)\to \mathrm{Clsd}\left(J\right)\in \mathrm{Moore}\left(\bigcup J\right)$$
4		mreuni	$$⊢\mathrm{Clsd}\left(J\right)\in \mathrm{Moore}\left(\bigcup J\right)\to \bigcup \mathrm{Clsd}\left(J\right)=\bigcup J$$
5	2 3 4	3syl	$$⊢J\in \mathrm{Top}\to \bigcup \mathrm{Clsd}\left(J\right)=\bigcup J$$