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

Definition df-xmet 17790
Description: Define the set of all extended metrics on a given base set. The definition is similar to df-met 17791, but we also allow the metric to take on the value . (Contributed by Mario Carneiro, 20-Aug-2015.)
Assertion
Ref Expression
df-xmet
Distinct variable group:   , , , ,

Detailed syntax breakdown of Definition df-xmet
StepHypRef Expression
1 cxmt 17781 . 2
2 vx . . 3
3 cvv 2967 . . 3
4 vy . . . . . . . . . . 11
54cv 1368 . . . . . . . . . 10
6 vz . . . . . . . . . . 11
76cv 1368 . . . . . . . . . 10
8 vd . . . . . . . . . . 11
98cv 1368 . . . . . . . . . 10
105, 7, 9co 6086 . . . . . . . . 9
11 cc0 9274 . . . . . . . . 9
1210, 11wceq 1369 . . . . . . . 8
134, 6weq 1695 . . . . . . . 8
1412, 13wb 184 . . . . . . 7
15 vw . . . . . . . . . . . 12
1615cv 1368 . . . . . . . . . . 11
1716, 5, 9co 6086 . . . . . . . . . 10
1816, 7, 9co 6086 . . . . . . . . . 10
19 cxad 11079 . . . . . . . . . 10
2017, 18, 19co 6086 . . . . . . . . 9
21 cle 9411 . . . . . . . . 9
2210, 20, 21wbr 4287 . . . . . . . 8
232cv 1368 . . . . . . . 8
2422, 15, 23wral 2710 . . . . . . 7
2514, 24wa 369 . . . . . 6
2625, 6, 23wral 2710 . . . . 5
2726, 4, 23wral 2710 . . . 4
28 cxr 9409 . . . . 5
2923, 23cxp 4833 . . . . 5
30 cmap 7206 . . . . 5
3128, 29, 30co 6086 . . . 4
3227, 8, 31crab 2714 . . 3
332, 3, 32cmpt 4345 . 2
341, 33wceq 1369 1
Colors of variables: wff setvar class
This definition is referenced by:  isxmet  19879  xmetunirn  19892  metuvalOLD  20104
  Copyright terms: Public domain W3C validator