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

Definition df-met 16696
 Description: Define the (proper) class of all metrics. (A metric space is the metric's base set paired with the metric; see df-ms 18351. However, we will often also call the metric itself a "metric space".) Equivalent to Definition 14-1.1 of [Gleason] p. 223. The 4 properties in Gleason's definition are shown by met0 18373, metgt0 18389, metsym 18380, and mettri 18382. (Contributed by NM, 25-Aug-2006.)
Assertion
Ref Expression
df-met
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-met
StepHypRef Expression
1 cme 16687 . 2
2 vx . . 3
3 cvv 2956 . . 3
4 vy . . . . . . . . . . 11
54cv 1651 . . . . . . . . . 10
6 vz . . . . . . . . . . 11
76cv 1651 . . . . . . . . . 10
8 vd . . . . . . . . . . 11
98cv 1651 . . . . . . . . . 10
105, 7, 9co 6081 . . . . . . . . 9
11 cc0 8990 . . . . . . . . 9
1210, 11wceq 1652 . . . . . . . 8
134, 6weq 1653 . . . . . . . 8
1412, 13wb 177 . . . . . . 7
15 vw . . . . . . . . . . . 12
1615cv 1651 . . . . . . . . . . 11
1716, 5, 9co 6081 . . . . . . . . . 10
1816, 7, 9co 6081 . . . . . . . . . 10
19 caddc 8993 . . . . . . . . . 10
2017, 18, 19co 6081 . . . . . . . . 9
21 cle 9121 . . . . . . . . 9
2210, 20, 21wbr 4212 . . . . . . . 8
232cv 1651 . . . . . . . 8
2422, 15, 23wral 2705 . . . . . . 7
2514, 24wa 359 . . . . . 6
2625, 6, 23wral 2705 . . . . 5
2726, 4, 23wral 2705 . . . 4
28 cr 8989 . . . . 5
2923, 23cxp 4876 . . . . 5
30 cmap 7018 . . . . 5
3128, 29, 30co 6081 . . . 4
3227, 8, 31crab 2709 . . 3
332, 3, 32cmpt 4266 . 2
341, 33wceq 1652 1
 Colors of variables: wff set class This definition is referenced by:  ismet  18353
 Copyright terms: Public domain W3C validator