Metamath Proof Explorer

Theorem xmstps

Description: An extended metric space is a topological space. (Contributed by Mario Carneiro, 26-Aug-2015)

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

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 isxms 
 |-  ( M e. *MetSp <-> ( M e. TopSp /\ ( TopOpen ` M ) = ( MetOpen ` ( ( dist ` M ) |` ( ( Base ` M ) X. ( Base ` M ) ) ) ) ) )
5 4 simplbi 
 |-  ( M e. *MetSp -> M e. TopSp )