Definition df-met 20241

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

Assertion

Ref	Expression
df-met	⊢ Met = (𝑥 ∈ V ↦ {𝑑 ∈ (ℝ ↑𝑚 (𝑥 × 𝑥)) ∣ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) + (𝑤𝑑𝑧)))})

Distinct variable group:   𝑥,𝑑,𝑦,𝑧,𝑤

Detailed syntax breakdown of Definition df-met

Step	Hyp	Ref	Expression
1		cmet 20233	. 2 class Met
2		vx	. . 3 setvar 𝑥
3		cvv 3416	. . 3 class V
4		vy	. . . . . . . . . . 11 setvar 𝑦
5	4	cv 1506	. . . . . . . . . 10 class 𝑦
6		vz	. . . . . . . . . . 11 setvar 𝑧
7	6	cv 1506	. . . . . . . . . 10 class 𝑧
8		vd	. . . . . . . . . . 11 setvar 𝑑
9	8	cv 1506	. . . . . . . . . 10 class 𝑑
10	5, 7, 9	co 6976	. . . . . . . . 9 class (𝑦𝑑𝑧)
11		cc0 10335	. . . . . . . . 9 class 0
12	10, 11	wceq 1507	. . . . . . . 8 wff (𝑦𝑑𝑧) = 0
13	4, 6	weq 1922	. . . . . . . 8 wff 𝑦 = 𝑧
14	12, 13	wb 198	. . . . . . 7 wff ((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧)
15		vw	. . . . . . . . . . . 12 setvar 𝑤
16	15	cv 1506	. . . . . . . . . . 11 class 𝑤
17	16, 5, 9	co 6976	. . . . . . . . . 10 class (𝑤𝑑𝑦)
18	16, 7, 9	co 6976	. . . . . . . . . 10 class (𝑤𝑑𝑧)
19		caddc 10338	. . . . . . . . . 10 class +
20	17, 18, 19	co 6976	. . . . . . . . 9 class ((𝑤𝑑𝑦) + (𝑤𝑑𝑧))
21		cle 10475	. . . . . . . . 9 class ≤
22	10, 20, 21	wbr 4929	. . . . . . . 8 wff (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) + (𝑤𝑑𝑧))
23	2	cv 1506	. . . . . . . 8 class 𝑥
24	22, 15, 23	wral 3089	. . . . . . 7 wff ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) + (𝑤𝑑𝑧))
25	14, 24	wa 387	. . . . . 6 wff (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) + (𝑤𝑑𝑧)))
26	25, 6, 23	wral 3089	. . . . 5 wff ∀𝑧 ∈ 𝑥 (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) + (𝑤𝑑𝑧)))
27	26, 4, 23	wral 3089	. . . 4 wff ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) + (𝑤𝑑𝑧)))
28		cr 10334	. . . . 5 class ℝ
29	23, 23	cxp 5405	. . . . 5 class (𝑥 × 𝑥)
30		cmap 8206	. . . . 5 class ↑𝑚
31	28, 29, 30	co 6976	. . . 4 class (ℝ ↑𝑚 (𝑥 × 𝑥))
32	27, 8, 31	crab 3093	. . 3 class {𝑑 ∈ (ℝ ↑𝑚 (𝑥 × 𝑥)) ∣ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) + (𝑤𝑑𝑧)))}
33	2, 3, 32	cmpt 5008	. 2 class (𝑥 ∈ V ↦ {𝑑 ∈ (ℝ ↑𝑚 (𝑥 × 𝑥)) ∣ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) + (𝑤𝑑𝑧)))})
34	1, 33	wceq 1507	1 wff Met = (𝑥 ∈ V ↦ {𝑑 ∈ (ℝ ↑𝑚 (𝑥 × 𝑥)) ∣ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) + (𝑤𝑑𝑧)))})

This definition is referenced by:  ismet  22636