Theorem metidss

Description: As a relation, the metric identification is a subset of a Cartesian product. (Contributed by Thierry Arnoux, 7-Feb-2018)

	Ref	Expression
Assertion	metidss	$$⊢D\in \mathrm{PsMet}\left(X\right)\to {~}_{\mathit{Met}}\left(D\right)\subseteq X\times X$$

Proof

Step	Hyp	Ref	Expression
1		metidval	$$⊢D\in \mathrm{PsMet}\left(X\right)\to {~}_{\mathit{Met}}\left(D\right)=\left\{⟨x,y⟩|\left(\left(x\in X\wedge y\in X\right)\wedge xDy=0\right)\right\}$$
2		opabssxp	$$⊢\left\{⟨x,y⟩|\left(\left(x\in X\wedge y\in X\right)\wedge xDy=0\right)\right\}\subseteq X\times X$$
3	1 2	eqsstrdi	$$⊢D\in \mathrm{PsMet}\left(X\right)\to {~}_{\mathit{Met}}\left(D\right)\subseteq X\times X$$