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

Definition df-xmet 16373
Description: Define the set of all extended metrics on a given base set. The definition is similar to df-met 16374, but we also allow the metric to take on the value  +oo. (Contributed by Mario Carneiro, 20-Aug-2015.)
Assertion
Ref Expression
df-xmet  |-  * 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 ) + e ( w d z ) ) ) } )
Distinct variable group:    x, d, y, z, w

Detailed syntax breakdown of Definition df-xmet
StepHypRef Expression
1 cxmt 16369 . 2  class  * Met
2 vx . . 3  set  x
3 cvv 2788 . . 3  class  _V
4 vy . . . . . . . . . . 11  set  y
54cv 1622 . . . . . . . . . 10  class  y
6 vz . . . . . . . . . . 11  set  z
76cv 1622 . . . . . . . . . 10  class  z
8 vd . . . . . . . . . . 11  set  d
98cv 1622 . . . . . . . . . 10  class  d
105, 7, 9co 5858 . . . . . . . . 9  class  ( y d z )
11 cc0 8737 . . . . . . . . 9  class  0
1210, 11wceq 1623 . . . . . . . 8  wff  ( y d z )  =  0
134, 6weq 1624 . . . . . . . 8  wff  y  =  z
1412, 13wb 176 . . . . . . 7  wff  ( ( y d z )  =  0  <->  y  =  z )
15 vw . . . . . . . . . . . 12  set  w
1615cv 1622 . . . . . . . . . . 11  class  w
1716, 5, 9co 5858 . . . . . . . . . 10  class  ( w d y )
1816, 7, 9co 5858 . . . . . . . . . 10  class  ( w d z )
19 cxad 10450 . . . . . . . . . 10  class  + e
2017, 18, 19co 5858 . . . . . . . . 9  class  ( ( w d y ) + e ( w d z ) )
21 cle 8868 . . . . . . . . 9  class  <_
2210, 20, 21wbr 4023 . . . . . . . 8  wff  ( y d z )  <_ 
( ( w d y ) + e
( w d z ) )
232cv 1622 . . . . . . . 8  class  x
2422, 15, 23wral 2543 . . . . . . 7  wff  A. w  e.  x  ( y
d z )  <_ 
( ( w d y ) + e
( w d z ) )
2514, 24wa 358 . . . . . 6  wff  ( ( ( y d z )  =  0  <->  y  =  z )  /\  A. w  e.  x  ( y d z )  <_  ( ( w d y ) + e ( w d z ) ) )
2625, 6, 23wral 2543 . . . . 5  wff  A. z  e.  x  ( (
( y d z )  =  0  <->  y  =  z )  /\  A. w  e.  x  ( y d z )  <_  ( ( w d y ) + e ( w d z ) ) )
2726, 4, 23wral 2543 . . . 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 ) + e ( w d z ) ) )
28 cxr 8866 . . . . 5  class  RR*
2923, 23cxp 4687 . . . . 5  class  ( x  X.  x )
30 cmap 6772 . . . . 5  class  ^m
3128, 29, 30co 5858 . . . 4  class  ( RR*  ^m  ( x  X.  x
) )
3227, 8, 31crab 2547 . . 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 ) + e ( w d z ) ) ) }
332, 3, 32cmpt 4077 . 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 ) + e ( w d z ) ) ) } )
341, 33wceq 1623 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 ) + e ( w d z ) ) ) } )
Colors of variables: wff set class
This definition is referenced by:  isxmet  17889  xmetunirn  17902
  Copyright terms: Public domain W3C validator