Theorem curf11

Description: Value of the double evaluated curry functor. (Contributed by Mario Carneiro, 12-Jan-2017)

	Ref	Expression
Hypotheses	curfval.g	$$⊢G=⟨C,D⟩{curry}_{F}F$$
	curfval.a	$$⊢A={\mathrm{Base}}_C$$
	curfval.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	curfval.d	$$⊢\phi \to D\in \mathrm{Cat}$$
	curfval.f	$$⊢\phi \to F\in \left(\left(C{\times }_{c}D\right)\mathrm{Func}E\right)$$
	curfval.b	$$⊢B={\mathrm{Base}}_D$$
	curf1.x	$$⊢\phi \to X\in A$$
	curf1.k	$$⊢K=1^{st}\left(G\right)\left(X\right)$$
	curf11.y	$$⊢\phi \to Y\in B$$
Assertion	curf11	$$⊢\phi \to 1^{st}\left(K\right)\left(Y\right)=X{1}^{st}\left(F\right)Y$$

Proof

Step	Hyp	Ref	Expression
1		curfval.g	$$⊢G=⟨C,D⟩{curry}_{F}F$$
2		curfval.a	$$⊢A={\mathrm{Base}}_C$$
3		curfval.c	$$⊢\phi \to C\in \mathrm{Cat}$$
4		curfval.d	$$⊢\phi \to D\in \mathrm{Cat}$$
5		curfval.f	$$⊢\phi \to F\in \left(\left(C{\times }_{c}D\right)\mathrm{Func}E\right)$$
6		curfval.b	$$⊢B={\mathrm{Base}}_D$$
7		curf1.x	$$⊢\phi \to X\in A$$
8		curf1.k	$$⊢K=1^{st}\left(G\right)\left(X\right)$$
9		curf11.y	$$⊢\phi \to Y\in B$$
10		eqid	$$⊢\mathrm{Hom}\left(D\right)=\mathrm{Hom}\left(D\right)$$
11		eqid	$$⊢\mathrm{Id}\left(C\right)=\mathrm{Id}\left(C\right)$$
12	1 2 3 4 5 6 7 8 10 11	curf1	$$⊢\phi \to K=⟨\left(y\in B⟼X{1}^{st}\left(F\right)y\right),\left(y\in B,z\in B⟼\left(g\in \left(y\mathrm{Hom}\left(D\right)z\right)⟼\mathrm{Id}\left(C\right)\left(X\right)\left(⟨X,y⟩2^{nd}\left(F\right)⟨X,z⟩\right)g\right)\right)⟩$$
13	6	fvexi	$$⊢B\in \mathrm{V}$$
14	13	mptex	$$⊢\left(y\in B⟼X{1}^{st}\left(F\right)y\right)\in \mathrm{V}$$
15	13 13	mpoex	$$⊢\left(y\in B,z\in B⟼\left(g\in \left(y\mathrm{Hom}\left(D\right)z\right)⟼\mathrm{Id}\left(C\right)\left(X\right)\left(⟨X,y⟩2^{nd}\left(F\right)⟨X,z⟩\right)g\right)\right)\in \mathrm{V}$$
16	14 15	op1std	$$⊢K=⟨\left(y\in B⟼X{1}^{st}\left(F\right)y\right),\left(y\in B,z\in B⟼\left(g\in \left(y\mathrm{Hom}\left(D\right)z\right)⟼\mathrm{Id}\left(C\right)\left(X\right)\left(⟨X,y⟩2^{nd}\left(F\right)⟨X,z⟩\right)g\right)\right)⟩\to 1^{st}\left(K\right)=\left(y\in B⟼X{1}^{st}\left(F\right)y\right)$$
17	12 16	syl	$$⊢\phi \to 1^{st}\left(K\right)=\left(y\in B⟼X{1}^{st}\left(F\right)y\right)$$
18		simpr	$$⊢\left(\phi \wedge y=Y\right)\to y=Y$$
19	18	oveq2d	$$⊢\left(\phi \wedge y=Y\right)\to X{1}^{st}\left(F\right)y=X{1}^{st}\left(F\right)Y$$
20		ovexd	$$⊢\phi \to X{1}^{st}\left(F\right)Y\in \mathrm{V}$$
21	17 19 9 20	fvmptd	$$⊢\phi \to 1^{st}\left(K\right)\left(Y\right)=X{1}^{st}\left(F\right)Y$$