Definition df-psmet 21356

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 ↦ {𝑑 ∈ (ℝ* ↑m (𝑥 × 𝑥)) ∣ ∀𝑦 ∈ 𝑥 ((𝑦𝑑𝑦) = 0 ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧)))})

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

Detailed syntax breakdown of Definition df-psmet

Step	Hyp	Ref	Expression
1		cpsmet 21348	. 2 class PsMet
2		vx	. . 3 setvar 𝑥
3		cvv 3480	. . 3 class V
4		vy	. . . . . . . . 9 setvar 𝑦
5	4	cv 1539	. . . . . . . 8 class 𝑦
6		vd	. . . . . . . . 9 setvar 𝑑
7	6	cv 1539	. . . . . . . 8 class 𝑑
8	5, 5, 7	co 7431	. . . . . . 7 class (𝑦𝑑𝑦)
9		cc0 11155	. . . . . . 7 class 0
10	8, 9	wceq 1540	. . . . . 6 wff (𝑦𝑑𝑦) = 0
11		vz	. . . . . . . . . . 11 setvar 𝑧
12	11	cv 1539	. . . . . . . . . 10 class 𝑧
13	5, 12, 7	co 7431	. . . . . . . . 9 class (𝑦𝑑𝑧)
14		vw	. . . . . . . . . . . 12 setvar 𝑤
15	14	cv 1539	. . . . . . . . . . 11 class 𝑤
16	15, 5, 7	co 7431	. . . . . . . . . 10 class (𝑤𝑑𝑦)
17	15, 12, 7	co 7431	. . . . . . . . . 10 class (𝑤𝑑𝑧)
18		cxad 13152	. . . . . . . . . 10 class +𝑒
19	16, 17, 18	co 7431	. . . . . . . . 9 class ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧))
20		cle 11296	. . . . . . . . 9 class ≤
21	13, 19, 20	wbr 5143	. . . . . . . 8 wff (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧))
22	2	cv 1539	. . . . . . . 8 class 𝑥
23	21, 14, 22	wral 3061	. . . . . . 7 wff ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧))
24	23, 11, 22	wral 3061	. . . . . 6 wff ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧))
25	10, 24	wa 395	. . . . 5 wff ((𝑦𝑑𝑦) = 0 ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧)))
26	25, 4, 22	wral 3061	. . . 4 wff ∀𝑦 ∈ 𝑥 ((𝑦𝑑𝑦) = 0 ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧)))
27		cxr 11294	. . . . 5 class ℝ*
28	22, 22	cxp 5683	. . . . 5 class (𝑥 × 𝑥)
29		cmap 8866	. . . . 5 class ↑m
30	27, 28, 29	co 7431	. . . 4 class (ℝ* ↑m (𝑥 × 𝑥))
31	26, 6, 30	crab 3436	. . 3 class {𝑑 ∈ (ℝ* ↑m (𝑥 × 𝑥)) ∣ ∀𝑦 ∈ 𝑥 ((𝑦𝑑𝑦) = 0 ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧)))}
32	2, 3, 31	cmpt 5225	. 2 class (𝑥 ∈ V ↦ {𝑑 ∈ (ℝ* ↑m (𝑥 × 𝑥)) ∣ ∀𝑦 ∈ 𝑥 ((𝑦𝑑𝑦) = 0 ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧)))})
33	1, 32	wceq 1540	1 wff PsMet = (𝑥 ∈ V ↦ {𝑑 ∈ (ℝ* ↑m (𝑥 × 𝑥)) ∣ ∀𝑦 ∈ 𝑥 ((𝑦𝑑𝑦) = 0 ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧)))})

This definition is referenced by:  ispsmet  24314