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

Definition df-xmet 18962
Description: Define the set of all extended metrics on a given base set. The definition is similar to df-met 18963, 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 18954 . 2  class  *Met
2 vx . . 3  setvar  x
3 cvv 3080 . . 3  class  _V
4 vy . . . . . . . . . . 11  setvar  y
54cv 1436 . . . . . . . . . 10  class  y
6 vz . . . . . . . . . . 11  setvar  z
76cv 1436 . . . . . . . . . 10  class  z
8 vd . . . . . . . . . . 11  setvar  d
98cv 1436 . . . . . . . . . 10  class  d
105, 7, 9co 6305 . . . . . . . . 9  class  ( y d z )
11 cc0 9546 . . . . . . . . 9  class  0
1210, 11wceq 1437 . . . . . . . 8  wff  ( y d z )  =  0
134, 6weq 1784 . . . . . . . 8  wff  y  =  z
1412, 13wb 187 . . . . . . 7  wff  ( ( y d z )  =  0  <->  y  =  z )
15 vw . . . . . . . . . . . 12  setvar  w
1615cv 1436 . . . . . . . . . . 11  class  w
1716, 5, 9co 6305 . . . . . . . . . 10  class  ( w d y )
1816, 7, 9co 6305 . . . . . . . . . 10  class  ( w d z )
19 cxad 11414 . . . . . . . . . 10  class  +e
2017, 18, 19co 6305 . . . . . . . . 9  class  ( ( w d y ) +e ( w d z ) )
21 cle 9683 . . . . . . . . 9  class  <_
2210, 20, 21wbr 4423 . . . . . . . 8  wff  ( y d z )  <_ 
( ( w d y ) +e
( w d z ) )
232cv 1436 . . . . . . . 8  class  x
2422, 15, 23wral 2771 . . . . . . 7  wff  A. w  e.  x  ( y
d z )  <_ 
( ( w d y ) +e
( w d z ) )
2514, 24wa 370 . . . . . 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 2771 . . . . 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 2771 . . . 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 9681 . . . . 5  class  RR*
2923, 23cxp 4851 . . . . 5  class  ( x  X.  x )
30 cmap 7483 . . . . 5  class  ^m
3128, 29, 30co 6305 . . . 4  class  ( RR*  ^m  ( x  X.  x
) )
3227, 8, 31crab 2775 . . 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 4482 . 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 1437 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 setvar class
This definition is referenced by:  isxmet  21337  xmetunirn  21350
  Copyright terms: Public domain W3C validator