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 ) |
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 ) |