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

Definition df-psmet 16649
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 16640 . 2  class PsMet
2 vx . . 3  set  x
3 cvv 2916 . . 3  class  _V
4 vy . . . . . . . . 9  set  y
54cv 1648 . . . . . . . 8  class  y
6 vd . . . . . . . . 9  set  d
76cv 1648 . . . . . . . 8  class  d
85, 5, 7co 6040 . . . . . . 7  class  ( y d y )
9 cc0 8946 . . . . . . 7  class  0
108, 9wceq 1649 . . . . . 6  wff  ( y d y )  =  0
11 vz . . . . . . . . . . 11  set  z
1211cv 1648 . . . . . . . . . 10  class  z
135, 12, 7co 6040 . . . . . . . . 9  class  ( y d z )
14 vw . . . . . . . . . . . 12  set  w
1514cv 1648 . . . . . . . . . . 11  class  w
1615, 5, 7co 6040 . . . . . . . . . 10  class  ( w d y )
1715, 12, 7co 6040 . . . . . . . . . 10  class  ( w d z )
18 cxad 10664 . . . . . . . . . 10  class  + e
1916, 17, 18co 6040 . . . . . . . . 9  class  ( ( w d y ) + e ( w d z ) )
20 cle 9077 . . . . . . . . 9  class  <_
2113, 19, 20wbr 4172 . . . . . . . 8  wff  ( y d z )  <_ 
( ( w d y ) + e
( w d z ) )
222cv 1648 . . . . . . . 8  class  x
2321, 14, 22wral 2666 . . . . . . 7  wff  A. w  e.  x  ( y
d z )  <_ 
( ( w d y ) + e
( w d z ) )
2423, 11, 22wral 2666 . . . . . 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 2666 . . . 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 9075 . . . . 5  class  RR*
2822, 22cxp 4835 . . . . 5  class  ( x  X.  x )
29 cmap 6977 . . . . 5  class  ^m
3027, 28, 29co 6040 . . . 4  class  ( RR*  ^m  ( x  X.  x
) )
3126, 6, 30crab 2670 . . 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 4226 . 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 1649 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  18288  metuval  18533  metidval  24238  pstmval  24243
  Copyright terms: Public domain W3C validator