Metamath Proof Explorer

Theorem xmetf

Description: Mapping of the distance function of an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xmetf 
|- ( D e. ( *Met ` X ) -> D : ( X X. X ) --> RR* )

Proof

Step Hyp Ref Expression
1 elfvdm 
 |-  ( D e. ( *Met ` X ) -> X e. dom *Met )
2 isxmet 
 |-  ( X e. dom *Met -> ( D e. ( *Met ` X ) <-> ( D : ( X X. X ) --> RR* /\ A. x e. X A. y e. X ( ( ( x D y ) = 0 <-> x = y ) /\ A. z e. X ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) ) ) ) )
3 1 2 syl 
 |-  ( D e. ( *Met ` X ) -> ( D e. ( *Met ` X ) <-> ( D : ( X X. X ) --> RR* /\ A. x e. X A. y e. X ( ( ( x D y ) = 0 <-> x = y ) /\ A. z e. X ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) ) ) ) )
4 3 ibi 
 |-  ( D e. ( *Met ` X ) -> ( D : ( X X. X ) --> RR* /\ A. x e. X A. y e. X ( ( ( x D y ) = 0 <-> x = y ) /\ A. z e. X ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) ) ) )
5 4 simpld 
 |-  ( D e. ( *Met ` X ) -> D : ( X X. X ) --> RR* )