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 ‘ 𝐷 ) 𝑟 ) ⊆ 𝑁 ) ) )