Metamath Proof Explorer

Theorem mopni

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

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

Proof

Step Hyp Ref Expression
1 mopni.1 ⊢ J = MetOpen ⁡ D
2 1 elmopn ⊢ D ∈ ∞Met ⁡ X → A ∈ J ↔ A ⊆ X ∧ ∀ y ∈ A ∃ x ∈ ran ⁡ ball ⁡ D y ∈ x ∧ x ⊆ A
3 2 simplbda ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ J → ∀ y ∈ A ∃ x ∈ ran ⁡ ball ⁡ D y ∈ x ∧ x ⊆ A
4 eleq1 ⊢ y = P → y ∈ x ↔ P ∈ x
5 4 anbi1d ⊢ y = P → y ∈ x ∧ x ⊆ A ↔ P ∈ x ∧ x ⊆ A
6 5 rexbidv ⊢ y = P → ∃ x ∈ ran ⁡ ball ⁡ D y ∈ x ∧ x ⊆ A ↔ ∃ x ∈ ran ⁡ ball ⁡ D P ∈ x ∧ x ⊆ A
7 6 rspccv ⊢ ∀ y ∈ A ∃ x ∈ ran ⁡ ball ⁡ D y ∈ x ∧ x ⊆ A → P ∈ A → ∃ x ∈ ran ⁡ ball ⁡ D P ∈ x ∧ x ⊆ A
8 3 7 syl ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ J → P ∈ A → ∃ x ∈ ran ⁡ ball ⁡ D P ∈ x ∧ x ⊆ A
9 8 3impia ⊢ D ∈ ∞Met ⁡ X ∧ A ∈ J ∧ P ∈ A → ∃ x ∈ ran ⁡ ball ⁡ D P ∈ x ∧ x ⊆ A