Metamath Proof Explorer

Theorem metf

Description: Mapping of the distance function of a metric space. (Contributed by NM, 30-Aug-2006)

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

Proof

Step	Hyp	Ref	Expression
1		metflem	\|- ( 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 ) + ( z D y ) ) ) ) )
2	1	simpld	\|- ( D e. ( Met ` X ) -> D : ( X X. X ) --> RR )

Step

Hyp

Ref

Expression

metflem

 |-  ( 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 ) + ( z D y ) ) ) ) )

simpld

 |-  ( D e. ( Met ` X ) -> D : ( X X. X ) --> RR )