Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-metid Structured version   Visualization version   GIF version

Definition df-metid 31825
Description: Define the metric identification relation for a pseudometric. (Contributed by Thierry Arnoux, 7-Feb-2018.)
Assertion
Ref Expression
df-metid ~Met = (𝑑 ran PsMet ↦ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ dom dom 𝑑𝑦 ∈ dom dom 𝑑) ∧ (𝑥𝑑𝑦) = 0)})
Distinct variable group:   𝑥,𝑑,𝑦

Detailed syntax breakdown of Definition df-metid
StepHypRef Expression
1 cmetid 31823 . 2 class ~Met
2 vd . . 3 setvar 𝑑
3 cpsmet 20570 . . . . 5 class PsMet
43crn 5587 . . . 4 class ran PsMet
54cuni 4841 . . 3 class ran PsMet
6 vx . . . . . . . 8 setvar 𝑥
76cv 1538 . . . . . . 7 class 𝑥
82cv 1538 . . . . . . . . 9 class 𝑑
98cdm 5586 . . . . . . . 8 class dom 𝑑
109cdm 5586 . . . . . . 7 class dom dom 𝑑
117, 10wcel 2106 . . . . . 6 wff 𝑥 ∈ dom dom 𝑑
12 vy . . . . . . . 8 setvar 𝑦
1312cv 1538 . . . . . . 7 class 𝑦
1413, 10wcel 2106 . . . . . 6 wff 𝑦 ∈ dom dom 𝑑
1511, 14wa 396 . . . . 5 wff (𝑥 ∈ dom dom 𝑑𝑦 ∈ dom dom 𝑑)
167, 13, 8co 7269 . . . . . 6 class (𝑥𝑑𝑦)
17 cc0 10860 . . . . . 6 class 0
1816, 17wceq 1539 . . . . 5 wff (𝑥𝑑𝑦) = 0
1915, 18wa 396 . . . 4 wff ((𝑥 ∈ dom dom 𝑑𝑦 ∈ dom dom 𝑑) ∧ (𝑥𝑑𝑦) = 0)
2019, 6, 12copab 5137 . . 3 class {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ dom dom 𝑑𝑦 ∈ dom dom 𝑑) ∧ (𝑥𝑑𝑦) = 0)}
212, 5, 20cmpt 5158 . 2 class (𝑑 ran PsMet ↦ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ dom dom 𝑑𝑦 ∈ dom dom 𝑑) ∧ (𝑥𝑑𝑦) = 0)})
221, 21wceq 1539 1 wff ~Met = (𝑑 ran PsMet ↦ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ dom dom 𝑑𝑦 ∈ dom dom 𝑑) ∧ (𝑥𝑑𝑦) = 0)})
Colors of variables: wff setvar class
This definition is referenced by:  metidval  31827
  Copyright terms: Public domain W3C validator