Theorem blnei

Description: A ball around a point is a neighborhood of the point. (Contributed by NM, 8-Nov-2007) (Revised by Mario Carneiro, 24-Aug-2015)

	Ref	Expression
Hypothesis	mopni.1	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
Assertion	blnei	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+ ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) )

Proof

Step	Hyp	Ref	Expression
1		mopni.1	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2	1	mopntop	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ Top )
3	2	3ad2ant1	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+ ) → 𝐽 ∈ Top )
4		rpxr	⊢ ( 𝑅 ∈ ℝ+ → 𝑅 ∈ ℝ* )
5	1	blopn	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∈ 𝐽 )
6	4 5	syl3an3	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+ ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∈ 𝐽 )
7		blcntr	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+ ) → 𝑃 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) )
8		opnneip	⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∈ 𝐽 ∧ 𝑃 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) )
9	3 6 7 8	syl3anc	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+ ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑃 } ) )