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	⊢ 𝐽 ∈ Top
	unicls.2	⊢ 𝑋 = ∪ 𝐽
Assertion	unicls	⊢ ∪ ( Clsd ‘ 𝐽 ) = 𝑋

Proof

Step	Hyp	Ref	Expression
1		unicls.1	⊢ 𝐽 ∈ Top
2		unicls.2	⊢ 𝑋 = ∪ 𝐽
3	2	cldss2	⊢ ( Clsd ‘ 𝐽 ) ⊆ 𝒫 𝑋
4		sspwuni	⊢ ( ( Clsd ‘ 𝐽 ) ⊆ 𝒫 𝑋 ↔ ∪ ( Clsd ‘ 𝐽 ) ⊆ 𝑋 )
5	3 4	mpbi	⊢ ∪ ( Clsd ‘ 𝐽 ) ⊆ 𝑋
6	2	topcld	⊢ ( 𝐽 ∈ Top → 𝑋 ∈ ( Clsd ‘ 𝐽 ) )
7	1 6	ax-mp	⊢ 𝑋 ∈ ( Clsd ‘ 𝐽 )
8		unissel	⊢ ( ( ∪ ( Clsd ‘ 𝐽 ) ⊆ 𝑋 ∧ 𝑋 ∈ ( Clsd ‘ 𝐽 ) ) → ∪ ( Clsd ‘ 𝐽 ) = 𝑋 )
9	5 7 8	mp2an	⊢ ∪ ( Clsd ‘ 𝐽 ) = 𝑋