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 ∈ X b = x ball ⁡ M d
2 1 simplbi ⊢ M ∈ TotBnd ⁡ X → M ∈ Met ⁡ X