Description: A direction is transitive. (Contributed by Jeff Hankins, 25-Nov-2009) (Revised by Mario Carneiro, 22-Nov-2013)
Ref | Expression | ||
---|---|---|---|
Assertion | dirtr | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | reldir | |
|
2 | brrelex1 | |
|
3 | 2 | ex | |
4 | brrelex1 | |
|
5 | 4 | ex | |
6 | 3 5 | anim12d | |
7 | 1 6 | syl | |
8 | eqid | |
|
9 | 8 | isdir | |
10 | 9 | ibi | |
11 | 10 | simprld | |
12 | cotr | |
|
13 | 11 12 | sylib | |
14 | breq12 | |
|
15 | 14 | 3adant3 | |
16 | breq12 | |
|
17 | 16 | 3adant1 | |
18 | 15 17 | anbi12d | |
19 | breq12 | |
|
20 | 19 | 3adant2 | |
21 | 18 20 | imbi12d | |
22 | 21 | spc3gv | |
23 | 13 22 | syl5 | |
24 | 23 | 3expia | |
25 | 24 | com4t | |
26 | 7 25 | mpdd | |
27 | 26 | imp31 | |
28 | 27 | an32s | |