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 = U. J
Assertion neindisj
|- ( ( ( J e. Top /\ S C_ X ) /\ ( P e. ( ( cls ` J ) ` S ) /\ N e. ( ( nei ` J ) ` { P } ) ) ) -> ( N i^i S ) =/= (/) )

Proof

Step Hyp Ref Expression
1 neips.1
 |-  X = U. J
2 1 clsss3
 |-  ( ( J e. Top /\ S C_ X ) -> ( ( cls ` J ) ` S ) C_ X )
3 2 sseld
 |-  ( ( J e. Top /\ S C_ X ) -> ( P e. ( ( cls ` J ) ` S ) -> P e. X ) )
4 3 impr
 |-  ( ( J e. Top /\ ( S C_ X /\ P e. ( ( cls ` J ) ` S ) ) ) -> P e. X )
5 1 isneip
 |-  ( ( J e. Top /\ P e. X ) -> ( N e. ( ( nei ` J ) ` { P } ) <-> ( N C_ X /\ E. g e. J ( P e. g /\ g C_ N ) ) ) )
6 4 5 syldan
 |-  ( ( J e. Top /\ ( S C_ X /\ P e. ( ( cls ` J ) ` S ) ) ) -> ( N e. ( ( nei ` J ) ` { P } ) <-> ( N C_ X /\ E. g e. J ( P e. g /\ g C_ N ) ) ) )
7 3anass
 |-  ( ( J e. Top /\ S C_ X /\ P e. ( ( cls ` J ) ` S ) ) <-> ( J e. Top /\ ( S C_ X /\ P e. ( ( cls ` J ) ` S ) ) ) )
8 1 clsndisj
 |-  ( ( ( J e. Top /\ S C_ X /\ P e. ( ( cls ` J ) ` S ) ) /\ ( g e. J /\ P e. g ) ) -> ( g i^i S ) =/= (/) )
9 7 8 sylanbr
 |-  ( ( ( J e. Top /\ ( S C_ X /\ P e. ( ( cls ` J ) ` S ) ) ) /\ ( g e. J /\ P e. g ) ) -> ( g i^i S ) =/= (/) )
10 9 anassrs
 |-  ( ( ( ( J e. Top /\ ( S C_ X /\ P e. ( ( cls ` J ) ` S ) ) ) /\ g e. J ) /\ P e. g ) -> ( g i^i S ) =/= (/) )
11 10 adantllr
 |-  ( ( ( ( ( J e. Top /\ ( S C_ X /\ P e. ( ( cls ` J ) ` S ) ) ) /\ N C_ X ) /\ g e. J ) /\ P e. g ) -> ( g i^i S ) =/= (/) )
12 11 adantrr
 |-  ( ( ( ( ( J e. Top /\ ( S C_ X /\ P e. ( ( cls ` J ) ` S ) ) ) /\ N C_ X ) /\ g e. J ) /\ ( P e. g /\ g C_ N ) ) -> ( g i^i S ) =/= (/) )
13 ssdisj
 |-  ( ( g C_ N /\ ( N i^i S ) = (/) ) -> ( g i^i S ) = (/) )
14 13 ex
 |-  ( g C_ N -> ( ( N i^i S ) = (/) -> ( g i^i S ) = (/) ) )
15 14 necon3d
 |-  ( g C_ N -> ( ( g i^i S ) =/= (/) -> ( N i^i S ) =/= (/) ) )
16 15 ad2antll
 |-  ( ( ( ( ( J e. Top /\ ( S C_ X /\ P e. ( ( cls ` J ) ` S ) ) ) /\ N C_ X ) /\ g e. J ) /\ ( P e. g /\ g C_ N ) ) -> ( ( g i^i S ) =/= (/) -> ( N i^i S ) =/= (/) ) )
17 12 16 mpd
 |-  ( ( ( ( ( J e. Top /\ ( S C_ X /\ P e. ( ( cls ` J ) ` S ) ) ) /\ N C_ X ) /\ g e. J ) /\ ( P e. g /\ g C_ N ) ) -> ( N i^i S ) =/= (/) )
18 17 rexlimdva2
 |-  ( ( ( J e. Top /\ ( S C_ X /\ P e. ( ( cls ` J ) ` S ) ) ) /\ N C_ X ) -> ( E. g e. J ( P e. g /\ g C_ N ) -> ( N i^i S ) =/= (/) ) )
19 18 expimpd
 |-  ( ( J e. Top /\ ( S C_ X /\ P e. ( ( cls ` J ) ` S ) ) ) -> ( ( N C_ X /\ E. g e. J ( P e. g /\ g C_ N ) ) -> ( N i^i S ) =/= (/) ) )
20 6 19 sylbid
 |-  ( ( J e. Top /\ ( S C_ X /\ P e. ( ( cls ` J ) ` S ) ) ) -> ( N e. ( ( nei ` J ) ` { P } ) -> ( N i^i S ) =/= (/) ) )
21 20 exp32
 |-  ( J e. Top -> ( S C_ X -> ( P e. ( ( cls ` J ) ` S ) -> ( N e. ( ( nei ` J ) ` { P } ) -> ( N i^i S ) =/= (/) ) ) ) )
22 21 imp43
 |-  ( ( ( J e. Top /\ S C_ X ) /\ ( P e. ( ( cls ` J ) ` S ) /\ N e. ( ( nei ` J ) ` { P } ) ) ) -> ( N i^i S ) =/= (/) )