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{\Delta }_{\mathrm{func}}D$$
	diagval.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	diagval.d	$$⊢\phi \to D\in \mathrm{Cat}$$
	diag11.a	$$⊢A={\mathrm{Base}}_C$$
	diag11.c	$$⊢\phi \to X\in A$$
	diag11.k	$$⊢K=1^{st}\left(L\right)\left(X\right)$$
	diag11.b	$$⊢B={\mathrm{Base}}_D$$
	diag11.y	$$⊢\phi \to Y\in B$$
Assertion	diag11	$$⊢\phi \to 1^{st}\left(K\right)\left(Y\right)=X$$

Proof

Step	Hyp	Ref	Expression
1		diagval.l	$$⊢L=C{\Delta }_{\mathrm{func}}D$$
2		diagval.c	$$⊢\phi \to C\in \mathrm{Cat}$$
3		diagval.d	$$⊢\phi \to D\in \mathrm{Cat}$$
4		diag11.a	$$⊢A={\mathrm{Base}}_C$$
5		diag11.c	$$⊢\phi \to X\in A$$
6		diag11.k	$$⊢K=1^{st}\left(L\right)\left(X\right)$$
7		diag11.b	$$⊢B={\mathrm{Base}}_D$$
8		diag11.y	$$⊢\phi \to Y\in B$$
9	1 2 3	diagval	$$⊢\phi \to L=⟨C,D⟩{curry}_F\left(C{1^{st}}_{F}D\right)$$
10	9	fveq2d	$$⊢\phi \to 1^{st}\left(L\right)=1^{st}\left(⟨C,D⟩{curry}_F\left(C{1^{st}}_{F}D\right)\right)$$
11	10	fveq1d	$$⊢\phi \to 1^{st}\left(L\right)\left(X\right)=1^{st}\left(⟨C,D⟩{curry}_F\left(C{1^{st}}_{F}D\right)\right)\left(X\right)$$
12	6 11	syl5eq	$$⊢\phi \to K=1^{st}\left(⟨C,D⟩{curry}_F\left(C{1^{st}}_{F}D\right)\right)\left(X\right)$$
13	12	fveq2d	$$⊢\phi \to 1^{st}\left(K\right)=1^{st}\left(1^{st}\left(⟨C,D⟩{curry}_F\left(C{1^{st}}_{F}D\right)\right)\left(X\right)\right)$$
14	13	fveq1d	$$⊢\phi \to 1^{st}\left(K\right)\left(Y\right)=1^{st}\left(1^{st}\left(⟨C,D⟩{curry}_F\left(C{1^{st}}_{F}D\right)\right)\left(X\right)\right)\left(Y\right)$$
15		eqid	$$⊢⟨C,D⟩{curry}_F\left(C{1^{st}}_{F}D\right)=⟨C,D⟩{curry}_F\left(C{1^{st}}_{F}D\right)$$
16		eqid	$$⊢C{\times }_{c}D=C{\times }_{c}D$$
17		eqid	$$⊢C{1^{st}}_{F}D=C{1^{st}}_{F}D$$
18	16 2 3 17	1stfcl	$$⊢\phi \to C{1^{st}}_{F}D\in \left(\left(C{\times }_{c}D\right)\mathrm{Func}C\right)$$
19		eqid	$$⊢1^{st}\left(⟨C,D⟩{curry}_F\left(C{1^{st}}_{F}D\right)\right)\left(X\right)=1^{st}\left(⟨C,D⟩{curry}_F\left(C{1^{st}}_{F}D\right)\right)\left(X\right)$$
20	15 4 2 3 18 7 5 19 8	curf11	$$⊢\phi \to 1^{st}\left(1^{st}\left(⟨C,D⟩{curry}_F\left(C{1^{st}}_{F}D\right)\right)\left(X\right)\right)\left(Y\right)=X{1}^{st}\left(C{1^{st}}_{F}D\right)Y$$
21		df-ov	$$⊢X{1}^{st}\left(C{1^{st}}_{F}D\right)Y=1^{st}\left(C{1^{st}}_{F}D\right)\left(⟨X,Y⟩\right)$$
22	16 4 7	xpcbas	$$⊢A\times B={\mathrm{Base}}_{\left(C{\times }_{c}D\right)}$$
23		eqid	$$⊢\mathrm{Hom}\left(C{\times }_{c}D\right)=\mathrm{Hom}\left(C{\times }_{c}D\right)$$
24	5 8	opelxpd	$$⊢\phi \to ⟨X,Y⟩\in \left(A\times B\right)$$
25	16 22 23 2 3 17 24	1stf1	$$⊢\phi \to 1^{st}\left(C{1^{st}}_{F}D\right)\left(⟨X,Y⟩\right)=1^{st}\left(⟨X,Y⟩\right)$$
26	21 25	syl5eq	$$⊢\phi \to X{1}^{st}\left(C{1^{st}}_{F}D\right)Y=1^{st}\left(⟨X,Y⟩\right)$$
27		op1stg	$$⊢\left(X\in A\wedge Y\in B\right)\to 1^{st}\left(⟨X,Y⟩\right)=X$$
28	5 8 27	syl2anc	$$⊢\phi \to 1^{st}\left(⟨X,Y⟩\right)=X$$
29	26 28	eqtrd	$$⊢\phi \to X{1}^{st}\left(C{1^{st}}_{F}D\right)Y=X$$
30	14 20 29	3eqtrd	$$⊢\phi \to 1^{st}\left(K\right)\left(Y\right)=X$$