Metamath Proof Explorer

Theorem istotbnd2

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

Ref Expression
Assertion istotbnd2 ⊢M∈Met⁡X→M∈TotBnd⁡X↔∀d∈ℝ+∃v∈Fin⋃v=X∧∀b∈v∃x∈Xb=xball⁡Md

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 baib ⊢M∈Met⁡X→M∈TotBnd⁡X↔∀d∈ℝ+∃v∈Fin⋃v=X∧∀b∈v∃x∈Xb=xball⁡Md