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 ) =/= (/) )