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	$⊢ X = ⋃ J$
	Assertion	cldlp	$⊢ (J \in Top \land S \subseteq X) \to (S \in Clsd (J) \leftrightarrow limPt (J) (S) \subseteq S)$

Proof

Step	Hyp	Ref	Expression
1		lpfval.1	$⊢ X = ⋃ J$
2	1	iscld3	$⊢ (J \in Top \land S \subseteq X) \to (S \in Clsd (J) \leftrightarrow cls (J) (S) = S)$
3	1	clslp	$⊢ (J \in Top \land S \subseteq X) \to cls (J) (S) = S \cup limPt (J) (S)$
4	3	eqeq1d	$⊢ (J \in Top \land S \subseteq X) \to (cls (J) (S) = S \leftrightarrow S \cup limPt (J) (S) = S)$
5		ssequn2	$⊢ limPt (J) (S) \subseteq S \leftrightarrow S \cup limPt (J) (S) = S$
6	4 5	bitr4di	$⊢ (J \in Top \land S \subseteq X) \to (cls (J) (S) = S \leftrightarrow limPt (J) (S) \subseteq S)$
7	2 6	bitrd	$⊢ (J \in Top \land S \subseteq X) \to (S \in Clsd (J) \leftrightarrow limPt (J) (S) \subseteq S)$