Theorem clstop

Description: The closure of a topology's underlying set is the entire set. (Contributed by NM, 5-Oct-2007) (Proof shortened by Jim Kingdon, 11-Mar-2023)

	Ref	Expression
Hypothesis	clscld.1	$$⊢X=\bigcup J$$
Assertion	clstop	$$⊢J\in \mathrm{Top}\to \mathrm{cls}\left(J\right)\left(X\right)=X$$

Proof

Step	Hyp	Ref	Expression
1		clscld.1	$$⊢X=\bigcup J$$
2	1	topcld	$$⊢J\in \mathrm{Top}\to X\in \mathrm{Clsd}\left(J\right)$$
3		cldcls	$$⊢X\in \mathrm{Clsd}\left(J\right)\to \mathrm{cls}\left(J\right)\left(X\right)=X$$
4	2 3	syl	$$⊢J\in \mathrm{Top}\to \mathrm{cls}\left(J\right)\left(X\right)=X$$