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 29061
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 29059 . 2 class ~Met
2 vd . . 3 setvar 𝑑
3 cpsmet 19493 . . . . 5 class PsMet
43crn 5025 . . . 4 class ran PsMet
54cuni 4362 . . 3 class ran PsMet
6 vx . . . . . . . 8 setvar 𝑥
76cv 1473 . . . . . . 7 class 𝑥
82cv 1473 . . . . . . . . 9 class 𝑑
98cdm 5024 . . . . . . . 8 class dom 𝑑
109cdm 5024 . . . . . . 7 class dom dom 𝑑
117, 10wcel 1975 . . . . . 6 wff 𝑥 ∈ dom dom 𝑑
12 vy . . . . . . . 8 setvar 𝑦
1312cv 1473 . . . . . . 7 class 𝑦
1413, 10wcel 1975 . . . . . 6 wff 𝑦 ∈ dom dom 𝑑
1511, 14wa 382 . . . . 5 wff (𝑥 ∈ dom dom 𝑑𝑦 ∈ dom dom 𝑑)
167, 13, 8co 6523 . . . . . 6 class (𝑥𝑑𝑦)
17 cc0 9788 . . . . . 6 class 0
1816, 17wceq 1474 . . . . 5 wff (𝑥𝑑𝑦) = 0
1915, 18wa 382 . . . 4 wff ((𝑥 ∈ dom dom 𝑑𝑦 ∈ dom dom 𝑑) ∧ (𝑥𝑑𝑦) = 0)
2019, 6, 12copab 4632 . . 3 class {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ dom dom 𝑑𝑦 ∈ dom dom 𝑑) ∧ (𝑥𝑑𝑦) = 0)}
212, 5, 20cmpt 4633 . 2 class (𝑑 ran PsMet ↦ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ dom dom 𝑑𝑦 ∈ dom dom 𝑑) ∧ (𝑥𝑑𝑦) = 0)})
221, 21wceq 1474 1 wff ~Met = (𝑑 ran PsMet ↦ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ dom dom 𝑑𝑦 ∈ dom dom 𝑑) ∧ (𝑥𝑑𝑦) = 0)})
Colors of variables: wff setvar class
This definition is referenced by:  metidval  29063
  Copyright terms: Public domain W3C validator