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

Metamath Proof Explorer

Theorem bndmet

Description: A bounded metric space is a metric space. (Contributed by Mario Carneiro, 16-Sep-2015)

Ref Expression
Assertion bndmet ⊢ M ∈ Bnd ⁡ X → M ∈ Met ⁡ X

Proof

Step Hyp Ref Expression
1 isbnd ⊢ M ∈ Bnd ⁡ X ↔ M ∈ Met ⁡ X ∧ ∀ x ∈ X ∃ y ∈ ℝ + X = x ball ⁡ M y
2 1 simplbi ⊢ M ∈ Bnd ⁡ X → M ∈ Met ⁡ X