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 Top S X S Clsd J limPt J S S

Proof

Step Hyp Ref Expression
1 lpfval.1 X = J
2 1 iscld3 J Top S X S Clsd J cls J S = S
3 1 clslp J Top S X cls J S = S limPt J S
4 3 eqeq1d J Top S X cls J S = S S limPt J S = S
5 ssequn2 limPt J S S S limPt J S = S
6 4 5 bitr4di J Top S X cls J S = S limPt J S S
7 2 6 bitrd J Top S X S Clsd J limPt J S S