# Metamath Proof Explorer

## Theorem neindisj

Description: Any neighborhood of an element in the closure of a subset intersects the subset. Part of proof of Theorem 6.6 of Munkres p. 97. (Contributed by NM, 26-Feb-2007)

Ref Expression
Hypothesis neips.1 ${⊢}{X}=\bigcup {J}$
Assertion neindisj ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge \left({P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\wedge {N}\in \mathrm{nei}\left({J}\right)\left(\left\{{P}\right\}\right)\right)\right)\to {N}\cap {S}\ne \varnothing$

### Proof

Step Hyp Ref Expression
1 neips.1 ${⊢}{X}=\bigcup {J}$
2 1 clsss3 ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to \mathrm{cls}\left({J}\right)\left({S}\right)\subseteq {X}$
3 2 sseld ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to \left({P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\to {P}\in {X}\right)$
4 3 impr ${⊢}\left({J}\in \mathrm{Top}\wedge \left({S}\subseteq {X}\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\right)\to {P}\in {X}$
5 1 isneip ${⊢}\left({J}\in \mathrm{Top}\wedge {P}\in {X}\right)\to \left({N}\in \mathrm{nei}\left({J}\right)\left(\left\{{P}\right\}\right)↔\left({N}\subseteq {X}\wedge \exists {g}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {g}\wedge {g}\subseteq {N}\right)\right)\right)$
6 4 5 syldan ${⊢}\left({J}\in \mathrm{Top}\wedge \left({S}\subseteq {X}\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\right)\to \left({N}\in \mathrm{nei}\left({J}\right)\left(\left\{{P}\right\}\right)↔\left({N}\subseteq {X}\wedge \exists {g}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {g}\wedge {g}\subseteq {N}\right)\right)\right)$
7 3anass ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)↔\left({J}\in \mathrm{Top}\wedge \left({S}\subseteq {X}\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\right)$
8 1 clsndisj ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\wedge \left({g}\in {J}\wedge {P}\in {g}\right)\right)\to {g}\cap {S}\ne \varnothing$
9 7 8 sylanbr ${⊢}\left(\left({J}\in \mathrm{Top}\wedge \left({S}\subseteq {X}\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\right)\wedge \left({g}\in {J}\wedge {P}\in {g}\right)\right)\to {g}\cap {S}\ne \varnothing$
10 9 anassrs ${⊢}\left(\left(\left({J}\in \mathrm{Top}\wedge \left({S}\subseteq {X}\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\right)\wedge {g}\in {J}\right)\wedge {P}\in {g}\right)\to {g}\cap {S}\ne \varnothing$
11 10 adantllr ${⊢}\left(\left(\left(\left({J}\in \mathrm{Top}\wedge \left({S}\subseteq {X}\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\right)\wedge {N}\subseteq {X}\right)\wedge {g}\in {J}\right)\wedge {P}\in {g}\right)\to {g}\cap {S}\ne \varnothing$
12 11 adantrr ${⊢}\left(\left(\left(\left({J}\in \mathrm{Top}\wedge \left({S}\subseteq {X}\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\right)\wedge {N}\subseteq {X}\right)\wedge {g}\in {J}\right)\wedge \left({P}\in {g}\wedge {g}\subseteq {N}\right)\right)\to {g}\cap {S}\ne \varnothing$
13 ssdisj ${⊢}\left({g}\subseteq {N}\wedge {N}\cap {S}=\varnothing \right)\to {g}\cap {S}=\varnothing$
14 13 ex ${⊢}{g}\subseteq {N}\to \left({N}\cap {S}=\varnothing \to {g}\cap {S}=\varnothing \right)$
15 14 necon3d ${⊢}{g}\subseteq {N}\to \left({g}\cap {S}\ne \varnothing \to {N}\cap {S}\ne \varnothing \right)$
16 15 ad2antll ${⊢}\left(\left(\left(\left({J}\in \mathrm{Top}\wedge \left({S}\subseteq {X}\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\right)\wedge {N}\subseteq {X}\right)\wedge {g}\in {J}\right)\wedge \left({P}\in {g}\wedge {g}\subseteq {N}\right)\right)\to \left({g}\cap {S}\ne \varnothing \to {N}\cap {S}\ne \varnothing \right)$
17 12 16 mpd ${⊢}\left(\left(\left(\left({J}\in \mathrm{Top}\wedge \left({S}\subseteq {X}\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\right)\wedge {N}\subseteq {X}\right)\wedge {g}\in {J}\right)\wedge \left({P}\in {g}\wedge {g}\subseteq {N}\right)\right)\to {N}\cap {S}\ne \varnothing$
18 17 rexlimdva2 ${⊢}\left(\left({J}\in \mathrm{Top}\wedge \left({S}\subseteq {X}\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\right)\wedge {N}\subseteq {X}\right)\to \left(\exists {g}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {g}\wedge {g}\subseteq {N}\right)\to {N}\cap {S}\ne \varnothing \right)$
19 18 expimpd ${⊢}\left({J}\in \mathrm{Top}\wedge \left({S}\subseteq {X}\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\right)\to \left(\left({N}\subseteq {X}\wedge \exists {g}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {g}\wedge {g}\subseteq {N}\right)\right)\to {N}\cap {S}\ne \varnothing \right)$
20 6 19 sylbid ${⊢}\left({J}\in \mathrm{Top}\wedge \left({S}\subseteq {X}\wedge {P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\right)\right)\to \left({N}\in \mathrm{nei}\left({J}\right)\left(\left\{{P}\right\}\right)\to {N}\cap {S}\ne \varnothing \right)$
21 20 exp32 ${⊢}{J}\in \mathrm{Top}\to \left({S}\subseteq {X}\to \left({P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\to \left({N}\in \mathrm{nei}\left({J}\right)\left(\left\{{P}\right\}\right)\to {N}\cap {S}\ne \varnothing \right)\right)\right)$
22 21 imp43 ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\wedge \left({P}\in \mathrm{cls}\left({J}\right)\left({S}\right)\wedge {N}\in \mathrm{nei}\left({J}\right)\left(\left\{{P}\right\}\right)\right)\right)\to {N}\cap {S}\ne \varnothing$