Metamath Proof Explorer

Definition df-met

Description: Define the (proper) class of all metrics. (A metric space is the metric's base set paired with the metric; see df-ms . 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 , metgt0 , metsym , and mettri . (Contributed by NM, 25-Aug-2006)

Ref Expression
Assertion df-met ⊢Met=x∈V⟼d∈ℝx×x|∀y∈x∀z∈xydz=0↔y=z∧∀w∈xydz≤wdy+wdz

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmet classMet
1 vx setvarx
2 cvv classV
3 vd setvard
4 cr classℝ
5 cmap class↑𝑚
6 1 cv setvarx
7 6 6 cxp classx×x
8 4 7 5 co classℝx×x
9 vy setvary
10 vz setvarz
11 9 cv setvary
12 3 cv setvard
13 10 cv setvarz
14 11 13 12 co classydz
15 cc0 class0
16 14 15 wceq wffydz=0
17 11 13 wceq wffy=z
18 16 17 wb wffydz=0↔y=z
19 vw setvarw
20 cle class≤
21 19 cv setvarw
22 21 11 12 co classwdy
23 caddc class+
24 21 13 12 co classwdz
25 22 24 23 co classwdy+wdz
26 14 25 20 wbr wffydz≤wdy+wdz
27 26 19 6 wral wff∀w∈xydz≤wdy+wdz
28 18 27 wa wffydz=0↔y=z∧∀w∈xydz≤wdy+wdz
29 28 10 6 wral wff∀z∈xydz=0↔y=z∧∀w∈xydz≤wdy+wdz
30 29 9 6 wral wff∀y∈x∀z∈xydz=0↔y=z∧∀w∈xydz≤wdy+wdz
31 30 3 8 crab classd∈ℝx×x|∀y∈x∀z∈xydz=0↔y=z∧∀w∈xydz≤wdy+wdz
32 1 2 31 cmpt classx∈V⟼d∈ℝx×x|∀y∈x∀z∈xydz=0↔y=z∧∀w∈xydz≤wdy+wdz
33 0 32 wceq wffMet=x∈V⟼d∈ℝx×x|∀y∈x∀z∈xydz=0↔y=z∧∀w∈xydz≤wdy+wdz