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 
|- ( ( ( R e. DirRel /\ C e. V ) /\ ( A R B /\ B R C ) ) -> A R C )

Proof

Step Hyp Ref Expression
1 reldir 
 |-  ( R e. DirRel -> Rel R )
2 brrelex1 
 |-  ( ( Rel R /\ A R B ) -> A e. _V )
3 2 ex 
 |-  ( Rel R -> ( A R B -> A e. _V ) )
4 brrelex1 
 |-  ( ( Rel R /\ B R C ) -> B e. _V )
5 4 ex 
 |-  ( Rel R -> ( B R C -> B e. _V ) )
6 3 5 anim12d 
 |-  ( Rel R -> ( ( A R B /\ B R C ) -> ( A e. _V /\ B e. _V ) ) )
7 1 6 syl 
 |-  ( R e. DirRel -> ( ( A R B /\ B R C ) -> ( A e. _V /\ B e. _V ) ) )
8 eqid 
 |-  U. U. R = U. U. R
9 8 isdir 
 |-  ( R e. DirRel -> ( R e. DirRel <-> ( ( Rel R /\ ( _I |` U. U. R ) C_ R ) /\ ( ( R o. R ) C_ R /\ ( U. U. R X. U. U. R ) C_ ( `' R o. R ) ) ) ) )
10 9 ibi 
 |-  ( R e. DirRel -> ( ( Rel R /\ ( _I |` U. U. R ) C_ R ) /\ ( ( R o. R ) C_ R /\ ( U. U. R X. U. U. R ) C_ ( `' R o. R ) ) ) )
11 10 simprld 
 |-  ( R e. DirRel -> ( R o. R ) C_ R )
12 cotr 
 |-  ( ( R o. R ) C_ R <-> A. x A. y A. z ( ( x R y /\ y R z ) -> x R z ) )
13 11 12 sylib 
 |-  ( R e. DirRel -> A. x A. y A. z ( ( x R y /\ y R z ) -> x R z ) )
14 breq12 
 |-  ( ( x = A /\ y = B ) -> ( x R y <-> A R B ) )
15 14 3adant3 
 |-  ( ( x = A /\ y = B /\ z = C ) -> ( x R y <-> A R B ) )
16 breq12 
 |-  ( ( y = B /\ z = C ) -> ( y R z <-> B R C ) )
17 16 3adant1 
 |-  ( ( x = A /\ y = B /\ z = C ) -> ( y R z <-> B R C ) )
18 15 17 anbi12d 
 |-  ( ( x = A /\ y = B /\ z = C ) -> ( ( x R y /\ y R z ) <-> ( A R B /\ B R C ) ) )
19 breq12 
 |-  ( ( x = A /\ z = C ) -> ( x R z <-> A R C ) )
20 19 3adant2 
 |-  ( ( x = A /\ y = B /\ z = C ) -> ( x R z <-> A R C ) )
21 18 20 imbi12d 
 |-  ( ( x = A /\ y = B /\ z = C ) -> ( ( ( x R y /\ y R z ) -> x R z ) <-> ( ( A R B /\ B R C ) -> A R C ) ) )
22 21 spc3gv 
 |-  ( ( A e. _V /\ B e. _V /\ C e. V ) -> ( A. x A. y A. z ( ( x R y /\ y R z ) -> x R z ) -> ( ( A R B /\ B R C ) -> A R C ) ) )
23 13 22 syl5 
 |-  ( ( A e. _V /\ B e. _V /\ C e. V ) -> ( R e. DirRel -> ( ( A R B /\ B R C ) -> A R C ) ) )
24 23 3expia 
 |-  ( ( A e. _V /\ B e. _V ) -> ( C e. V -> ( R e. DirRel -> ( ( A R B /\ B R C ) -> A R C ) ) ) )
25 24 com4t 
 |-  ( R e. DirRel -> ( ( A R B /\ B R C ) -> ( ( A e. _V /\ B e. _V ) -> ( C e. V -> A R C ) ) ) )
26 7 25 mpdd 
 |-  ( R e. DirRel -> ( ( A R B /\ B R C ) -> ( C e. V -> A R C ) ) )
27 26 imp31 
 |-  ( ( ( R e. DirRel /\ ( A R B /\ B R C ) ) /\ C e. V ) -> A R C )
28 27 an32s 
 |-  ( ( ( R e. DirRel /\ C e. V ) /\ ( A R B /\ B R C ) ) -> A R C )