MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-xmet Structured version   Visualization version   GIF version

Definition df-xmet 21228
Description: Define the set of all extended metrics on a given base set. The definition is similar to df-met 21229, 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 ↦ {𝑑 ∈ (ℝ* ↑m (π‘₯ Γ— π‘₯)) ∣ βˆ€π‘¦ ∈ π‘₯ βˆ€π‘§ ∈ π‘₯ (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ βˆ€π‘€ ∈ π‘₯ (𝑦𝑑𝑧) ≀ ((𝑀𝑑𝑦) +𝑒 (𝑀𝑑𝑧)))})
Distinct variable group:   π‘₯,𝑑,𝑦,𝑧,𝑀

Detailed syntax breakdown of Definition df-xmet
StepHypRef Expression
1 cxmet 21220 . 2 class ∞Met
2 vx . . 3 setvar π‘₯
3 cvv 3468 . . 3 class V
4 vy . . . . . . . . . . 11 setvar 𝑦
54cv 1532 . . . . . . . . . 10 class 𝑦
6 vz . . . . . . . . . . 11 setvar 𝑧
76cv 1532 . . . . . . . . . 10 class 𝑧
8 vd . . . . . . . . . . 11 setvar 𝑑
98cv 1532 . . . . . . . . . 10 class 𝑑
105, 7, 9co 7404 . . . . . . . . 9 class (𝑦𝑑𝑧)
11 cc0 11109 . . . . . . . . 9 class 0
1210, 11wceq 1533 . . . . . . . 8 wff (𝑦𝑑𝑧) = 0
134, 6weq 1958 . . . . . . . 8 wff 𝑦 = 𝑧
1412, 13wb 205 . . . . . . 7 wff ((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧)
15 vw . . . . . . . . . . . 12 setvar 𝑀
1615cv 1532 . . . . . . . . . . 11 class 𝑀
1716, 5, 9co 7404 . . . . . . . . . 10 class (𝑀𝑑𝑦)
1816, 7, 9co 7404 . . . . . . . . . 10 class (𝑀𝑑𝑧)
19 cxad 13093 . . . . . . . . . 10 class +𝑒
2017, 18, 19co 7404 . . . . . . . . 9 class ((𝑀𝑑𝑦) +𝑒 (𝑀𝑑𝑧))
21 cle 11250 . . . . . . . . 9 class ≀
2210, 20, 21wbr 5141 . . . . . . . 8 wff (𝑦𝑑𝑧) ≀ ((𝑀𝑑𝑦) +𝑒 (𝑀𝑑𝑧))
232cv 1532 . . . . . . . 8 class π‘₯
2422, 15, 23wral 3055 . . . . . . 7 wff βˆ€π‘€ ∈ π‘₯ (𝑦𝑑𝑧) ≀ ((𝑀𝑑𝑦) +𝑒 (𝑀𝑑𝑧))
2514, 24wa 395 . . . . . 6 wff (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ βˆ€π‘€ ∈ π‘₯ (𝑦𝑑𝑧) ≀ ((𝑀𝑑𝑦) +𝑒 (𝑀𝑑𝑧)))
2625, 6, 23wral 3055 . . . . 5 wff βˆ€π‘§ ∈ π‘₯ (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ βˆ€π‘€ ∈ π‘₯ (𝑦𝑑𝑧) ≀ ((𝑀𝑑𝑦) +𝑒 (𝑀𝑑𝑧)))
2726, 4, 23wral 3055 . . . 4 wff βˆ€π‘¦ ∈ π‘₯ βˆ€π‘§ ∈ π‘₯ (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ βˆ€π‘€ ∈ π‘₯ (𝑦𝑑𝑧) ≀ ((𝑀𝑑𝑦) +𝑒 (𝑀𝑑𝑧)))
28 cxr 11248 . . . . 5 class ℝ*
2923, 23cxp 5667 . . . . 5 class (π‘₯ Γ— π‘₯)
30 cmap 8819 . . . . 5 class ↑m
3128, 29, 30co 7404 . . . 4 class (ℝ* ↑m (π‘₯ Γ— π‘₯))
3227, 8, 31crab 3426 . . 3 class {𝑑 ∈ (ℝ* ↑m (π‘₯ Γ— π‘₯)) ∣ βˆ€π‘¦ ∈ π‘₯ βˆ€π‘§ ∈ π‘₯ (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ βˆ€π‘€ ∈ π‘₯ (𝑦𝑑𝑧) ≀ ((𝑀𝑑𝑦) +𝑒 (𝑀𝑑𝑧)))}
332, 3, 32cmpt 5224 . 2 class (π‘₯ ∈ V ↦ {𝑑 ∈ (ℝ* ↑m (π‘₯ Γ— π‘₯)) ∣ βˆ€π‘¦ ∈ π‘₯ βˆ€π‘§ ∈ π‘₯ (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ βˆ€π‘€ ∈ π‘₯ (𝑦𝑑𝑧) ≀ ((𝑀𝑑𝑦) +𝑒 (𝑀𝑑𝑧)))})
341, 33wceq 1533 1 wff ∞Met = (π‘₯ ∈ V ↦ {𝑑 ∈ (ℝ* ↑m (π‘₯ Γ— π‘₯)) ∣ βˆ€π‘¦ ∈ π‘₯ βˆ€π‘§ ∈ π‘₯ (((𝑦𝑑𝑧) = 0 ↔ 𝑦 = 𝑧) ∧ βˆ€π‘€ ∈ π‘₯ (𝑦𝑑𝑧) ≀ ((𝑀𝑑𝑦) +𝑒 (𝑀𝑑𝑧)))})
Colors of variables: wff setvar class
This definition is referenced by:  isxmet  24180  xmetunirn  24193
  Copyright terms: Public domain W3C validator