Description: Functor composition is associative. (Contributed by Mario Carneiro, 3-Jan-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cofuass.g | |
|
cofuass.h | |
||
cofuass.k | |
||
Assertion | cofuass | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cofuass.g | |
|
2 | cofuass.h | |
|
3 | cofuass.k | |
|
4 | coass | |
|
5 | eqid | |
|
6 | 5 2 3 | cofu1st | |
7 | 6 | coeq1d | |
8 | eqid | |
|
9 | 8 1 2 | cofu1st | |
10 | 9 | coeq2d | |
11 | 4 7 10 | 3eqtr4a | |
12 | coass | |
|
13 | 2 | 3ad2ant1 | |
14 | 3 | 3ad2ant1 | |
15 | relfunc | |
|
16 | 1st2ndbr | |
|
17 | 15 1 16 | sylancr | |
18 | 17 | 3ad2ant1 | |
19 | 8 5 18 | funcf1 | |
20 | simp2 | |
|
21 | 19 20 | ffvelrnd | |
22 | simp3 | |
|
23 | 19 22 | ffvelrnd | |
24 | 5 13 14 21 23 | cofu2nd | |
25 | 24 | coeq1d | |
26 | 1 | 3ad2ant1 | |
27 | 8 26 13 20 | cofu1 | |
28 | 8 26 13 22 | cofu1 | |
29 | 27 28 | oveq12d | |
30 | 8 26 13 20 22 | cofu2nd | |
31 | 29 30 | coeq12d | |
32 | 12 25 31 | 3eqtr4a | |
33 | 32 | mpoeq3dva | |
34 | 11 33 | opeq12d | |
35 | 2 3 | cofucl | |
36 | 8 1 35 | cofuval | |
37 | 1 2 | cofucl | |
38 | 8 37 3 | cofuval | |
39 | 34 36 38 | 3eqtr4d | |