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	⊢ ( 𝐽 ∈ Top → ∪ ( Clsd ‘ 𝐽 ) = ∪ 𝐽 )

Proof

Step	Hyp	Ref	Expression
1		toptopon2	⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
2	1	biimpi	⊢ ( 𝐽 ∈ Top → 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
3		cldmreon	⊢ ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) → ( Clsd ‘ 𝐽 ) ∈ ( Moore ‘ ∪ 𝐽 ) )
4		mreuni	⊢ ( ( Clsd ‘ 𝐽 ) ∈ ( Moore ‘ ∪ 𝐽 ) → ∪ ( Clsd ‘ 𝐽 ) = ∪ 𝐽 )
5	2 3 4	3syl	⊢ ( 𝐽 ∈ Top → ∪ ( Clsd ‘ 𝐽 ) = ∪ 𝐽 )