# Metamath Proof Explorer

## Theorem neindisj2

Description: A point P belongs to the closure of a set S iff every neighborhood of P meets S . (Contributed by FL, 15-Sep-2013)

Ref Expression
Hypothesis tpnei.1 ${⊢}{X}=\bigcup {J}$
Assertion neindisj2 ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\wedge {P}\in {X}\right)\to \left({P}\in \mathrm{cls}\left({J}\right)\left({S}\right)↔\forall {n}\in \mathrm{nei}\left({J}\right)\left(\left\{{P}\right\}\right)\phantom{\rule{.4em}{0ex}}{n}\cap {S}\ne \varnothing \right)$

### Proof

Step Hyp Ref Expression
1 tpnei.1 ${⊢}{X}=\bigcup {J}$
2 1 elcls ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\wedge {P}\in {X}\right)\to \left({P}\in \mathrm{cls}\left({J}\right)\left({S}\right)↔\forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to {x}\cap {S}\ne \varnothing \right)\right)$
3 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 {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\wedge {x}\subseteq {n}\right)\right)\right)$
4 r19.29r ${⊢}\left(\exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\wedge {x}\subseteq {n}\right)\wedge \forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to {x}\cap {S}\ne \varnothing \right)\right)\to \exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\left(\left({P}\in {x}\wedge {x}\subseteq {n}\right)\wedge \left({P}\in {x}\to {x}\cap {S}\ne \varnothing \right)\right)$
5 pm3.35 ${⊢}\left({P}\in {x}\wedge \left({P}\in {x}\to {x}\cap {S}\ne \varnothing \right)\right)\to {x}\cap {S}\ne \varnothing$
6 ssrin ${⊢}{x}\subseteq {n}\to {x}\cap {S}\subseteq {n}\cap {S}$
7 sseq2 ${⊢}{n}\cap {S}=\varnothing \to \left({x}\cap {S}\subseteq {n}\cap {S}↔{x}\cap {S}\subseteq \varnothing \right)$
8 ss0 ${⊢}{x}\cap {S}\subseteq \varnothing \to {x}\cap {S}=\varnothing$
9 7 8 syl6bi ${⊢}{n}\cap {S}=\varnothing \to \left({x}\cap {S}\subseteq {n}\cap {S}\to {x}\cap {S}=\varnothing \right)$
10 6 9 syl5com ${⊢}{x}\subseteq {n}\to \left({n}\cap {S}=\varnothing \to {x}\cap {S}=\varnothing \right)$
11 10 necon3d ${⊢}{x}\subseteq {n}\to \left({x}\cap {S}\ne \varnothing \to {n}\cap {S}\ne \varnothing \right)$
12 5 11 syl5com ${⊢}\left({P}\in {x}\wedge \left({P}\in {x}\to {x}\cap {S}\ne \varnothing \right)\right)\to \left({x}\subseteq {n}\to {n}\cap {S}\ne \varnothing \right)$
13 12 ex ${⊢}{P}\in {x}\to \left(\left({P}\in {x}\to {x}\cap {S}\ne \varnothing \right)\to \left({x}\subseteq {n}\to {n}\cap {S}\ne \varnothing \right)\right)$
14 13 com23 ${⊢}{P}\in {x}\to \left({x}\subseteq {n}\to \left(\left({P}\in {x}\to {x}\cap {S}\ne \varnothing \right)\to {n}\cap {S}\ne \varnothing \right)\right)$
15 14 imp31 ${⊢}\left(\left({P}\in {x}\wedge {x}\subseteq {n}\right)\wedge \left({P}\in {x}\to {x}\cap {S}\ne \varnothing \right)\right)\to {n}\cap {S}\ne \varnothing$
16 15 rexlimivw ${⊢}\exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\left(\left({P}\in {x}\wedge {x}\subseteq {n}\right)\wedge \left({P}\in {x}\to {x}\cap {S}\ne \varnothing \right)\right)\to {n}\cap {S}\ne \varnothing$
17 4 16 syl ${⊢}\left(\exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\wedge {x}\subseteq {n}\right)\wedge \forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to {x}\cap {S}\ne \varnothing \right)\right)\to {n}\cap {S}\ne \varnothing$
18 17 ex ${⊢}\exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\wedge {x}\subseteq {n}\right)\to \left(\forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to {x}\cap {S}\ne \varnothing \right)\to {n}\cap {S}\ne \varnothing \right)$
19 18 adantl ${⊢}\left({n}\subseteq {X}\wedge \exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\wedge {x}\subseteq {n}\right)\right)\to \left(\forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to {x}\cap {S}\ne \varnothing \right)\to {n}\cap {S}\ne \varnothing \right)$
20 3 19 syl6bi ${⊢}\left({J}\in \mathrm{Top}\wedge {P}\in {X}\right)\to \left({n}\in \mathrm{nei}\left({J}\right)\left(\left\{{P}\right\}\right)\to \left(\forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to {x}\cap {S}\ne \varnothing \right)\to {n}\cap {S}\ne \varnothing \right)\right)$
21 20 3adant2 ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\wedge {P}\in {X}\right)\to \left({n}\in \mathrm{nei}\left({J}\right)\left(\left\{{P}\right\}\right)\to \left(\forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to {x}\cap {S}\ne \varnothing \right)\to {n}\cap {S}\ne \varnothing \right)\right)$
22 21 com23 ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\wedge {P}\in {X}\right)\to \left(\forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to {x}\cap {S}\ne \varnothing \right)\to \left({n}\in \mathrm{nei}\left({J}\right)\left(\left\{{P}\right\}\right)\to {n}\cap {S}\ne \varnothing \right)\right)$
23 22 imp ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\wedge {P}\in {X}\right)\wedge \forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to {x}\cap {S}\ne \varnothing \right)\right)\to \left({n}\in \mathrm{nei}\left({J}\right)\left(\left\{{P}\right\}\right)\to {n}\cap {S}\ne \varnothing \right)$
24 23 ralrimiv ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\wedge {P}\in {X}\right)\wedge \forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to {x}\cap {S}\ne \varnothing \right)\right)\to \forall {n}\in \mathrm{nei}\left({J}\right)\left(\left\{{P}\right\}\right)\phantom{\rule{.4em}{0ex}}{n}\cap {S}\ne \varnothing$
25 opnneip ${⊢}\left({J}\in \mathrm{Top}\wedge {x}\in {J}\wedge {P}\in {x}\right)\to {x}\in \mathrm{nei}\left({J}\right)\left(\left\{{P}\right\}\right)$
26 ineq1 ${⊢}{n}={x}\to {n}\cap {S}={x}\cap {S}$
27 26 neeq1d ${⊢}{n}={x}\to \left({n}\cap {S}\ne \varnothing ↔{x}\cap {S}\ne \varnothing \right)$
28 27 rspccva ${⊢}\left(\forall {n}\in \mathrm{nei}\left({J}\right)\left(\left\{{P}\right\}\right)\phantom{\rule{.4em}{0ex}}{n}\cap {S}\ne \varnothing \wedge {x}\in \mathrm{nei}\left({J}\right)\left(\left\{{P}\right\}\right)\right)\to {x}\cap {S}\ne \varnothing$
29 idd ${⊢}\left({P}\in {X}\wedge \left({J}\in \mathrm{Top}\wedge {x}\in {J}\wedge {P}\in {x}\right)\wedge {S}\subseteq {X}\right)\to \left({x}\cap {S}\ne \varnothing \to {x}\cap {S}\ne \varnothing \right)$
30 29 3exp ${⊢}{P}\in {X}\to \left(\left({J}\in \mathrm{Top}\wedge {x}\in {J}\wedge {P}\in {x}\right)\to \left({S}\subseteq {X}\to \left({x}\cap {S}\ne \varnothing \to {x}\cap {S}\ne \varnothing \right)\right)\right)$
31 30 com14 ${⊢}{x}\cap {S}\ne \varnothing \to \left(\left({J}\in \mathrm{Top}\wedge {x}\in {J}\wedge {P}\in {x}\right)\to \left({S}\subseteq {X}\to \left({P}\in {X}\to {x}\cap {S}\ne \varnothing \right)\right)\right)$
32 28 31 syl ${⊢}\left(\forall {n}\in \mathrm{nei}\left({J}\right)\left(\left\{{P}\right\}\right)\phantom{\rule{.4em}{0ex}}{n}\cap {S}\ne \varnothing \wedge {x}\in \mathrm{nei}\left({J}\right)\left(\left\{{P}\right\}\right)\right)\to \left(\left({J}\in \mathrm{Top}\wedge {x}\in {J}\wedge {P}\in {x}\right)\to \left({S}\subseteq {X}\to \left({P}\in {X}\to {x}\cap {S}\ne \varnothing \right)\right)\right)$
33 32 ex ${⊢}\forall {n}\in \mathrm{nei}\left({J}\right)\left(\left\{{P}\right\}\right)\phantom{\rule{.4em}{0ex}}{n}\cap {S}\ne \varnothing \to \left({x}\in \mathrm{nei}\left({J}\right)\left(\left\{{P}\right\}\right)\to \left(\left({J}\in \mathrm{Top}\wedge {x}\in {J}\wedge {P}\in {x}\right)\to \left({S}\subseteq {X}\to \left({P}\in {X}\to {x}\cap {S}\ne \varnothing \right)\right)\right)\right)$
34 33 com3l ${⊢}{x}\in \mathrm{nei}\left({J}\right)\left(\left\{{P}\right\}\right)\to \left(\left({J}\in \mathrm{Top}\wedge {x}\in {J}\wedge {P}\in {x}\right)\to \left(\forall {n}\in \mathrm{nei}\left({J}\right)\left(\left\{{P}\right\}\right)\phantom{\rule{.4em}{0ex}}{n}\cap {S}\ne \varnothing \to \left({S}\subseteq {X}\to \left({P}\in {X}\to {x}\cap {S}\ne \varnothing \right)\right)\right)\right)$
35 25 34 mpcom ${⊢}\left({J}\in \mathrm{Top}\wedge {x}\in {J}\wedge {P}\in {x}\right)\to \left(\forall {n}\in \mathrm{nei}\left({J}\right)\left(\left\{{P}\right\}\right)\phantom{\rule{.4em}{0ex}}{n}\cap {S}\ne \varnothing \to \left({S}\subseteq {X}\to \left({P}\in {X}\to {x}\cap {S}\ne \varnothing \right)\right)\right)$
36 35 3expia ${⊢}\left({J}\in \mathrm{Top}\wedge {x}\in {J}\right)\to \left({P}\in {x}\to \left(\forall {n}\in \mathrm{nei}\left({J}\right)\left(\left\{{P}\right\}\right)\phantom{\rule{.4em}{0ex}}{n}\cap {S}\ne \varnothing \to \left({S}\subseteq {X}\to \left({P}\in {X}\to {x}\cap {S}\ne \varnothing \right)\right)\right)\right)$
37 36 com25 ${⊢}\left({J}\in \mathrm{Top}\wedge {x}\in {J}\right)\to \left({P}\in {X}\to \left(\forall {n}\in \mathrm{nei}\left({J}\right)\left(\left\{{P}\right\}\right)\phantom{\rule{.4em}{0ex}}{n}\cap {S}\ne \varnothing \to \left({S}\subseteq {X}\to \left({P}\in {x}\to {x}\cap {S}\ne \varnothing \right)\right)\right)\right)$
38 37 ex ${⊢}{J}\in \mathrm{Top}\to \left({x}\in {J}\to \left({P}\in {X}\to \left(\forall {n}\in \mathrm{nei}\left({J}\right)\left(\left\{{P}\right\}\right)\phantom{\rule{.4em}{0ex}}{n}\cap {S}\ne \varnothing \to \left({S}\subseteq {X}\to \left({P}\in {x}\to {x}\cap {S}\ne \varnothing \right)\right)\right)\right)\right)$
39 38 com25 ${⊢}{J}\in \mathrm{Top}\to \left({S}\subseteq {X}\to \left({P}\in {X}\to \left(\forall {n}\in \mathrm{nei}\left({J}\right)\left(\left\{{P}\right\}\right)\phantom{\rule{.4em}{0ex}}{n}\cap {S}\ne \varnothing \to \left({x}\in {J}\to \left({P}\in {x}\to {x}\cap {S}\ne \varnothing \right)\right)\right)\right)\right)$
40 39 3imp1 ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\wedge {P}\in {X}\right)\wedge \forall {n}\in \mathrm{nei}\left({J}\right)\left(\left\{{P}\right\}\right)\phantom{\rule{.4em}{0ex}}{n}\cap {S}\ne \varnothing \right)\to \left({x}\in {J}\to \left({P}\in {x}\to {x}\cap {S}\ne \varnothing \right)\right)$
41 40 ralrimiv ${⊢}\left(\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\wedge {P}\in {X}\right)\wedge \forall {n}\in \mathrm{nei}\left({J}\right)\left(\left\{{P}\right\}\right)\phantom{\rule{.4em}{0ex}}{n}\cap {S}\ne \varnothing \right)\to \forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to {x}\cap {S}\ne \varnothing \right)$
42 24 41 impbida ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\wedge {P}\in {X}\right)\to \left(\forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({P}\in {x}\to {x}\cap {S}\ne \varnothing \right)↔\forall {n}\in \mathrm{nei}\left({J}\right)\left(\left\{{P}\right\}\right)\phantom{\rule{.4em}{0ex}}{n}\cap {S}\ne \varnothing \right)$
43 2 42 bitrd ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\wedge {P}\in {X}\right)\to \left({P}\in \mathrm{cls}\left({J}\right)\left({S}\right)↔\forall {n}\in \mathrm{nei}\left({J}\right)\left(\left\{{P}\right\}\right)\phantom{\rule{.4em}{0ex}}{n}\cap {S}\ne \varnothing \right)$