Metamath Proof Explorer

Definition df-met

Description: Define the (proper) class of all metrics. (A metric space is the metric's base set paired with the metric; see df-ms . However, we will often also call the metric itself a "metric space".) Equivalent to Definition 14-1.1 of Gleason p. 223. The 4 properties in Gleason's definition are shown by met0 , metgt0 , metsym , and mettri . (Contributed by NM, 25-Aug-2006)

Ref Expression
Assertion df-met 
|- Met = ( x e. _V |-> { d e. ( RR ^m ( x X. x ) ) | A. y e. x A. z e. x ( ( ( y d z ) = 0 <-> y = z ) /\ A. w e. x ( y d z ) <_ ( ( w d y ) + ( w d z ) ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmet 
 |-  Met
1 vx 
 |-  x
2 cvv 
 |-  _V
3 vd 
 |-  d
4 cr 
 |-  RR
5 cmap 
 |-  ^m
6 1 cv 
 |-  x
7 6 6 cxp 
 |-  ( x X. x )
8 4 7 5 co 
 |-  ( RR ^m ( x X. x ) )
9 vy 
 |-  y
10 vz 
 |-  z
11 9 cv 
 |-  y
12 3 cv 
 |-  d
13 10 cv 
 |-  z
14 11 13 12 co 
 |-  ( y d z )
15 cc0 
 |-  0
16 14 15 wceq 
 |-  ( y d z ) = 0
17 11 13 wceq 
 |-  y = z
18 16 17 wb 
 |-  ( ( y d z ) = 0 <-> y = z )
19 vw 
 |-  w
20 cle 
 |-  <_
21 19 cv 
 |-  w
22 21 11 12 co 
 |-  ( w d y )
23 caddc 
 |-  +
24 21 13 12 co 
 |-  ( w d z )
25 22 24 23 co 
 |-  ( ( w d y ) + ( w d z ) )
26 14 25 20 wbr 
 |-  ( y d z ) <_ ( ( w d y ) + ( w d z ) )
27 26 19 6 wral 
 |-  A. w e. x ( y d z ) <_ ( ( w d y ) + ( w d z ) )
28 18 27 wa 
 |-  ( ( ( y d z ) = 0 <-> y = z ) /\ A. w e. x ( y d z ) <_ ( ( w d y ) + ( w d z ) ) )
29 28 10 6 wral 
 |-  A. z e. x ( ( ( y d z ) = 0 <-> y = z ) /\ A. w e. x ( y d z ) <_ ( ( w d y ) + ( w d z ) ) )
30 29 9 6 wral 
 |-  A. y e. x A. z e. x ( ( ( y d z ) = 0 <-> y = z ) /\ A. w e. x ( y d z ) <_ ( ( w d y ) + ( w d z ) ) )
31 30 3 8 crab 
 |-  { d e. ( RR ^m ( x X. x ) ) | A. y e. x A. z e. x ( ( ( y d z ) = 0 <-> y = z ) /\ A. w e. x ( y d z ) <_ ( ( w d y ) + ( w d z ) ) ) }
32 1 2 31 cmpt 
 |-  ( x e. _V |-> { d e. ( RR ^m ( x X. x ) ) | A. y e. x A. z e. x ( ( ( y d z ) = 0 <-> y = z ) /\ A. w e. x ( y d z ) <_ ( ( w d y ) + ( w d z ) ) ) } )
33 0 32 wceq 
 |-  Met = ( x e. _V |-> { d e. ( RR ^m ( x X. x ) ) | A. y e. x A. z e. x ( ( ( y d z ) = 0 <-> y = z ) /\ A. w e. x ( y d z ) <_ ( ( w d y ) + ( w d z ) ) ) } )