Metamath Proof Explorer

Theorem bndmet

Description: A bounded metric space is a metric space. (Contributed by Mario Carneiro, 16-Sep-2015)

Ref Expression
Assertion bndmet 
|- ( M e. ( Bnd ` X ) -> M e. ( Met ` X ) )

Proof

Step Hyp Ref Expression
1 isbnd 
 |-  ( M e. ( Bnd ` X ) <-> ( M e. ( Met ` X ) /\ A. x e. X E. y e. RR+ X = ( x ( ball ` M ) y ) ) )
2 1 simplbi 
 |-  ( M e. ( Bnd ` X ) -> M e. ( Met ` X ) )