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	⊢ 𝑋 = ∪ 𝐽
Assertion	clstop	⊢ ( 𝐽 ∈ Top → ( ( cls ‘ 𝐽 ) ‘ 𝑋 ) = 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		clscld.1	⊢ 𝑋 = ∪ 𝐽
2	1	topcld	⊢ ( 𝐽 ∈ Top → 𝑋 ∈ ( Clsd ‘ 𝐽 ) )
3		cldcls	⊢ ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑋 ) = 𝑋 )
4	2 3	syl	⊢ ( 𝐽 ∈ Top → ( ( cls ‘ 𝐽 ) ‘ 𝑋 ) = 𝑋 )