# Metamath Proof Explorer

## Theorem clslp

Description: The closure of a subset of a topological space is the subset together with its limit points. Theorem 6.6 of Munkres p. 97. (Contributed by NM, 26-Feb-2007)

Ref Expression
Hypothesis lpfval.1 ${⊢}{X}=\bigcup {J}$
Assertion clslp ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to \mathrm{cls}\left({J}\right)\left({S}\right)={S}\cup \mathrm{limPt}\left({J}\right)\left({S}\right)$

### Proof

Step Hyp Ref Expression
1 lpfval.1 ${⊢}{X}=\bigcup {J}$
2 1 neindisj ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge \left({x}\in \mathrm{cls}\left({J}\right)\left({S}\right)\wedge {n}\in \mathrm{nei}\left({J}\right)\left(\left\{{x}\right\}\right)\right)\right)\to {n}\cap {S}\ne \varnothing$
3 2 expr ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {x}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\to \left({n}\in \mathrm{nei}\left({J}\right)\left(\left\{{x}\right\}\right)\to {n}\cap {S}\ne \varnothing \right)$
4 3 adantr ${⊢}\left(\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {x}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge ¬{x}\in {S}\right)\to \left({n}\in \mathrm{nei}\left({J}\right)\left(\left\{{x}\right\}\right)\to {n}\cap {S}\ne \varnothing \right)$
5 difsn ${⊢}¬{x}\in {S}\to {S}\setminus \left\{{x}\right\}={S}$
6 5 ineq2d ${⊢}¬{x}\in {S}\to {n}\cap \left({S}\setminus \left\{{x}\right\}\right)={n}\cap {S}$
7 6 neeq1d ${⊢}¬{x}\in {S}\to \left({n}\cap \left({S}\setminus \left\{{x}\right\}\right)\ne \varnothing ↔{n}\cap {S}\ne \varnothing \right)$
8 7 adantl ${⊢}\left(\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {x}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge ¬{x}\in {S}\right)\to \left({n}\cap \left({S}\setminus \left\{{x}\right\}\right)\ne \varnothing ↔{n}\cap {S}\ne \varnothing \right)$
9 4 8 sylibrd ${⊢}\left(\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {x}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge ¬{x}\in {S}\right)\to \left({n}\in \mathrm{nei}\left({J}\right)\left(\left\{{x}\right\}\right)\to {n}\cap \left({S}\setminus \left\{{x}\right\}\right)\ne \varnothing \right)$
10 9 ex ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {x}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\to \left(¬{x}\in {S}\to \left({n}\in \mathrm{nei}\left({J}\right)\left(\left\{{x}\right\}\right)\to {n}\cap \left({S}\setminus \left\{{x}\right\}\right)\ne \varnothing \right)\right)$
11 10 ralrimdv ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {x}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\to \left(¬{x}\in {S}\to \forall {n}\in \mathrm{nei}\left({J}\right)\left(\left\{{x}\right\}\right)\phantom{\rule{.4em}{0ex}}{n}\cap \left({S}\setminus \left\{{x}\right\}\right)\ne \varnothing \right)$
12 simpll ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {x}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\to {J}\in \mathrm{Top}$
13 simplr ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {x}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\to {S}\subseteq {X}$
14 1 clsss3 ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to \mathrm{cls}\left({J}\right)\left({S}\right)\subseteq {X}$
15 14 sselda ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {x}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\to {x}\in {X}$
16 1 islp2 ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\wedge {x}\in {X}\right)\to \left({x}\in \mathrm{limPt}\left({J}\right)\left({S}\right)↔\forall {n}\in \mathrm{nei}\left({J}\right)\left(\left\{{x}\right\}\right)\phantom{\rule{.4em}{0ex}}{n}\cap \left({S}\setminus \left\{{x}\right\}\right)\ne \varnothing \right)$
17 12 13 15 16 syl3anc ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {x}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\to \left({x}\in \mathrm{limPt}\left({J}\right)\left({S}\right)↔\forall {n}\in \mathrm{nei}\left({J}\right)\left(\left\{{x}\right\}\right)\phantom{\rule{.4em}{0ex}}{n}\cap \left({S}\setminus \left\{{x}\right\}\right)\ne \varnothing \right)$
18 11 17 sylibrd ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {x}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\to \left(¬{x}\in {S}\to {x}\in \mathrm{limPt}\left({J}\right)\left({S}\right)\right)$
19 18 orrd ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {x}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\to \left({x}\in {S}\vee {x}\in \mathrm{limPt}\left({J}\right)\left({S}\right)\right)$
20 elun ${⊢}{x}\in \left({S}\cup \mathrm{limPt}\left({J}\right)\left({S}\right)\right)↔\left({x}\in {S}\vee {x}\in \mathrm{limPt}\left({J}\right)\left({S}\right)\right)$
21 19 20 sylibr ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge {x}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\to {x}\in \left({S}\cup \mathrm{limPt}\left({J}\right)\left({S}\right)\right)$
22 21 ex ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to \left({x}\in \mathrm{cls}\left({J}\right)\left({S}\right)\to {x}\in \left({S}\cup \mathrm{limPt}\left({J}\right)\left({S}\right)\right)\right)$
23 22 ssrdv ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to \mathrm{cls}\left({J}\right)\left({S}\right)\subseteq {S}\cup \mathrm{limPt}\left({J}\right)\left({S}\right)$
24 1 sscls ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to {S}\subseteq \mathrm{cls}\left({J}\right)\left({S}\right)$
25 1 lpsscls ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to \mathrm{limPt}\left({J}\right)\left({S}\right)\subseteq \mathrm{cls}\left({J}\right)\left({S}\right)$
26 24 25 unssd ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to {S}\cup \mathrm{limPt}\left({J}\right)\left({S}\right)\subseteq \mathrm{cls}\left({J}\right)\left({S}\right)$
27 23 26 eqssd ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to \mathrm{cls}\left({J}\right)\left({S}\right)={S}\cup \mathrm{limPt}\left({J}\right)\left({S}\right)$