This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem neibl

Description: The neighborhoods around a point P of a metric space are those subsets containing a ball around P . Definition of neighborhood in Kreyszig p. 19. (Contributed by NM, 8-Nov-2007) (Revised by Mario Carneiro, 23-Dec-2013)

Ref Expression
Hypothesis mopni.1 
|- J = ( MetOpen ` D )
Assertion neibl 
|- ( ( D e. ( *Met ` X ) /\ P e. X ) -> ( N e. ( ( nei ` J ) ` { P } ) <-> ( N C_ X /\ E. r e. RR+ ( P ( ball ` D ) r ) C_ N ) ) )

Proof

Step Hyp Ref Expression
1 mopni.1 
 |-  J = ( MetOpen ` D )
2 1 mopntop 
 |-  ( D e. ( *Met ` X ) -> J e. Top )
3 2 adantr 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X ) -> J e. Top )
4 1 mopnuni 
 |-  ( D e. ( *Met ` X ) -> X = U. J )
5 4 eleq2d 
 |-  ( D e. ( *Met ` X ) -> ( P e. X <-> P e. U. J ) )
6 5 biimpa 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X ) -> P e. U. J )
7 eqid 
 |-  U. J = U. J
8 7 isneip 
 |-  ( ( J e. Top /\ P e. U. J ) -> ( N e. ( ( nei ` J ) ` { P } ) <-> ( N C_ U. J /\ E. y e. J ( P e. y /\ y C_ N ) ) ) )
9 3 6 8 syl2anc 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X ) -> ( N e. ( ( nei ` J ) ` { P } ) <-> ( N C_ U. J /\ E. y e. J ( P e. y /\ y C_ N ) ) ) )
10 4 sseq2d 
 |-  ( D e. ( *Met ` X ) -> ( N C_ X <-> N C_ U. J ) )
11 10 adantr 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X ) -> ( N C_ X <-> N C_ U. J ) )
12 11 anbi1d 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X ) -> ( ( N C_ X /\ E. y e. J ( P e. y /\ y C_ N ) ) <-> ( N C_ U. J /\ E. y e. J ( P e. y /\ y C_ N ) ) ) )
13 1 mopni2 
 |-  ( ( D e. ( *Met ` X ) /\ y e. J /\ P e. y ) -> E. r e. RR+ ( P ( ball ` D ) r ) C_ y )
14 sstr2 
 |-  ( ( P ( ball ` D ) r ) C_ y -> ( y C_ N -> ( P ( ball ` D ) r ) C_ N ) )
15 14 com12 
 |-  ( y C_ N -> ( ( P ( ball ` D ) r ) C_ y -> ( P ( ball ` D ) r ) C_ N ) )
16 15 reximdv 
 |-  ( y C_ N -> ( E. r e. RR+ ( P ( ball ` D ) r ) C_ y -> E. r e. RR+ ( P ( ball ` D ) r ) C_ N ) )
17 13 16 syl5com 
 |-  ( ( D e. ( *Met ` X ) /\ y e. J /\ P e. y ) -> ( y C_ N -> E. r e. RR+ ( P ( ball ` D ) r ) C_ N ) )
18 17 3exp 
 |-  ( D e. ( *Met ` X ) -> ( y e. J -> ( P e. y -> ( y C_ N -> E. r e. RR+ ( P ( ball ` D ) r ) C_ N ) ) ) )
19 18 imp4a 
 |-  ( D e. ( *Met ` X ) -> ( y e. J -> ( ( P e. y /\ y C_ N ) -> E. r e. RR+ ( P ( ball ` D ) r ) C_ N ) ) )
20 19 ad2antrr 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ N C_ X ) -> ( y e. J -> ( ( P e. y /\ y C_ N ) -> E. r e. RR+ ( P ( ball ` D ) r ) C_ N ) ) )
21 20 rexlimdv 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ N C_ X ) -> ( E. y e. J ( P e. y /\ y C_ N ) -> E. r e. RR+ ( P ( ball ` D ) r ) C_ N ) )
22 rpxr 
 |-  ( r e. RR+ -> r e. RR* )
23 1 blopn 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ r e. RR* ) -> ( P ( ball ` D ) r ) e. J )
24 22 23 syl3an3 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ r e. RR+ ) -> ( P ( ball ` D ) r ) e. J )
25 blcntr 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ r e. RR+ ) -> P e. ( P ( ball ` D ) r ) )
26 eleq2 
 |-  ( y = ( P ( ball ` D ) r ) -> ( P e. y <-> P e. ( P ( ball ` D ) r ) ) )
27 sseq1 
 |-  ( y = ( P ( ball ` D ) r ) -> ( y C_ N <-> ( P ( ball ` D ) r ) C_ N ) )
28 26 27 anbi12d 
 |-  ( y = ( P ( ball ` D ) r ) -> ( ( P e. y /\ y C_ N ) <-> ( P e. ( P ( ball ` D ) r ) /\ ( P ( ball ` D ) r ) C_ N ) ) )
29 28 rspcev 
 |-  ( ( ( P ( ball ` D ) r ) e. J /\ ( P e. ( P ( ball ` D ) r ) /\ ( P ( ball ` D ) r ) C_ N ) ) -> E. y e. J ( P e. y /\ y C_ N ) )
30 29 expr 
 |-  ( ( ( P ( ball ` D ) r ) e. J /\ P e. ( P ( ball ` D ) r ) ) -> ( ( P ( ball ` D ) r ) C_ N -> E. y e. J ( P e. y /\ y C_ N ) ) )
31 24 25 30 syl2anc 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X /\ r e. RR+ ) -> ( ( P ( ball ` D ) r ) C_ N -> E. y e. J ( P e. y /\ y C_ N ) ) )
32 31 3expia 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X ) -> ( r e. RR+ -> ( ( P ( ball ` D ) r ) C_ N -> E. y e. J ( P e. y /\ y C_ N ) ) ) )
33 32 rexlimdv 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X ) -> ( E. r e. RR+ ( P ( ball ` D ) r ) C_ N -> E. y e. J ( P e. y /\ y C_ N ) ) )
34 33 adantr 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ N C_ X ) -> ( E. r e. RR+ ( P ( ball ` D ) r ) C_ N -> E. y e. J ( P e. y /\ y C_ N ) ) )
35 21 34 impbid 
 |-  ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ N C_ X ) -> ( E. y e. J ( P e. y /\ y C_ N ) <-> E. r e. RR+ ( P ( ball ` D ) r ) C_ N ) )
36 35 pm5.32da 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X ) -> ( ( N C_ X /\ E. y e. J ( P e. y /\ y C_ N ) ) <-> ( N C_ X /\ E. r e. RR+ ( P ( ball ` D ) r ) C_ N ) ) )
37 9 12 36 3bitr2d 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X ) -> ( N e. ( ( nei ` J ) ` { P } ) <-> ( N C_ X /\ E. r e. RR+ ( P ( ball ` D ) r ) C_ N ) ) )