Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-psmet GIF version

Definition df-psmet 12182
 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
StepHypRef Expression
1 cpsmet 12174 . 2 class PsMet
2 vx . . 3 setvar 𝑥
3 cvv 2686 . . 3 class V
4 vy . . . . . . . . 9 setvar 𝑦
54cv 1330 . . . . . . . 8 class 𝑦
6 vd . . . . . . . . 9 setvar 𝑑
76cv 1330 . . . . . . . 8 class 𝑑
85, 5, 7co 5777 . . . . . . 7 class (𝑦𝑑𝑦)
9 cc0 7639 . . . . . . 7 class 0
108, 9wceq 1331 . . . . . 6 wff (𝑦𝑑𝑦) = 0
11 vz . . . . . . . . . . 11 setvar 𝑧
1211cv 1330 . . . . . . . . . 10 class 𝑧
135, 12, 7co 5777 . . . . . . . . 9 class (𝑦𝑑𝑧)
14 vw . . . . . . . . . . . 12 setvar 𝑤
1514cv 1330 . . . . . . . . . . 11 class 𝑤
1615, 5, 7co 5777 . . . . . . . . . 10 class (𝑤𝑑𝑦)
1715, 12, 7co 5777 . . . . . . . . . 10 class (𝑤𝑑𝑧)
18 cxad 9580 . . . . . . . . . 10 class +𝑒
1916, 17, 18co 5777 . . . . . . . . 9 class ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧))
20 cle 7820 . . . . . . . . 9 class
2113, 19, 20wbr 3932 . . . . . . . 8 wff (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧))
222cv 1330 . . . . . . . 8 class 𝑥
2321, 14, 22wral 2416 . . . . . . 7 wff 𝑤𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧))
2423, 11, 22wral 2416 . . . . . 6 wff 𝑧𝑥𝑤𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧))
2510, 24wa 103 . . . . 5 wff ((𝑦𝑑𝑦) = 0 ∧ ∀𝑧𝑥𝑤𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧)))
2625, 4, 22wral 2416 . . . 4 wff 𝑦𝑥 ((𝑦𝑑𝑦) = 0 ∧ ∀𝑧𝑥𝑤𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧)))
27 cxr 7818 . . . . 5 class *
2822, 22cxp 4540 . . . . 5 class (𝑥 × 𝑥)
29 cmap 6545 . . . . 5 class 𝑚
3027, 28, 29co 5777 . . . 4 class (ℝ*𝑚 (𝑥 × 𝑥))
3126, 6, 30crab 2420 . . 3 class {𝑑 ∈ (ℝ*𝑚 (𝑥 × 𝑥)) ∣ ∀𝑦𝑥 ((𝑦𝑑𝑦) = 0 ∧ ∀𝑧𝑥𝑤𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧)))}
322, 3, 31cmpt 3992 . 2 class (𝑥 ∈ V ↦ {𝑑 ∈ (ℝ*𝑚 (𝑥 × 𝑥)) ∣ ∀𝑦𝑥 ((𝑦𝑑𝑦) = 0 ∧ ∀𝑧𝑥𝑤𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧)))})
331, 32wceq 1331 1 wff PsMet = (𝑥 ∈ V ↦ {𝑑 ∈ (ℝ*𝑚 (𝑥 × 𝑥)) ∣ ∀𝑦𝑥 ((𝑦𝑑𝑦) = 0 ∧ ∀𝑧𝑥𝑤𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧)))})
 Colors of variables: wff set class This definition is referenced by:  psmetrel  12517  ispsmet  12518  psmetdmdm  12519  psmetf  12520  psmet0  12522  psmettri2  12523  psmetres2  12528
 Copyright terms: Public domain W3C validator