Description: The distance function of a metric space is a function into the real numbers. (Contributed by NM, 30-Aug-2006) (Revised by Mario Carneiro, 12-Nov-2013)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | msf.x | |- X = ( Base ` M ) |
|
| msf.d | |- D = ( ( dist ` M ) |` ( X X. X ) ) |
||
| Assertion | msf | |- ( M e. MetSp -> D : ( X X. X ) --> RR ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | msf.x | |- X = ( Base ` M ) |
|
| 2 | msf.d | |- D = ( ( dist ` M ) |` ( X X. X ) ) |
|
| 3 | 1 2 | msmet | |- ( M e. MetSp -> D e. ( Met ` X ) ) |
| 4 | metf | |- ( D e. ( Met ` X ) -> D : ( X X. X ) --> RR ) |
|
| 5 | 3 4 | syl | |- ( M e. MetSp -> D : ( X X. X ) --> RR ) |