Theorem ismeti

Description: Properties that determine a metric. (Contributed by NM, 17-Nov-2006) (Revised by Mario Carneiro, 14-Aug-2015)

	Ref	Expression
Hypotheses	ismeti.0	|- X e. _V
	ismeti.1	|- D : ( X X. X ) --> RR
	ismeti.2	|- ( ( x e. X /\ y e. X ) -> ( ( x D y ) = 0 <-> x = y ) )
	ismeti.3	|- ( ( x e. X /\ y e. X /\ z e. X ) -> ( x D y ) <_ ( ( z D x ) + ( z D y ) ) )
Assertion	ismeti	|- D e. ( Met ` X )

Proof

Step	Hyp	Ref	Expression
1		ismeti.0	|- X e. _V
2		ismeti.1	|- D : ( X X. X ) --> RR
3		ismeti.2	|- ( ( x e. X /\ y e. X ) -> ( ( x D y ) = 0 <-> x = y ) )
4		ismeti.3	|- ( ( x e. X /\ y e. X /\ z e. X ) -> ( x D y ) <_ ( ( z D x ) + ( z D y ) ) )
5	4	3expa	|- ( ( ( x e. X /\ y e. X ) /\ z e. X ) -> ( x D y ) <_ ( ( z D x ) + ( z D y ) ) )
6	5	ralrimiva	|- ( ( x e. X /\ y e. X ) -> A. z e. X ( x D y ) <_ ( ( z D x ) + ( z D y ) ) )
7	3 6	jca	|- ( ( x e. X /\ y e. X ) -> ( ( ( x D y ) = 0 <-> x = y ) /\ A. z e. X ( x D y ) <_ ( ( z D x ) + ( z D y ) ) ) )
8	7	rgen2	|- 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 ) ) )
9		ismet	|- ( X e. _V -> ( 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 ) ) ) ) ) )
10	1 9	ax-mp	|- ( 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 ) ) ) ) )
11	2 8 10	mpbir2an	|- D e. ( Met ` X )