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

Definition df-xmet 12230
 Description: Define the set of all extended metrics on a given base set. The definition is similar to df-met 12231, but we also allow the metric to take on the value +∞. (Contributed by Mario Carneiro, 20-Aug-2015.)
Assertion
Ref Expression
df-xmet ∞Met = (𝑥 ∈ V ↦ {𝑑 ∈ (ℝ*𝑚 (𝑥 × 𝑥)) ∣ ∀𝑦𝑥𝑧𝑥 (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ ∀𝑤𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧)))})
Distinct variable group:   𝑥,𝑑,𝑦,𝑧,𝑤

Detailed syntax breakdown of Definition df-xmet
StepHypRef Expression
1 cxmet 12222 . 2 class ∞Met
2 vx . . 3 setvar 𝑥
3 cvv 2690 . . 3 class V
4 vy . . . . . . . . . . 11 setvar 𝑦
54cv 1331 . . . . . . . . . 10 class 𝑦
6 vz . . . . . . . . . . 11 setvar 𝑧
76cv 1331 . . . . . . . . . 10 class 𝑧
8 vd . . . . . . . . . . 11 setvar 𝑑
98cv 1331 . . . . . . . . . 10 class 𝑑
105, 7, 9co 5785 . . . . . . . . 9 class (𝑦𝑑𝑧)
11 cc0 7671 . . . . . . . . 9 class 0
1210, 11wceq 1332 . . . . . . . 8 wff (𝑦𝑑𝑧) = 0
134, 6weq 1480 . . . . . . . 8 wff 𝑦 = 𝑧
1412, 13wb 104 . . . . . . 7 wff ((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧)
15 vw . . . . . . . . . . . 12 setvar 𝑤
1615cv 1331 . . . . . . . . . . 11 class 𝑤
1716, 5, 9co 5785 . . . . . . . . . 10 class (𝑤𝑑𝑦)
1816, 7, 9co 5785 . . . . . . . . . 10 class (𝑤𝑑𝑧)
19 cxad 9614 . . . . . . . . . 10 class +𝑒
2017, 18, 19co 5785 . . . . . . . . 9 class ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧))
21 cle 7852 . . . . . . . . 9 class
2210, 20, 21wbr 3938 . . . . . . . 8 wff (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧))
232cv 1331 . . . . . . . 8 class 𝑥
2422, 15, 23wral 2417 . . . . . . 7 wff 𝑤𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧))
2514, 24wa 103 . . . . . 6 wff (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ ∀𝑤𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧)))
2625, 6, 23wral 2417 . . . . 5 wff 𝑧𝑥 (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ ∀𝑤𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧)))
2726, 4, 23wral 2417 . . . 4 wff 𝑦𝑥𝑧𝑥 (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ ∀𝑤𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧)))
28 cxr 7850 . . . . 5 class *
2923, 23cxp 4548 . . . . 5 class (𝑥 × 𝑥)
30 cmap 6553 . . . . 5 class 𝑚
3128, 29, 30co 5785 . . . 4 class (ℝ*𝑚 (𝑥 × 𝑥))
3227, 8, 31crab 2421 . . 3 class {𝑑 ∈ (ℝ*𝑚 (𝑥 × 𝑥)) ∣ ∀𝑦𝑥𝑧𝑥 (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ ∀𝑤𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧)))}
332, 3, 32cmpt 3998 . 2 class (𝑥 ∈ V ↦ {𝑑 ∈ (ℝ*𝑚 (𝑥 × 𝑥)) ∣ ∀𝑦𝑥𝑧𝑥 (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ ∀𝑤𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧)))})
341, 33wceq 1332 1 wff ∞Met = (𝑥 ∈ V ↦ {𝑑 ∈ (ℝ*𝑚 (𝑥 × 𝑥)) ∣ ∀𝑦𝑥𝑧𝑥 (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ ∀𝑤𝑥 (𝑦𝑑𝑧) ≤ ((𝑤𝑑𝑦) +𝑒 (𝑤𝑑𝑧)))})
 Colors of variables: wff set class This definition is referenced by:  xmetrel  12585  isxmet  12587  xmetf  12592  xmetunirn  12600
 Copyright terms: Public domain W3C validator