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 ∈ X b = x ball ⁡ M d

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