Description: Value of the constant functor at an object. (Contributed by Mario Carneiro, 7-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 | |
||
Assertion | diag11 | |
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 | 1 2 3 | diagval | |
10 | 9 | fveq2d | |
11 | 10 | fveq1d | |
12 | 6 11 | eqtrid | |
13 | 12 | fveq2d | |
14 | 13 | fveq1d | |
15 | eqid | |
|
16 | eqid | |
|
17 | eqid | |
|
18 | 16 2 3 17 | 1stfcl | |
19 | eqid | |
|
20 | 15 4 2 3 18 7 5 19 8 | curf11 | |
21 | df-ov | |
|
22 | 16 4 7 | xpcbas | |
23 | eqid | |
|
24 | 5 8 | opelxpd | |
25 | 16 22 23 2 3 17 24 | 1stf1 | |
26 | 21 25 | eqtrid | |
27 | op1stg | |
|
28 | 5 8 27 | syl2anc | |
29 | 26 28 | eqtrd | |
30 | 14 20 29 | 3eqtrd | |