Definition df-psmet 14852

Description: Define the set of all pseudometrics on a given base set. In a pseudo metric, two distinct points may have a distance zero. (Contributed by Thierry Arnoux, 7-Feb-2018.)

Assertion

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

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

Detailed syntax breakdown of Definition df-psmet

Step	Hyp	Ref	Expression
1		cpsmet 14844	. 2 class PsMet
2		vx	. . 3 setvar 𝑥
3		cvv 2821	. . 3 class V
4		vy	. . . . . . . . 9 setvar 𝑦
5	4	cv 1401	. . . . . . . 8 class 𝑦
6		vd	. . . . . . . . 9 setvar 𝑑
7	6	cv 1401	. . . . . . . 8 class 𝑑
8	5, 5, 7	co 6075	. . . . . . 7 class (𝑦𝑑𝑦)
9		cc0 8169	. . . . . . 7 class 0
10	8, 9	wceq 1402	. . . . . 6 wff (𝑦𝑑𝑦) = 0
11		vz	. . . . . . . . . . 11 setvar 𝑧
12	11	cv 1401	. . . . . . . . . 10 class 𝑧
13	5, 12, 7	co 6075	. . . . . . . . 9 class (𝑦𝑑𝑧)
14		vw	. . . . . . . . . . . 12 setvar 𝑤
15	14	cv 1401	. . . . . . . . . . 11 class 𝑤
16	15, 5, 7	co 6075	. . . . . . . . . 10 class (𝑤𝑑𝑦)
17	15, 12, 7	co 6075	. . . . . . . . . 10 class (𝑤𝑑𝑧)
18		cxad 10151	. . . . . . . . . 10 class +𝑒
19	16, 17, 18	co 6075	. . . . . . . . 9 class ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧))
20		cle 8351	. . . . . . . . 9 class ≤
21	13, 19, 20	wbr 4125	. . . . . . . 8 wff (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧))
22	2	cv 1401	. . . . . . . 8 class 𝑥
23	21, 14, 22	wral 2528	. . . . . . 7 wff ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧))
24	23, 11, 22	wral 2528	. . . . . 6 wff ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧))
25	10, 24	wa 104	. . . . 5 wff ((𝑦𝑑𝑦) = 0 ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧)))
26	25, 4, 22	wral 2528	. . . 4 wff ∀𝑦 ∈ 𝑥 ((𝑦𝑑𝑦) = 0 ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧)))
27		cxr 8349	. . . . 5 class ℝ*
28	22, 22	cxp 4767	. . . . 5 class (𝑥 × 𝑥)
29		cmap 6912	. . . . 5 class ↑𝑚
30	27, 28, 29	co 6075	. . . 4 class (ℝ* ↑𝑚 (𝑥 × 𝑥))
31	26, 6, 30	crab 2532	. . 3 class {𝑑 ∈ (ℝ* ↑𝑚 (𝑥 × 𝑥)) ∣ ∀𝑦 ∈ 𝑥 ((𝑦𝑑𝑦) = 0 ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧)))}
32	2, 3, 31	cmpt 4187	. 2 class (𝑥 ∈ V ↦ {𝑑 ∈ (ℝ* ↑𝑚 (𝑥 × 𝑥)) ∣ ∀𝑦 ∈ 𝑥 ((𝑦𝑑𝑦) = 0 ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧)))})
33	1, 32	wceq 1402	1 wff PsMet = (𝑥 ∈ V ↦ {𝑑 ∈ (ℝ* ↑𝑚 (𝑥 × 𝑥)) ∣ ∀𝑦 ∈ 𝑥 ((𝑦𝑑𝑦) = 0 ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧)))})

This definition is referenced by:  psmetrel  15346  ispsmet  15347  psmetdmdm  15348  psmetf  15349  psmet0  15351  psmettri2  15352  psmetres2  15357