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 e. ( TotBnd ` X ) -> M e. ( Met ` X ) )

Proof

Step Hyp Ref Expression
1 istotbnd 
 |-  ( M e. ( TotBnd ` X ) <-> ( M e. ( Met ` X ) /\ A. d e. RR+ E. v e. Fin ( U. v = X /\ A. b e. v E. x e. X b = ( x ( ball ` M ) d ) ) ) )
2 1 simplbi 
 |-  ( M e. ( TotBnd ` X ) -> M e. ( Met ` X ) )