This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )