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 ∈ x y d z = 0 ↔ y = z ∧ ∀ w ∈ x y d z ≤ w d y + w d z

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmet class Met
1 vx setvar x
2 cvv class V
3 vd setvar d
4 cr class ℝ
5 cmap class ↑ 𝑚
6 1 cv setvar x
7 6 6 cxp class x × x
8 4 7 5 co class ℝ x × x
9 vy setvar y
10 vz setvar z
11 9 cv setvar y
12 3 cv setvar d
13 10 cv setvar z
14 11 13 12 co class y d z
15 cc0 class 0
16 14 15 wceq wff y d z = 0
17 11 13 wceq wff y = z
18 16 17 wb wff y d z = 0 ↔ y = z
19 vw setvar w
20 cle class ≤
21 19 cv setvar w
22 21 11 12 co class w d y
23 caddc class +
24 21 13 12 co class w d z
25 22 24 23 co class w d y + w d z
26 14 25 20 wbr wff y d z ≤ w d y + w d z
27 26 19 6 wral wff ∀ w ∈ x y d z ≤ w d y + w d z
28 18 27 wa wff y d z = 0 ↔ y = z ∧ ∀ w ∈ x y d z ≤ w d y + w d z
29 28 10 6 wral wff ∀ z ∈ x y d z = 0 ↔ y = z ∧ ∀ w ∈ x y d z ≤ w d y + w d z
30 29 9 6 wral wff ∀ y ∈ x ∀ z ∈ x y d z = 0 ↔ y = z ∧ ∀ w ∈ x y d z ≤ w d y + w d z
31 30 3 8 crab class d ∈ ℝ x × x | ∀ y ∈ x ∀ z ∈ x y d z = 0 ↔ y = z ∧ ∀ w ∈ x y d z ≤ w d y + w d z
32 1 2 31 cmpt class x ∈ V ⟼ d ∈ ℝ x × x | ∀ y ∈ x ∀ z ∈ x y d z = 0 ↔ y = z ∧ ∀ w ∈ x y d z ≤ w d y + w d z
33 0 32 wceq wff Met = x ∈ V ⟼ d ∈ ℝ x × x | ∀ y ∈ x ∀ z ∈ x y d z = 0 ↔ y = z ∧ ∀ w ∈ x y d z ≤ w d y + w d z