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 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
Assertion neibl ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ↔ ( 𝑁 ⊆ 𝑋 ∧ ∃ 𝑟 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 mopni.1 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2 1 mopntop ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ Top )
3 2 adantr ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → 𝐽 ∈ Top )
4 1 mopnuni ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
5 4 eleq2d ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑃 ∈ 𝑋 ↔ 𝑃 ∈ ∪ 𝐽 ) )
6 5 biimpa ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → 𝑃 ∈ ∪ 𝐽 )
7 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
8 7 isneip ⊢ ( ( 𝐽 ∈ Top ∧ 𝑃 ∈ ∪ 𝐽 ) → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ↔ ( 𝑁 ⊆ ∪ 𝐽 ∧ ∃ 𝑦 ∈ 𝐽 ( 𝑃 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑁 ) ) ) )
9 3 6 8 syl2anc ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ↔ ( 𝑁 ⊆ ∪ 𝐽 ∧ ∃ 𝑦 ∈ 𝐽 ( 𝑃 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑁 ) ) ) )
10 4 sseq2d ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑁 ⊆ 𝑋 ↔ 𝑁 ⊆ ∪ 𝐽 ) )
11 10 adantr ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝑁 ⊆ 𝑋 ↔ 𝑁 ⊆ ∪ 𝐽 ) )
12 11 anbi1d ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → ( ( 𝑁 ⊆ 𝑋 ∧ ∃ 𝑦 ∈ 𝐽 ( 𝑃 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑁 ) ) ↔ ( 𝑁 ⊆ ∪ 𝐽 ∧ ∃ 𝑦 ∈ 𝐽 ( 𝑃 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑁 ) ) ) )
13 1 mopni2 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐽 ∧ 𝑃 ∈ 𝑦 ) → ∃ 𝑟 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑦 )
14 sstr2 ⊢ ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑦 → ( 𝑦 ⊆ 𝑁 → ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑁 ) )
15 14 com12 ⊢ ( 𝑦 ⊆ 𝑁 → ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑦 → ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑁 ) )
16 15 reximdv ⊢ ( 𝑦 ⊆ 𝑁 → ( ∃ 𝑟 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑦 → ∃ 𝑟 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑁 ) )
17 13 16 syl5com ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐽 ∧ 𝑃 ∈ 𝑦 ) → ( 𝑦 ⊆ 𝑁 → ∃ 𝑟 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑁 ) )
18 17 3exp ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑦 ∈ 𝐽 → ( 𝑃 ∈ 𝑦 → ( 𝑦 ⊆ 𝑁 → ∃ 𝑟 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑁 ) ) ) )
19 18 imp4a ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑦 ∈ 𝐽 → ( ( 𝑃 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑁 ) → ∃ 𝑟 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑁 ) ) )
20 19 ad2antrr ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑁 ⊆ 𝑋 ) → ( 𝑦 ∈ 𝐽 → ( ( 𝑃 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑁 ) → ∃ 𝑟 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑁 ) ) )
21 20 rexlimdv ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑁 ⊆ 𝑋 ) → ( ∃ 𝑦 ∈ 𝐽 ( 𝑃 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑁 ) → ∃ 𝑟 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑁 ) )
22 rpxr ⊢ ( 𝑟 ∈ ℝ+ → 𝑟 ∈ ℝ* )
23 1 blopn ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑟 ∈ ℝ* ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ∈ 𝐽 )
24 22 23 syl3an3 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ∈ 𝐽 )
25 blcntr ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) → 𝑃 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) )
26 eleq2 ⊢ ( 𝑦 = ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) → ( 𝑃 ∈ 𝑦 ↔ 𝑃 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ) )
27 sseq1 ⊢ ( 𝑦 = ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) → ( 𝑦 ⊆ 𝑁 ↔ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑁 ) )
28 26 27 anbi12d ⊢ ( 𝑦 = ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) → ( ( 𝑃 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑁 ) ↔ ( 𝑃 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ∧ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑁 ) ) )
29 28 rspcev ⊢ ( ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ∈ 𝐽 ∧ ( 𝑃 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ∧ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑁 ) ) → ∃ 𝑦 ∈ 𝐽 ( 𝑃 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑁 ) )
30 29 expr ⊢ ( ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ∈ 𝐽 ∧ 𝑃 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ) → ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑁 → ∃ 𝑦 ∈ 𝐽 ( 𝑃 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑁 ) ) )
31 24 25 30 syl2anc ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) → ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑁 → ∃ 𝑦 ∈ 𝐽 ( 𝑃 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑁 ) ) )
32 31 3expia ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝑟 ∈ ℝ+ → ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑁 → ∃ 𝑦 ∈ 𝐽 ( 𝑃 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑁 ) ) ) )
33 32 rexlimdv ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → ( ∃ 𝑟 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑁 → ∃ 𝑦 ∈ 𝐽 ( 𝑃 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑁 ) ) )
34 33 adantr ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑁 ⊆ 𝑋 ) → ( ∃ 𝑟 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑁 → ∃ 𝑦 ∈ 𝐽 ( 𝑃 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑁 ) ) )
35 21 34 impbid ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑁 ⊆ 𝑋 ) → ( ∃ 𝑦 ∈ 𝐽 ( 𝑃 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑁 ) ↔ ∃ 𝑟 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑁 ) )
36 35 pm5.32da ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → ( ( 𝑁 ⊆ 𝑋 ∧ ∃ 𝑦 ∈ 𝐽 ( 𝑃 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑁 ) ) ↔ ( 𝑁 ⊆ 𝑋 ∧ ∃ 𝑟 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑁 ) ) )
37 9 12 36 3bitr2d ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) ↔ ( 𝑁 ⊆ 𝑋 ∧ ∃ 𝑟 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑁 ) ) )