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 30271
 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 30269 . 2 class ~Met
2 vd . . 3 setvar 𝑑
3 cpsmet 19945 . . . . 5 class PsMet
43crn 5250 . . . 4 class ran PsMet
54cuni 4574 . . 3 class ran PsMet
6 vx . . . . . . . 8 setvar 𝑥
76cv 1630 . . . . . . 7 class 𝑥
82cv 1630 . . . . . . . . 9 class 𝑑
98cdm 5249 . . . . . . . 8 class dom 𝑑
109cdm 5249 . . . . . . 7 class dom dom 𝑑
117, 10wcel 2145 . . . . . 6 wff 𝑥 ∈ dom dom 𝑑
12 vy . . . . . . . 8 setvar 𝑦
1312cv 1630 . . . . . . 7 class 𝑦
1413, 10wcel 2145 . . . . . 6 wff 𝑦 ∈ dom dom 𝑑
1511, 14wa 382 . . . . 5 wff (𝑥 ∈ dom dom 𝑑𝑦 ∈ dom dom 𝑑)
167, 13, 8co 6793 . . . . . 6 class (𝑥𝑑𝑦)
17 cc0 10138 . . . . . 6 class 0
1816, 17wceq 1631 . . . . 5 wff (𝑥𝑑𝑦) = 0
1915, 18wa 382 . . . 4 wff ((𝑥 ∈ dom dom 𝑑𝑦 ∈ dom dom 𝑑) ∧ (𝑥𝑑𝑦) = 0)
2019, 6, 12copab 4846 . . 3 class {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ dom dom 𝑑𝑦 ∈ dom dom 𝑑) ∧ (𝑥𝑑𝑦) = 0)}
212, 5, 20cmpt 4863 . 2 class (𝑑 ran PsMet ↦ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ dom dom 𝑑𝑦 ∈ dom dom 𝑑) ∧ (𝑥𝑑𝑦) = 0)})
221, 21wceq 1631 1 wff ~Met = (𝑑 ran PsMet ↦ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ dom dom 𝑑𝑦 ∈ dom dom 𝑑) ∧ (𝑥𝑑𝑦) = 0)})
 Colors of variables: wff setvar class This definition is referenced by:  metidval  30273
 Copyright terms: Public domain W3C validator