Definition df-psmet 12781

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 12773	. 2 class PsMet
2		vx	. . 3 setvar 𝑥
3		cvv 2730	. . 3 class V
4		vy	. . . . . . . . 9 setvar 𝑦
5	4	cv 1347	. . . . . . . 8 class 𝑦
6		vd	. . . . . . . . 9 setvar 𝑑
7	6	cv 1347	. . . . . . . 8 class 𝑑
8	5, 5, 7	co 5853	. . . . . . 7 class (𝑦𝑑𝑦)
9		cc0 7774	. . . . . . 7 class 0
10	8, 9	wceq 1348	. . . . . 6 wff (𝑦𝑑𝑦) = 0
11		vz	. . . . . . . . . . 11 setvar 𝑧
12	11	cv 1347	. . . . . . . . . 10 class 𝑧
13	5, 12, 7	co 5853	. . . . . . . . 9 class (𝑦𝑑𝑧)
14		vw	. . . . . . . . . . . 12 setvar 𝑤
15	14	cv 1347	. . . . . . . . . . 11 class 𝑤
16	15, 5, 7	co 5853	. . . . . . . . . 10 class (𝑤𝑑𝑦)
17	15, 12, 7	co 5853	. . . . . . . . . 10 class (𝑤𝑑𝑧)
18		cxad 9727	. . . . . . . . . 10 class +𝑒
19	16, 17, 18	co 5853	. . . . . . . . 9 class ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧))
20		cle 7955	. . . . . . . . 9 class ≤
21	13, 19, 20	wbr 3989	. . . . . . . 8 wff (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧))
22	2	cv 1347	. . . . . . . 8 class 𝑥
23	21, 14, 22	wral 2448	. . . . . . 7 wff ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧))
24	23, 11, 22	wral 2448	. . . . . 6 wff ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧))
25	10, 24	wa 103	. . . . 5 wff ((𝑦𝑑𝑦) = 0 ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧)))
26	25, 4, 22	wral 2448	. . . 4 wff ∀𝑦 ∈ 𝑥 ((𝑦𝑑𝑦) = 0 ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧)))
27		cxr 7953	. . . . 5 class ℝ*
28	22, 22	cxp 4609	. . . . 5 class (𝑥 × 𝑥)
29		cmap 6626	. . . . 5 class ↑𝑚
30	27, 28, 29	co 5853	. . . 4 class (ℝ* ↑𝑚 (𝑥 × 𝑥))
31	26, 6, 30	crab 2452	. . 3 class {𝑑 ∈ (ℝ* ↑𝑚 (𝑥 × 𝑥)) ∣ ∀𝑦 ∈ 𝑥 ((𝑦𝑑𝑦) = 0 ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧)))}
32	2, 3, 31	cmpt 4050	. 2 class (𝑥 ∈ V ↦ {𝑑 ∈ (ℝ* ↑𝑚 (𝑥 × 𝑥)) ∣ ∀𝑦 ∈ 𝑥 ((𝑦𝑑𝑦) = 0 ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧)))})
33	1, 32	wceq 1348	1 wff PsMet = (𝑥 ∈ V ↦ {𝑑 ∈ (ℝ* ↑𝑚 (𝑥 × 𝑥)) ∣ ∀𝑦 ∈ 𝑥 ((𝑦𝑑𝑦) = 0 ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧)))})

This definition is referenced by:  psmetrel  13116  ispsmet  13117  psmetdmdm  13118  psmetf  13119  psmet0  13121  psmettri2  13122  psmetres2  13127