MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-met Unicode version

Definition df-met 16336
Description: Define the (proper) class of all metrics. (A metric space is the metric's base set paired with the metric; see df-ms 17848. 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 17870, metgt0 17885, metsym 17876, and mettri 17878. (Contributed by NM, 25-Aug-2006.)
Assertion
Ref Expression
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 ) ) ) } )
Distinct variable group:    x, d, y, z, w

Detailed syntax breakdown of Definition df-met
StepHypRef Expression
1 cme 16332 . 2  class  Met
2 vx . . 3  set  x
3 cvv 2763 . . 3  class  _V
4 vy . . . . . . . . . . 11  set  y
54cv 1618 . . . . . . . . . 10  class  y
6 vz . . . . . . . . . . 11  set  z
76cv 1618 . . . . . . . . . 10  class  z
8 vd . . . . . . . . . . 11  set  d
98cv 1618 . . . . . . . . . 10  class  d
105, 7, 9co 5792 . . . . . . . . 9  class  ( y d z )
11 cc0 8705 . . . . . . . . 9  class  0
1210, 11wceq 1619 . . . . . . . 8  wff  ( y d z )  =  0
134, 6weq 1620 . . . . . . . 8  wff  y  =  z
1412, 13wb 178 . . . . . . 7  wff  ( ( y d z )  =  0  <->  y  =  z )
15 vw . . . . . . . . . . . 12  set  w
1615cv 1618 . . . . . . . . . . 11  class  w
1716, 5, 9co 5792 . . . . . . . . . 10  class  ( w d y )
1816, 7, 9co 5792 . . . . . . . . . 10  class  ( w d z )
19 caddc 8708 . . . . . . . . . 10  class  +
2017, 18, 19co 5792 . . . . . . . . 9  class  ( ( w d y )  +  ( w d z ) )
21 cle 8836 . . . . . . . . 9  class  <_
2210, 20, 21wbr 3997 . . . . . . . 8  wff  ( y d z )  <_ 
( ( w d y )  +  ( w d z ) )
232cv 1618 . . . . . . . 8  class  x
2422, 15, 23wral 2518 . . . . . . 7  wff  A. w  e.  x  ( y
d z )  <_ 
( ( w d y )  +  ( w d z ) )
2514, 24wa 360 . . . . . 6  wff  ( ( ( y d z )  =  0  <->  y  =  z )  /\  A. w  e.  x  ( y d z )  <_  ( ( w d y )  +  ( w d z ) ) )
2625, 6, 23wral 2518 . . . . 5  wff  A. z  e.  x  ( (
( y d z )  =  0  <->  y  =  z )  /\  A. w  e.  x  ( y d z )  <_  ( ( w d y )  +  ( w d z ) ) )
2726, 4, 23wral 2518 . . . 4  wff  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 ) ) )
28 cr 8704 . . . . 5  class  RR
2923, 23cxp 4659 . . . . 5  class  ( x  X.  x )
30 cmap 6740 . . . . 5  class  ^m
3128, 29, 30co 5792 . . . 4  class  ( RR 
^m  ( x  X.  x ) )
3227, 8, 31crab 2522 . . 3  class  { 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 ) ) ) }
332, 3, 32cmpt 4051 . 2  class  ( 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 ) ) ) } )
341, 33wceq 1619 1  wff  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 ) ) ) } )
Colors of variables: wff set class
This definition is referenced by:  ismet  17850
  Copyright terms: Public domain W3C validator