Description: Value of the diagonal functor at a morphism. (Contributed by Mario Carneiro, 7-Jan-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | diag2.l | |
|
diag2.a | |
||
diag2.b | |
||
diag2.h | |
||
diag2.c | |
||
diag2.d | |
||
diag2.x | |
||
diag2.y | |
||
diag2.f | |
||
Assertion | diag2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | diag2.l | |
|
2 | diag2.a | |
|
3 | diag2.b | |
|
4 | diag2.h | |
|
5 | diag2.c | |
|
6 | diag2.d | |
|
7 | diag2.x | |
|
8 | diag2.y | |
|
9 | diag2.f | |
|
10 | 1 5 6 | diagval | |
11 | 10 | fveq2d | |
12 | 11 | oveqd | |
13 | 12 | fveq1d | |
14 | eqid | |
|
15 | eqid | |
|
16 | eqid | |
|
17 | 15 5 6 16 | 1stfcl | |
18 | eqid | |
|
19 | eqid | |
|
20 | 14 2 5 6 17 3 4 18 7 8 9 19 | curf2 | |
21 | 15 2 3 | xpcbas | |
22 | eqid | |
|
23 | 5 | adantr | |
24 | 6 | adantr | |
25 | opelxpi | |
|
26 | 7 25 | sylan | |
27 | opelxpi | |
|
28 | 8 27 | sylan | |
29 | 15 21 22 23 24 16 26 28 | 1stf2 | |
30 | 29 | oveqd | |
31 | df-ov | |
|
32 | 9 | adantr | |
33 | eqid | |
|
34 | simpr | |
|
35 | 3 33 18 24 34 | catidcl | |
36 | 32 35 | opelxpd | |
37 | 7 | adantr | |
38 | 8 | adantr | |
39 | 15 2 3 4 33 37 34 38 34 22 | xpchom2 | |
40 | 36 39 | eleqtrrd | |
41 | 40 | fvresd | |
42 | 31 41 | eqtrid | |
43 | op1stg | |
|
44 | 9 35 43 | syl2an2r | |
45 | 30 42 44 | 3eqtrd | |
46 | 45 | mpteq2dva | |
47 | fconstmpt | |
|
48 | 46 47 | eqtr4di | |
49 | 13 20 48 | 3eqtrd | |