metidval

Description: Value of the metric identification relation. (Contributed by Thierry Arnoux, 7-Feb-2018)

		Ref	Expression
	Assertion	metidval	$⊢ D \in PsMet (X) \to ~_{Met} (D) = \{⟨x, y⟩ \| ((x \in X \land y \in X) \land x D y = 0)\}$

Proof

Step	Hyp	Ref	Expression
1		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)\})$
2		simpr	$⊢ (D \in PsMet (X) \land d = D) \to d = D$
3	2	dmeqd	$⊢ (D \in PsMet (X) \land d = D) \to dom d = dom D$
4	3	dmeqd	$⊢ (D \in PsMet (X) \land d = D) \to dom dom d = dom dom D$
5		psmetdmdm	$⊢ D \in PsMet (X) \to X = dom dom D$
6	5	adantr	$⊢ (D \in PsMet (X) \land d = D) \to X = dom dom D$
7	4 6	eqtr4d	$⊢ (D \in PsMet (X) \land d = D) \to dom dom d = X$
8	7	eleq2d	$⊢ (D \in PsMet (X) \land d = D) \to (x \in dom dom d \leftrightarrow x \in X)$
9	7	eleq2d	$⊢ (D \in PsMet (X) \land d = D) \to (y \in dom dom d \leftrightarrow y \in X)$
10	8 9	anbi12d	$⊢ (D \in PsMet (X) \land d = D) \to ((x \in dom dom d \land y \in dom dom d) \leftrightarrow (x \in X \land y \in X))$
11	2	oveqd	$⊢ (D \in PsMet (X) \land d = D) \to x d y = x D y$
12	11	eqeq1d	$⊢ (D \in PsMet (X) \land d = D) \to (x d y = 0 \leftrightarrow x D y = 0)$
13	10 12	anbi12d	$⊢ (D \in PsMet (X) \land d = D) \to (((x \in dom dom d \land y \in dom dom d) \land x d y = 0) \leftrightarrow ((x \in X \land y \in X) \land x D y = 0))$
14	13	opabbidv	$⊢ (D \in PsMet (X) \land d = D) \to \{⟨x, y⟩ \| ((x \in dom dom d \land y \in dom dom d) \land x d y = 0)\} = \{⟨x, y⟩ \| ((x \in X \land y \in X) \land x D y = 0)\}$
15		elfvunirn	$⊢ D \in PsMet (X) \to D \in ⋃ ran PsMet$
16		opabssxp	$⊢ \{⟨x, y⟩ \| ((x \in X \land y \in X) \land x D y = 0)\} \subseteq X \times X$
17		elfvex	$⊢ D \in PsMet (X) \to X \in V$
18	17 17	xpexd	$⊢ D \in PsMet (X) \to X \times X \in V$
19		ssexg	$⊢ (\{⟨x, y⟩ \| ((x \in X \land y \in X) \land x D y = 0)\} \subseteq X \times X \land X \times X \in V) \to \{⟨x, y⟩ \| ((x \in X \land y \in X) \land x D y = 0)\} \in V$
20	16 18 19	sylancr	$⊢ D \in PsMet (X) \to \{⟨x, y⟩ \| ((x \in X \land y \in X) \land x D y = 0)\} \in V$
21	1 14 15 20	fvmptd2	$⊢ D \in PsMet (X) \to ~_{Met} (D) = \{⟨x, y⟩ \| ((x \in X \land y \in X) \land x D y = 0)\}$

Metamath Proof Explorer

Theorem metidval

Proof