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 29905
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 29903 . 2 class ~Met
2 vd . . 3 setvar 𝑑
3 cpsmet 19711 . . . . 5 class PsMet
43crn 5105 . . . 4 class ran PsMet
54cuni 4427 . . 3 class ran PsMet
6 vx . . . . . . . 8 setvar 𝑥
76cv 1480 . . . . . . 7 class 𝑥
82cv 1480 . . . . . . . . 9 class 𝑑
98cdm 5104 . . . . . . . 8 class dom 𝑑
109cdm 5104 . . . . . . 7 class dom dom 𝑑
117, 10wcel 1988 . . . . . 6 wff 𝑥 ∈ dom dom 𝑑
12 vy . . . . . . . 8 setvar 𝑦
1312cv 1480 . . . . . . 7 class 𝑦
1413, 10wcel 1988 . . . . . 6 wff 𝑦 ∈ dom dom 𝑑
1511, 14wa 384 . . . . 5 wff (𝑥 ∈ dom dom 𝑑𝑦 ∈ dom dom 𝑑)
167, 13, 8co 6635 . . . . . 6 class (𝑥𝑑𝑦)
17 cc0 9921 . . . . . 6 class 0
1816, 17wceq 1481 . . . . 5 wff (𝑥𝑑𝑦) = 0
1915, 18wa 384 . . . 4 wff ((𝑥 ∈ dom dom 𝑑𝑦 ∈ dom dom 𝑑) ∧ (𝑥𝑑𝑦) = 0)
2019, 6, 12copab 4703 . . 3 class {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ dom dom 𝑑𝑦 ∈ dom dom 𝑑) ∧ (𝑥𝑑𝑦) = 0)}
212, 5, 20cmpt 4720 . 2 class (𝑑 ran PsMet ↦ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ dom dom 𝑑𝑦 ∈ dom dom 𝑑) ∧ (𝑥𝑑𝑦) = 0)})
221, 21wceq 1481 1 wff ~Met = (𝑑 ran PsMet ↦ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ dom dom 𝑑𝑦 ∈ dom dom 𝑑) ∧ (𝑥𝑑𝑦) = 0)})
Colors of variables: wff setvar class
This definition is referenced by:  metidval  29907
  Copyright terms: Public domain W3C validator