Theorem curf1fval

Description: Value of the object part of the 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$$
	curfval.j	$$⊢J=\mathrm{Hom}\left(D\right)$$
	curfval.1	$$⊢\underset{\dot{}}{1}=\mathrm{Id}\left(C\right)$$
Assertion	curf1fval	$$⊢\phi \to 1^{st}\left(G\right)=\left(x\in A⟼⟨\left(y\in B⟼x{1}^{st}\left(F\right)y\right),\left(y\in B,z\in B⟼\left(g\in \left(yJz\right)⟼\underset{\dot{}}{1}\left(x\right)\left(⟨x,y⟩2^{nd}\left(F\right)⟨x,z⟩\right)g\right)\right)⟩\right)$$

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		curfval.j	$$⊢J=\mathrm{Hom}\left(D\right)$$
8		curfval.1	$$⊢\underset{\dot{}}{1}=\mathrm{Id}\left(C\right)$$
9		eqid	$$⊢\mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(C\right)$$
10		eqid	$$⊢\mathrm{Id}\left(D\right)=\mathrm{Id}\left(D\right)$$
11	1 2 3 4 5 6 7 8 9 10	curfval	$$⊢\phi \to G=⟨\left(x\in A⟼⟨\left(y\in B⟼x{1}^{st}\left(F\right)y\right),\left(y\in B,z\in B⟼\left(g\in \left(yJz\right)⟼\underset{\dot{}}{1}\left(x\right)\left(⟨x,y⟩2^{nd}\left(F\right)⟨x,z⟩\right)g\right)\right)⟩\right),\left(x\in A,y\in A⟼\left(g\in \left(x\mathrm{Hom}\left(C\right)y\right)⟼\left(z\in B⟼g\left(⟨x,z⟩2^{nd}\left(F\right)⟨y,z⟩\right)\mathrm{Id}\left(D\right)\left(z\right)\right)\right)\right)⟩$$
12	2	fvexi	$$⊢A\in \mathrm{V}$$
13	12	mptex	$$⊢\left(x\in A⟼⟨\left(y\in B⟼x{1}^{st}\left(F\right)y\right),\left(y\in B,z\in B⟼\left(g\in \left(yJz\right)⟼\underset{\dot{}}{1}\left(x\right)\left(⟨x,y⟩2^{nd}\left(F\right)⟨x,z⟩\right)g\right)\right)⟩\right)\in \mathrm{V}$$
14	12 12	mpoex	$$⊢\left(x\in A,y\in A⟼\left(g\in \left(x\mathrm{Hom}\left(C\right)y\right)⟼\left(z\in B⟼g\left(⟨x,z⟩2^{nd}\left(F\right)⟨y,z⟩\right)\mathrm{Id}\left(D\right)\left(z\right)\right)\right)\right)\in \mathrm{V}$$
15	13 14	op1std	$$⊢G=⟨\left(x\in A⟼⟨\left(y\in B⟼x{1}^{st}\left(F\right)y\right),\left(y\in B,z\in B⟼\left(g\in \left(yJz\right)⟼\underset{\dot{}}{1}\left(x\right)\left(⟨x,y⟩2^{nd}\left(F\right)⟨x,z⟩\right)g\right)\right)⟩\right),\left(x\in A,y\in A⟼\left(g\in \left(x\mathrm{Hom}\left(C\right)y\right)⟼\left(z\in B⟼g\left(⟨x,z⟩2^{nd}\left(F\right)⟨y,z⟩\right)\mathrm{Id}\left(D\right)\left(z\right)\right)\right)\right)⟩\to 1^{st}\left(G\right)=\left(x\in A⟼⟨\left(y\in B⟼x{1}^{st}\left(F\right)y\right),\left(y\in B,z\in B⟼\left(g\in \left(yJz\right)⟼\underset{\dot{}}{1}\left(x\right)\left(⟨x,y⟩2^{nd}\left(F\right)⟨x,z⟩\right)g\right)\right)⟩\right)$$
16	11 15	syl	$$⊢\phi \to 1^{st}\left(G\right)=\left(x\in A⟼⟨\left(y\in B⟼x{1}^{st}\left(F\right)y\right),\left(y\in B,z\in B⟼\left(g\in \left(yJz\right)⟼\underset{\dot{}}{1}\left(x\right)\left(⟨x,y⟩2^{nd}\left(F\right)⟨x,z⟩\right)g\right)\right)⟩\right)$$