Description: Value of the constant functor at a morphism. (Contributed by Mario Carneiro, 6-Jan-2017) (Revised by Mario Carneiro, 15-Jan-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | diagval.l | |
|
diagval.c | |
||
diagval.d | |
||
diag11.a | |
||
diag11.c | |
||
diag11.k | |
||
diag11.b | |
||
diag11.y | |
||
diag12.j | |
||
diag12.i | |
||
diag12.z | |
||
diag12.f | |
||
Assertion | diag12 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | diagval.l | |
|
2 | diagval.c | |
|
3 | diagval.d | |
|
4 | diag11.a | |
|
5 | diag11.c | |
|
6 | diag11.k | |
|
7 | diag11.b | |
|
8 | diag11.y | |
|
9 | diag12.j | |
|
10 | diag12.i | |
|
11 | diag12.z | |
|
12 | diag12.f | |
|
13 | 1 2 3 | diagval | |
14 | 13 | fveq2d | |
15 | 14 | fveq1d | |
16 | 6 15 | eqtrid | |
17 | 16 | fveq2d | |
18 | 17 | oveqd | |
19 | 18 | fveq1d | |
20 | eqid | |
|
21 | eqid | |
|
22 | eqid | |
|
23 | 21 2 3 22 | 1stfcl | |
24 | eqid | |
|
25 | 20 4 2 3 23 7 5 24 8 9 10 11 12 | curf12 | |
26 | df-ov | |
|
27 | 21 4 7 | xpcbas | |
28 | eqid | |
|
29 | 5 8 | opelxpd | |
30 | 5 11 | opelxpd | |
31 | 21 27 28 2 3 22 29 30 | 1stf2 | |
32 | 31 | fveq1d | |
33 | 26 32 | eqtrid | |
34 | eqid | |
|
35 | 4 34 10 2 5 | catidcl | |
36 | 35 12 | opelxpd | |
37 | 21 4 7 34 9 5 8 5 11 28 | xpchom2 | |
38 | 36 37 | eleqtrrd | |
39 | 38 | fvresd | |
40 | op1stg | |
|
41 | 35 12 40 | syl2anc | |
42 | 33 39 41 | 3eqtrd | |
43 | 19 25 42 | 3eqtrd | |