Metamath Proof Explorer


Theorem diag11

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 L=CΔfuncD
diagval.c φCCat
diagval.d φDCat
diag11.a A=BaseC
diag11.c φXA
diag11.k K=1stLX
diag11.b B=BaseD
diag11.y φYB
Assertion diag11 φ1stKY=X

Proof

Step Hyp Ref Expression
1 diagval.l L=CΔfuncD
2 diagval.c φCCat
3 diagval.d φDCat
4 diag11.a A=BaseC
5 diag11.c φXA
6 diag11.k K=1stLX
7 diag11.b B=BaseD
8 diag11.y φYB
9 1 2 3 diagval φL=CDcurryFC1stFD
10 9 fveq2d φ1stL=1stCDcurryFC1stFD
11 10 fveq1d φ1stLX=1stCDcurryFC1stFDX
12 6 11 eqtrid φK=1stCDcurryFC1stFDX
13 12 fveq2d φ1stK=1st1stCDcurryFC1stFDX
14 13 fveq1d φ1stKY=1st1stCDcurryFC1stFDXY
15 eqid CDcurryFC1stFD=CDcurryFC1stFD
16 eqid C×cD=C×cD
17 eqid C1stFD=C1stFD
18 16 2 3 17 1stfcl φC1stFDC×cDFuncC
19 eqid 1stCDcurryFC1stFDX=1stCDcurryFC1stFDX
20 15 4 2 3 18 7 5 19 8 curf11 φ1st1stCDcurryFC1stFDXY=X1stC1stFDY
21 df-ov X1stC1stFDY=1stC1stFDXY
22 16 4 7 xpcbas A×B=BaseC×cD
23 eqid HomC×cD=HomC×cD
24 5 8 opelxpd φXYA×B
25 16 22 23 2 3 17 24 1stf1 φ1stC1stFDXY=1stXY
26 21 25 eqtrid φX1stC1stFDY=1stXY
27 op1stg XAYB1stXY=X
28 5 8 27 syl2anc φ1stXY=X
29 26 28 eqtrd φX1stC1stFDY=X
30 14 20 29 3eqtrd φ1stKY=X