Metamath Proof Explorer

Theorem mopni2

Description: An open set of a metric space includes a ball around each of its points. (Contributed by NM, 2-May-2007) (Revised by Mario Carneiro, 12-Nov-2013)

Ref Expression
Hypothesis mopni.1 ⊢ J = MetOpen ⁡ D
Assertion mopni2 ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ J ∧ P ∈ A → ∃ x ∈ ℝ + P ball ⁡ D x ⊆ A

Proof

Step Hyp Ref Expression
1 mopni.1 ⊢ J = MetOpen ⁡ D
2 1 mopni ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ J ∧ P ∈ A → ∃ y ∈ ran ⁡ ball ⁡ D P ∈ y ∧ y ⊆ A
3 1 mopnss ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ J → A ⊆ X
4 3 sselda ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ J ∧ P ∈ A → P ∈ X
5 blssex ⊢ D ∈ ∞Met ⁡ X ∧ P ∈ X → ∃ y ∈ ran ⁡ ball ⁡ D P ∈ y ∧ y ⊆ A ↔ ∃ x ∈ ℝ + P ball ⁡ D x ⊆ A
6 5 adantlr ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ J ∧ P ∈ X → ∃ y ∈ ran ⁡ ball ⁡ D P ∈ y ∧ y ⊆ A ↔ ∃ x ∈ ℝ + P ball ⁡ D x ⊆ A
7 4 6 syldan ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ J ∧ P ∈ A → ∃ y ∈ ran ⁡ ball ⁡ D P ∈ y ∧ y ⊆ A ↔ ∃ x ∈ ℝ + P ball ⁡ D x ⊆ A
8 7 3impa ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ J ∧ P ∈ A → ∃ y ∈ ran ⁡ ball ⁡ D P ∈ y ∧ y ⊆ A ↔ ∃ x ∈ ℝ + P ball ⁡ D x ⊆ A
9 2 8 mpbid ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ J ∧ P ∈ A → ∃ x ∈ ℝ + P ball ⁡ D x ⊆ A