This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cldlp

Description: A subset of a topological space is closed iff it contains all its limit points. Corollary 6.7 of Munkres p. 97. (Contributed by NM, 26-Feb-2007)

		Ref	Expression
	Hypothesis	lpfval.1	⊢ 𝑋 = ∪ 𝐽
	Assertion	cldlp	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) ↔ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		lpfval.1	⊢ 𝑋 = ∪ 𝐽
2	1	iscld3	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) ↔ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) = 𝑆 ) )
3	1	clslp	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) = ( 𝑆 ∪ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ) )
4	3	eqeq1d	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) = 𝑆 ↔ ( 𝑆 ∪ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ) = 𝑆 ) )
5		ssequn2	⊢ ( ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝑆 ↔ ( 𝑆 ∪ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ) = 𝑆 )
6	4 5	bitr4di	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) = 𝑆 ↔ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝑆 ) )
7	2 6	bitrd	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) ↔ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝑆 ) )