Metamath Proof Explorer

Theorem totbndmet

Description: The predicate "totally bounded" implies M is a metric space. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion totbndmet ⊢M∈TotBnd⁡X→M∈Met⁡X

Proof

Step Hyp Ref Expression
1 istotbnd ⊢M∈TotBnd⁡X↔M∈Met⁡X∧∀d∈ℝ+∃v∈Fin⋃v=X∧∀b∈v∃x∈Xb=xball⁡Md
2 1 simplbi ⊢M∈TotBnd⁡X→M∈Met⁡X