Metamath Proof Explorer

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 ⊢ J = MetOpen ⁡ D
Assertion blnei ⊢ D ∈ ∞Met ⁡ X ∧ P ∈ X ∧ R ∈ ℝ + → P ball ⁡ D R ∈ nei ⁡ J ⁡ P

Proof

Step Hyp Ref Expression
1 mopni.1 ⊢ J = MetOpen ⁡ D
2 1 mopntop ⊢ D ∈ ∞Met ⁡ X → J ∈ Top
3 2 3ad2ant1 ⊢ D ∈ ∞Met ⁡ X ∧ P ∈ X ∧ R ∈ ℝ + → J ∈ Top
4 rpxr ⊢ R ∈ ℝ + → R ∈ ℝ *
5 1 blopn ⊢ D ∈ ∞Met ⁡ X ∧ P ∈ X ∧ R ∈ ℝ * → P ball ⁡ D R ∈ J
6 4 5 syl3an3 ⊢ D ∈ ∞Met ⁡ X ∧ P ∈ X ∧ R ∈ ℝ + → P ball ⁡ D R ∈ J
7 blcntr ⊢ D ∈ ∞Met ⁡ X ∧ P ∈ X ∧ R ∈ ℝ + → P ∈ P ball ⁡ D R
8 opnneip ⊢ J ∈ Top ∧ P ball ⁡ D R ∈ J ∧ P ∈ P ball ⁡ D R → P ball ⁡ D R ∈ nei ⁡ J ⁡ P
9 3 6 7 8 syl3anc ⊢ D ∈ ∞Met ⁡ X ∧ P ∈ X ∧ R ∈ ℝ + → P ball ⁡ D R ∈ nei ⁡ J ⁡ P