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

Proof

Step Hyp Ref Expression
1 tpnei.1
 |-  X = U. J
2 1 elcls
 |-  ( ( J e. Top /\ S C_ X /\ P e. X ) -> ( P e. ( ( cls ` J ) ` S ) <-> A. x e. J ( P e. x -> ( x i^i S ) =/= (/) ) ) )
3 1 isneip
 |-  ( ( J e. Top /\ P e. X ) -> ( n e. ( ( nei ` J ) ` { P } ) <-> ( n C_ X /\ E. x e. J ( P e. x /\ x C_ n ) ) ) )
4 r19.29r
 |-  ( ( E. x e. J ( P e. x /\ x C_ n ) /\ A. x e. J ( P e. x -> ( x i^i S ) =/= (/) ) ) -> E. x e. J ( ( P e. x /\ x C_ n ) /\ ( P e. x -> ( x i^i S ) =/= (/) ) ) )
5 pm3.35
 |-  ( ( P e. x /\ ( P e. x -> ( x i^i S ) =/= (/) ) ) -> ( x i^i S ) =/= (/) )
6 ssrin
 |-  ( x C_ n -> ( x i^i S ) C_ ( n i^i S ) )
7 sseq2
 |-  ( ( n i^i S ) = (/) -> ( ( x i^i S ) C_ ( n i^i S ) <-> ( x i^i S ) C_ (/) ) )
8 ss0
 |-  ( ( x i^i S ) C_ (/) -> ( x i^i S ) = (/) )
9 7 8 syl6bi
 |-  ( ( n i^i S ) = (/) -> ( ( x i^i S ) C_ ( n i^i S ) -> ( x i^i S ) = (/) ) )
10 6 9 syl5com
 |-  ( x C_ n -> ( ( n i^i S ) = (/) -> ( x i^i S ) = (/) ) )
11 10 necon3d
 |-  ( x C_ n -> ( ( x i^i S ) =/= (/) -> ( n i^i S ) =/= (/) ) )
12 5 11 syl5com
 |-  ( ( P e. x /\ ( P e. x -> ( x i^i S ) =/= (/) ) ) -> ( x C_ n -> ( n i^i S ) =/= (/) ) )
13 12 ex
 |-  ( P e. x -> ( ( P e. x -> ( x i^i S ) =/= (/) ) -> ( x C_ n -> ( n i^i S ) =/= (/) ) ) )
14 13 com23
 |-  ( P e. x -> ( x C_ n -> ( ( P e. x -> ( x i^i S ) =/= (/) ) -> ( n i^i S ) =/= (/) ) ) )
15 14 imp31
 |-  ( ( ( P e. x /\ x C_ n ) /\ ( P e. x -> ( x i^i S ) =/= (/) ) ) -> ( n i^i S ) =/= (/) )
16 15 rexlimivw
 |-  ( E. x e. J ( ( P e. x /\ x C_ n ) /\ ( P e. x -> ( x i^i S ) =/= (/) ) ) -> ( n i^i S ) =/= (/) )
17 4 16 syl
 |-  ( ( E. x e. J ( P e. x /\ x C_ n ) /\ A. x e. J ( P e. x -> ( x i^i S ) =/= (/) ) ) -> ( n i^i S ) =/= (/) )
18 17 ex
 |-  ( E. x e. J ( P e. x /\ x C_ n ) -> ( A. x e. J ( P e. x -> ( x i^i S ) =/= (/) ) -> ( n i^i S ) =/= (/) ) )
19 18 adantl
 |-  ( ( n C_ X /\ E. x e. J ( P e. x /\ x C_ n ) ) -> ( A. x e. J ( P e. x -> ( x i^i S ) =/= (/) ) -> ( n i^i S ) =/= (/) ) )
20 3 19 syl6bi
 |-  ( ( J e. Top /\ P e. X ) -> ( n e. ( ( nei ` J ) ` { P } ) -> ( A. x e. J ( P e. x -> ( x i^i S ) =/= (/) ) -> ( n i^i S ) =/= (/) ) ) )
21 20 3adant2
 |-  ( ( J e. Top /\ S C_ X /\ P e. X ) -> ( n e. ( ( nei ` J ) ` { P } ) -> ( A. x e. J ( P e. x -> ( x i^i S ) =/= (/) ) -> ( n i^i S ) =/= (/) ) ) )
22 21 com23
 |-  ( ( J e. Top /\ S C_ X /\ P e. X ) -> ( A. x e. J ( P e. x -> ( x i^i S ) =/= (/) ) -> ( n e. ( ( nei ` J ) ` { P } ) -> ( n i^i S ) =/= (/) ) ) )
23 22 imp
 |-  ( ( ( J e. Top /\ S C_ X /\ P e. X ) /\ A. x e. J ( P e. x -> ( x i^i S ) =/= (/) ) ) -> ( n e. ( ( nei ` J ) ` { P } ) -> ( n i^i S ) =/= (/) ) )
24 23 ralrimiv
 |-  ( ( ( J e. Top /\ S C_ X /\ P e. X ) /\ A. x e. J ( P e. x -> ( x i^i S ) =/= (/) ) ) -> A. n e. ( ( nei ` J ) ` { P } ) ( n i^i S ) =/= (/) )
25 opnneip
 |-  ( ( J e. Top /\ x e. J /\ P e. x ) -> x e. ( ( nei ` J ) ` { P } ) )
26 ineq1
 |-  ( n = x -> ( n i^i S ) = ( x i^i S ) )
27 26 neeq1d
 |-  ( n = x -> ( ( n i^i S ) =/= (/) <-> ( x i^i S ) =/= (/) ) )
28 27 rspccva
 |-  ( ( A. n e. ( ( nei ` J ) ` { P } ) ( n i^i S ) =/= (/) /\ x e. ( ( nei ` J ) ` { P } ) ) -> ( x i^i S ) =/= (/) )
29 idd
 |-  ( ( P e. X /\ ( J e. Top /\ x e. J /\ P e. x ) /\ S C_ X ) -> ( ( x i^i S ) =/= (/) -> ( x i^i S ) =/= (/) ) )
30 29 3exp
 |-  ( P e. X -> ( ( J e. Top /\ x e. J /\ P e. x ) -> ( S C_ X -> ( ( x i^i S ) =/= (/) -> ( x i^i S ) =/= (/) ) ) ) )
31 30 com14
 |-  ( ( x i^i S ) =/= (/) -> ( ( J e. Top /\ x e. J /\ P e. x ) -> ( S C_ X -> ( P e. X -> ( x i^i S ) =/= (/) ) ) ) )
32 28 31 syl
 |-  ( ( A. n e. ( ( nei ` J ) ` { P } ) ( n i^i S ) =/= (/) /\ x e. ( ( nei ` J ) ` { P } ) ) -> ( ( J e. Top /\ x e. J /\ P e. x ) -> ( S C_ X -> ( P e. X -> ( x i^i S ) =/= (/) ) ) ) )
33 32 ex
 |-  ( A. n e. ( ( nei ` J ) ` { P } ) ( n i^i S ) =/= (/) -> ( x e. ( ( nei ` J ) ` { P } ) -> ( ( J e. Top /\ x e. J /\ P e. x ) -> ( S C_ X -> ( P e. X -> ( x i^i S ) =/= (/) ) ) ) ) )
34 33 com3l
 |-  ( x e. ( ( nei ` J ) ` { P } ) -> ( ( J e. Top /\ x e. J /\ P e. x ) -> ( A. n e. ( ( nei ` J ) ` { P } ) ( n i^i S ) =/= (/) -> ( S C_ X -> ( P e. X -> ( x i^i S ) =/= (/) ) ) ) ) )
35 25 34 mpcom
 |-  ( ( J e. Top /\ x e. J /\ P e. x ) -> ( A. n e. ( ( nei ` J ) ` { P } ) ( n i^i S ) =/= (/) -> ( S C_ X -> ( P e. X -> ( x i^i S ) =/= (/) ) ) ) )
36 35 3expia
 |-  ( ( J e. Top /\ x e. J ) -> ( P e. x -> ( A. n e. ( ( nei ` J ) ` { P } ) ( n i^i S ) =/= (/) -> ( S C_ X -> ( P e. X -> ( x i^i S ) =/= (/) ) ) ) ) )
37 36 com25
 |-  ( ( J e. Top /\ x e. J ) -> ( P e. X -> ( A. n e. ( ( nei ` J ) ` { P } ) ( n i^i S ) =/= (/) -> ( S C_ X -> ( P e. x -> ( x i^i S ) =/= (/) ) ) ) ) )
38 37 ex
 |-  ( J e. Top -> ( x e. J -> ( P e. X -> ( A. n e. ( ( nei ` J ) ` { P } ) ( n i^i S ) =/= (/) -> ( S C_ X -> ( P e. x -> ( x i^i S ) =/= (/) ) ) ) ) ) )
39 38 com25
 |-  ( J e. Top -> ( S C_ X -> ( P e. X -> ( A. n e. ( ( nei ` J ) ` { P } ) ( n i^i S ) =/= (/) -> ( x e. J -> ( P e. x -> ( x i^i S ) =/= (/) ) ) ) ) ) )
40 39 3imp1
 |-  ( ( ( J e. Top /\ S C_ X /\ P e. X ) /\ A. n e. ( ( nei ` J ) ` { P } ) ( n i^i S ) =/= (/) ) -> ( x e. J -> ( P e. x -> ( x i^i S ) =/= (/) ) ) )
41 40 ralrimiv
 |-  ( ( ( J e. Top /\ S C_ X /\ P e. X ) /\ A. n e. ( ( nei ` J ) ` { P } ) ( n i^i S ) =/= (/) ) -> A. x e. J ( P e. x -> ( x i^i S ) =/= (/) ) )
42 24 41 impbida
 |-  ( ( J e. Top /\ S C_ X /\ P e. X ) -> ( A. x e. J ( P e. x -> ( x i^i S ) =/= (/) ) <-> A. n e. ( ( nei ` J ) ` { P } ) ( n i^i S ) =/= (/) ) )
43 2 42 bitrd
 |-  ( ( J e. Top /\ S C_ X /\ P e. X ) -> ( P e. ( ( cls ` J ) ` S ) <-> A. n e. ( ( nei ` J ) ` { P } ) ( n i^i S ) =/= (/) ) )