metreslem

		Ref	Expression
	Assertion	metreslem	$⊢ dom D = X \times X \to {D ↾}_{(R \times R)} = {D ↾}_{((X \cap R) \times (X \cap R))}$

Step	Hyp	Ref	Expression
1		resdmres	$⊢ {D ↾}_{dom ({D ↾}_{(R \times R)})} = {D ↾}_{(R \times R)}$
2		ineq2	$⊢ dom D = X \times X \to (R \times R) \cap dom D = (R \times R) \cap (X \times X)$
3		dmres	$⊢ dom ({D ↾}_{(R \times R)}) = (R \times R) \cap dom D$
4		inxp	$⊢ (X \times X) \cap (R \times R) = (X \cap R) \times (X \cap R)$
5		incom	$⊢ (X \times X) \cap (R \times R) = (R \times R) \cap (X \times X)$
6	4 5	eqtr3i	$⊢ (X \cap R) \times (X \cap R) = (R \times R) \cap (X \times X)$
7	2 3 6	3eqtr4g	$⊢ dom D = X \times X \to dom ({D ↾}_{(R \times R)}) = (X \cap R) \times (X \cap R)$
8	7	reseq2d	$⊢ dom D = X \times X \to {D ↾}_{dom ({D ↾}_{(R \times R)})} = {D ↾}_{((X \cap R) \times (X \cap R))}$
9	1 8	eqtr3id	$⊢ dom D = X \times X \to {D ↾}_{(R \times R)} = {D ↾}_{((X \cap R) \times (X \cap R))}$

Metamath Proof Explorer