Metamath Proof Explorer


Theorem trinxp

Description: The relation induced by a transitive relation on a part of its field is transitive. (Taking the intersection of a relation with a Cartesian square is a way to restrict it to a subset of its field.) (Contributed by FL, 31-Jul-2009)

Ref Expression
Assertion trinxp RRRRA×ARA×ARA×A

Proof

Step Hyp Ref Expression
1 xpidtr A×AA×AA×A
2 trin2 RRRA×AA×AA×ARA×ARA×ARA×A
3 1 2 mpan2 RRRRA×ARA×ARA×A