Metamath Proof Explorer

Theorem cmsms

Description: A complete metric space is a metric space. (Contributed by Mario Carneiro, 15-Oct-2015)

Ref Expression
Assertion cmsms 
|- ( G e. CMetSp -> G e. MetSp )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Base ` G ) = ( Base ` G )
2 eqid 
 |-  ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) = ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) )
3 1 2 iscms 
 |-  ( G e. CMetSp <-> ( G e. MetSp /\ ( ( dist ` G ) |` ( ( Base ` G ) X. ( Base ` G ) ) ) e. ( CMet ` ( Base ` G ) ) ) )
4 3 simplbi 
 |-  ( G e. CMetSp -> G e. MetSp )