df-metid

Description: Define the metric identification relation for a pseudometric. (Contributed by Thierry Arnoux, 7-Feb-2018)

		Ref	Expression
	Assertion	df-metid	$⊢ ~_{Met} = (d \in ⋃ ran PsMet ⟼ \{⟨x, y⟩ \| ((x \in dom dom d \land y \in dom dom d) \land x d y = 0)\})$

Step	Hyp	Ref	Expression
0		cmetid	$class ~_{Met}$
1		vd	$setvar d$
2		cpsmet	$class PsMet$
3	2	crn	$class ran PsMet$
4	3	cuni	$class ⋃ ran PsMet$
5		vx	$setvar x$
6		vy	$setvar y$
7	5	cv	$setvar x$
8	1	cv	$setvar d$
9	8	cdm	$class dom d$
10	9	cdm	$class dom dom d$
11	7 10	wcel	$wff x \in dom dom d$
12	6	cv	$setvar y$
13	12 10	wcel	$wff y \in dom dom d$
14	11 13	wa	$wff (x \in dom dom d \land y \in dom dom d)$
15	7 12 8	co	$class (x d y)$
16		cc0	$class 0$
17	15 16	wceq	$wff x d y = 0$
18	14 17	wa	$wff ((x \in dom dom d \land y \in dom dom d) \land x d y = 0)$
19	18 5 6	copab	$class \{⟨x, y⟩ \| ((x \in dom dom d \land y \in dom dom d) \land x d y = 0)\}$
20	1 4 19	cmpt	$class (d \in ⋃ ran PsMet ⟼ \{⟨x, y⟩ \| ((x \in dom dom d \land y \in dom dom d) \land x d y = 0)\})$
21	0 20	wceq	$wff ~_{Met} = (d \in ⋃ ran PsMet ⟼ \{⟨x, y⟩ \| ((x \in dom dom d \land y \in dom dom d) \land x d y = 0)\})$

Metamath Proof Explorer