This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem blssopn

Description: The balls of a metric space are open sets. (Contributed by NM, 12-Sep-2006) (Revised by Mario Carneiro, 23-Dec-2013)

Ref Expression
Hypothesis mopni.1 ⊢ J = MetOpen ⁡ D
Assertion blssopn ⊢ D ∈ ∞Met ⁡ X → ran ⁡ ball ⁡ D ⊆ J

Proof

Step Hyp Ref Expression
1 mopni.1 ⊢ J = MetOpen ⁡ D
2 blbas ⊢ D ∈ ∞Met ⁡ X → ran ⁡ ball ⁡ D ∈ TopBases
3 bastg ⊢ ran ⁡ ball ⁡ D ∈ TopBases → ran ⁡ ball ⁡ D ⊆ topGen ⁡ ran ⁡ ball ⁡ D
4 2 3 syl ⊢ D ∈ ∞Met ⁡ X → ran ⁡ ball ⁡ D ⊆ topGen ⁡ ran ⁡ ball ⁡ D
5 1 mopnval ⊢ D ∈ ∞Met ⁡ X → J = topGen ⁡ ran ⁡ ball ⁡ D
6 4 5 sseqtrrd ⊢ D ∈ ∞Met ⁡ X → ran ⁡ ball ⁡ D ⊆ J