Metamath Proof Explorer


Theorem dirtr

Description: A direction is transitive. (Contributed by Jeff Hankins, 25-Nov-2009) (Revised by Mario Carneiro, 22-Nov-2013)

Ref Expression
Assertion dirtr RDirRelCVARBBRCARC

Proof

Step Hyp Ref Expression
1 reldir RDirRelRelR
2 brrelex1 RelRARBAV
3 2 ex RelRARBAV
4 brrelex1 RelRBRCBV
5 4 ex RelRBRCBV
6 3 5 anim12d RelRARBBRCAVBV
7 1 6 syl RDirRelARBBRCAVBV
8 eqid R=R
9 8 isdir RDirRelRDirRelRelRIRRRRRR×RR-1R
10 9 ibi RDirRelRelRIRRRRRR×RR-1R
11 10 simprld RDirRelRRR
12 cotr RRRxyzxRyyRzxRz
13 11 12 sylib RDirRelxyzxRyyRzxRz
14 breq12 x=Ay=BxRyARB
15 14 3adant3 x=Ay=Bz=CxRyARB
16 breq12 y=Bz=CyRzBRC
17 16 3adant1 x=Ay=Bz=CyRzBRC
18 15 17 anbi12d x=Ay=Bz=CxRyyRzARBBRC
19 breq12 x=Az=CxRzARC
20 19 3adant2 x=Ay=Bz=CxRzARC
21 18 20 imbi12d x=Ay=Bz=CxRyyRzxRzARBBRCARC
22 21 spc3gv AVBVCVxyzxRyyRzxRzARBBRCARC
23 13 22 syl5 AVBVCVRDirRelARBBRCARC
24 23 3expia AVBVCVRDirRelARBBRCARC
25 24 com4t RDirRelARBBRCAVBVCVARC
26 7 25 mpdd RDirRelARBBRCCVARC
27 26 imp31 RDirRelARBBRCCVARC
28 27 an32s RDirRelCVARBBRCARC