Metamath Proof Explorer

Theorem msxms

Description: A metric space is an extended metric space. (Contributed by Mario Carneiro, 26-Aug-2015)

Ref Expression
Assertion msxms 
|- ( M e. MetSp -> M e. *MetSp )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( TopOpen ` M ) = ( TopOpen ` M )
2 eqid 
 |-  ( Base ` M ) = ( Base ` M )
3 eqid 
 |-  ( ( dist ` M ) |` ( ( Base ` M ) X. ( Base ` M ) ) ) = ( ( dist ` M ) |` ( ( Base ` M ) X. ( Base ` M ) ) )
4 1 2 3 isms 
 |-  ( M e. MetSp <-> ( M e. *MetSp /\ ( ( dist ` M ) |` ( ( Base ` M ) X. ( Base ` M ) ) ) e. ( Met ` ( Base ` M ) ) ) )
5 4 simplbi 
 |-  ( M e. MetSp -> M e. *MetSp )