Definition df-metid 31344

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

Step	Hyp	Ref	Expression
1		cmetid 31342	. 2 class ~Met
2		vd	. . 3 setvar 𝑑
3		cpsmet 20135	. . . . 5 class PsMet
4	3	crn 5518	. . . 4 class ran PsMet
5	4	cuni 4791	. . 3 class ∪ ran PsMet
6		vx	. . . . . . . 8 setvar 𝑥
7	6	cv 1538	. . . . . . 7 class 𝑥
8	2	cv 1538	. . . . . . . . 9 class 𝑑
9	8	cdm 5517	. . . . . . . 8 class dom 𝑑
10	9	cdm 5517	. . . . . . 7 class dom dom 𝑑
11	7, 10	wcel 2112	. . . . . 6 wff 𝑥 ∈ dom dom 𝑑
12		vy	. . . . . . . 8 setvar 𝑦
13	12	cv 1538	. . . . . . 7 class 𝑦
14	13, 10	wcel 2112	. . . . . 6 wff 𝑦 ∈ dom dom 𝑑
15	11, 14	wa 400	. . . . 5 wff (𝑥 ∈ dom dom 𝑑 ∧ 𝑦 ∈ dom dom 𝑑)
16	7, 13, 8	co 7143	. . . . . 6 class (𝑥𝑑𝑦)
17		cc0 10560	. . . . . 6 class 0
18	16, 17	wceq 1539	. . . . 5 wff (𝑥𝑑𝑦) = 0
19	15, 18	wa 400	. . . 4 wff ((𝑥 ∈ dom dom 𝑑 ∧ 𝑦 ∈ dom dom 𝑑) ∧ (𝑥𝑑𝑦) = 0)
20	19, 6, 12	copab 5087	. . 3 class {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ dom dom 𝑑 ∧ 𝑦 ∈ dom dom 𝑑) ∧ (𝑥𝑑𝑦) = 0)}
21	2, 5, 20	cmpt 5105	. 2 class (𝑑 ∈ ∪ ran PsMet ↦ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ dom dom 𝑑 ∧ 𝑦 ∈ dom dom 𝑑) ∧ (𝑥𝑑𝑦) = 0)})
22	1, 21	wceq 1539	1 wff ~Met = (𝑑 ∈ ∪ ran PsMet ↦ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ dom dom 𝑑 ∧ 𝑦 ∈ dom dom 𝑑) ∧ (𝑥𝑑𝑦) = 0)})

This definition is referenced by:  metidval  31346