Metamath Proof Explorer


Theorem metreslem

Description: Lemma for metres . (Contributed by Mario Carneiro, 24-Aug-2015)

Ref Expression
Assertion metreslem dom D = X × X D R × R = D X R × X R

Proof

Step Hyp Ref Expression
1 resdmres D dom D R × R = D R × R
2 ineq2 dom D = X × X R × R dom D = R × R X × X
3 dmres dom D R × R = R × R dom D
4 inxp X × X R × R = X R × X R
5 incom X × X R × R = R × R X × X
6 4 5 eqtr3i X R × X R = R × R X × X
7 2 3 6 3eqtr4g dom D = X × X dom D R × R = X R × X R
8 7 reseq2d dom D = X × X D dom D R × R = D X R × X R
9 1 8 eqtr3id dom D = X × X D R × R = D X R × X R