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