Metamath Proof Explorer

Theorem elmopn

Description: The defining property of an open set of a metric space. (Contributed by NM, 1-Sep-2006) (Revised by Mario Carneiro, 12-Nov-2013)

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

Proof

Step Hyp Ref Expression
1 mopnval.1 ⊢ J = MetOpen ⁡ D
2 1 mopnval ⊢ D ∈ ∞Met ⁡ X → J = topGen ⁡ ran ⁡ ball ⁡ D
3 2 eleq2d ⊢ D ∈ ∞Met ⁡ X → A ∈ J ↔ A ∈ topGen ⁡ ran ⁡ ball ⁡ D
4 blbas ⊢ D ∈ ∞Met ⁡ X → ran ⁡ ball ⁡ D ∈ TopBases
5 eltg2 ⊢ ran ⁡ ball ⁡ D ∈ TopBases → A ∈ topGen ⁡ ran ⁡ ball ⁡ D ↔ A ⊆ ⋃ ran ⁡ ball ⁡ D ∧ ∀ x ∈ A ∃ y ∈ ran ⁡ ball ⁡ D x ∈ y ∧ y ⊆ A
6 4 5 syl ⊢ D ∈ ∞Met ⁡ X → A ∈ topGen ⁡ ran ⁡ ball ⁡ D ↔ A ⊆ ⋃ ran ⁡ ball ⁡ D ∧ ∀ x ∈ A ∃ y ∈ ran ⁡ ball ⁡ D x ∈ y ∧ y ⊆ A
7 unirnbl ⊢ D ∈ ∞Met ⁡ X → ⋃ ran ⁡ ball ⁡ D = X
8 7 sseq2d ⊢ D ∈ ∞Met ⁡ X → A ⊆ ⋃ ran ⁡ ball ⁡ D ↔ A ⊆ X
9 8 anbi1d ⊢ D ∈ ∞Met ⁡ X → A ⊆ ⋃ ran ⁡ ball ⁡ D ∧ ∀ x ∈ A ∃ y ∈ ran ⁡ ball ⁡ D x ∈ y ∧ y ⊆ A ↔ A ⊆ X ∧ ∀ x ∈ A ∃ y ∈ ran ⁡ ball ⁡ D x ∈ y ∧ y ⊆ A
10 3 6 9 3bitrd ⊢ D ∈ ∞Met ⁡ X → A ∈ J ↔ A ⊆ X ∧ ∀ x ∈ A ∃ y ∈ ran ⁡ ball ⁡ D x ∈ y ∧ y ⊆ A