Metamath Proof Explorer

Theorem elmopn2

Description: A defining property of an open set of a metric space. (Contributed by NM, 5-May-2007) (Revised by Mario Carneiro, 12-Nov-2013)

Ref Expression
Hypothesis mopnval.1 ⊢ J = MetOpen ⁡ D
Assertion elmopn2 ⊢ D ∈ ∞Met ⁡ X → A ∈ J ↔ A ⊆ X ∧ ∀ x ∈ A ∃ y ∈ ℝ + x ball ⁡ D y ⊆ A

Proof

Step Hyp Ref Expression
1 mopnval.1 ⊢ J = MetOpen ⁡ D
2 1 elmopn ⊢ D ∈ ∞Met ⁡ X → A ∈ J ↔ A ⊆ X ∧ ∀ x ∈ A ∃ z ∈ ran ⁡ ball ⁡ D x ∈ z ∧ z ⊆ A
3 ssel2 ⊢ A ⊆ X ∧ x ∈ A → x ∈ X
4 blssex ⊢ D ∈ ∞Met ⁡ X ∧ x ∈ X → ∃ z ∈ ran ⁡ ball ⁡ D x ∈ z ∧ z ⊆ A ↔ ∃ y ∈ ℝ + x ball ⁡ D y ⊆ A
5 3 4 sylan2 ⊢ D ∈ ∞Met ⁡ X ∧ A ⊆ X ∧ x ∈ A → ∃ z ∈ ran ⁡ ball ⁡ D x ∈ z ∧ z ⊆ A ↔ ∃ y ∈ ℝ + x ball ⁡ D y ⊆ A
6 5 anassrs ⊢ D ∈ ∞Met ⁡ X ∧ A ⊆ X ∧ x ∈ A → ∃ z ∈ ran ⁡ ball ⁡ D x ∈ z ∧ z ⊆ A ↔ ∃ y ∈ ℝ + x ball ⁡ D y ⊆ A
7 6 ralbidva ⊢ D ∈ ∞Met ⁡ X ∧ A ⊆ X → ∀ x ∈ A ∃ z ∈ ran ⁡ ball ⁡ D x ∈ z ∧ z ⊆ A ↔ ∀ x ∈ A ∃ y ∈ ℝ + x ball ⁡ D y ⊆ A
8 7 pm5.32da ⊢ D ∈ ∞Met ⁡ X → A ⊆ X ∧ ∀ x ∈ A ∃ z ∈ ran ⁡ ball ⁡ D x ∈ z ∧ z ⊆ A ↔ A ⊆ X ∧ ∀ x ∈ A ∃ y ∈ ℝ + x ball ⁡ D y ⊆ A
9 2 8 bitrd ⊢ D ∈ ∞Met ⁡ X → A ∈ J ↔ A ⊆ X ∧ ∀ x ∈ A ∃ y ∈ ℝ + x ball ⁡ D y ⊆ A