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

Definition df-psmet 16682
Description: Define the set of all pseudometrics on a given base set. In a pseudo metric, two distinct points may have a distance zero. (Contributed by Thierry Arnoux, 7-Feb-2018.)
Assertion
Ref Expression
df-psmet  |- PsMet  =  ( x  e.  _V  |->  { d  e.  ( RR*  ^m  ( x  X.  x
) )  |  A. y  e.  x  (
( y d y )  =  0  /\ 
A. z  e.  x  A. w  e.  x  ( y d z )  <_  ( (
w d y ) + e ( w d z ) ) ) } )
Distinct variable group:    x, d, y, z, w

Detailed syntax breakdown of Definition df-psmet
StepHypRef Expression
1 cpsmet 16673 . 2  class PsMet
2 vx . . 3  set  x
3 cvv 2948 . . 3  class  _V
4 vy . . . . . . . . 9  set  y
54cv 1651 . . . . . . . 8  class  y
6 vd . . . . . . . . 9  set  d
76cv 1651 . . . . . . . 8  class  d
85, 5, 7co 6072 . . . . . . 7  class  ( y d y )
9 cc0 8979 . . . . . . 7  class  0
108, 9wceq 1652 . . . . . 6  wff  ( y d y )  =  0
11 vz . . . . . . . . . . 11  set  z
1211cv 1651 . . . . . . . . . 10  class  z
135, 12, 7co 6072 . . . . . . . . 9  class  ( y d z )
14 vw . . . . . . . . . . . 12  set  w
1514cv 1651 . . . . . . . . . . 11  class  w
1615, 5, 7co 6072 . . . . . . . . . 10  class  ( w d y )
1715, 12, 7co 6072 . . . . . . . . . 10  class  ( w d z )
18 cxad 10697 . . . . . . . . . 10  class  + e
1916, 17, 18co 6072 . . . . . . . . 9  class  ( ( w d y ) + e ( w d z ) )
20 cle 9110 . . . . . . . . 9  class  <_
2113, 19, 20wbr 4204 . . . . . . . 8  wff  ( y d z )  <_ 
( ( w d y ) + e
( w d z ) )
222cv 1651 . . . . . . . 8  class  x
2321, 14, 22wral 2697 . . . . . . 7  wff  A. w  e.  x  ( y
d z )  <_ 
( ( w d y ) + e
( w d z ) )
2423, 11, 22wral 2697 . . . . . 6  wff  A. z  e.  x  A. w  e.  x  ( y
d z )  <_ 
( ( w d y ) + e
( w d z ) )
2510, 24wa 359 . . . . 5  wff  ( ( y d y )  =  0  /\  A. z  e.  x  A. w  e.  x  (
y d z )  <_  ( ( w d y ) + e ( w d z ) ) )
2625, 4, 22wral 2697 . . . 4  wff  A. y  e.  x  ( (
y d y )  =  0  /\  A. z  e.  x  A. w  e.  x  (
y d z )  <_  ( ( w d y ) + e ( w d z ) ) )
27 cxr 9108 . . . . 5  class  RR*
2822, 22cxp 4867 . . . . 5  class  ( x  X.  x )
29 cmap 7009 . . . . 5  class  ^m
3027, 28, 29co 6072 . . . 4  class  ( RR*  ^m  ( x  X.  x
) )
3126, 6, 30crab 2701 . . 3  class  { d  e.  ( RR*  ^m  (
x  X.  x ) )  |  A. y  e.  x  ( (
y d y )  =  0  /\  A. z  e.  x  A. w  e.  x  (
y d z )  <_  ( ( w d y ) + e ( w d z ) ) ) }
322, 3, 31cmpt 4258 . 2  class  ( x  e.  _V  |->  { d  e.  ( RR*  ^m  (
x  X.  x ) )  |  A. y  e.  x  ( (
y d y )  =  0  /\  A. z  e.  x  A. w  e.  x  (
y d z )  <_  ( ( w d y ) + e ( w d z ) ) ) } )
331, 32wceq 1652 1  wff PsMet  =  ( x  e.  _V  |->  { d  e.  ( RR*  ^m  ( x  X.  x
) )  |  A. y  e.  x  (
( y d y )  =  0  /\ 
A. z  e.  x  A. w  e.  x  ( y d z )  <_  ( (
w d y ) + e ( w d z ) ) ) } )
Colors of variables: wff set class
This definition is referenced by:  ispsmet  18323  metuval  18568  metidval  24273  pstmval  24278
  Copyright terms: Public domain W3C validator