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 )