Theorem cofu1st

Description: Value of the object part of the functor composition. (Contributed by Mario Carneiro, 3-Jan-2017)

	Ref	Expression
Hypotheses	cofuval.b	$$⊢B={\mathrm{Base}}_C$$
	cofuval.f	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
	cofuval.g	$$⊢\phi \to G\in \left(D\mathrm{Func}E\right)$$
Assertion	cofu1st	$$⊢\phi \to 1^{st}\left(G{\circ }_{\mathrm{func}}F\right)=1^{st}\left(G\right)\circ 1^{st}\left(F\right)$$

Proof

Step	Hyp	Ref	Expression
1		cofuval.b	$$⊢B={\mathrm{Base}}_C$$
2		cofuval.f	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
3		cofuval.g	$$⊢\phi \to G\in \left(D\mathrm{Func}E\right)$$
4	1 2 3	cofuval	$$⊢\phi \to G{\circ }_{\mathrm{func}}F=⟨1^{st}\left(G\right)\circ 1^{st}\left(F\right),\left(x\in B,y\in B⟼\left(1^{st}\left(F\right)\left(x\right)2^{nd}\left(G\right)1^{st}\left(F\right)\left(y\right)\right)\circ \left(x{2}^{nd}\left(F\right)y\right)\right)⟩$$
5	4	fveq2d	$$⊢\phi \to 1^{st}\left(G{\circ }_{\mathrm{func}}F\right)=1^{st}\left(⟨1^{st}\left(G\right)\circ 1^{st}\left(F\right),\left(x\in B,y\in B⟼\left(1^{st}\left(F\right)\left(x\right)2^{nd}\left(G\right)1^{st}\left(F\right)\left(y\right)\right)\circ \left(x{2}^{nd}\left(F\right)y\right)\right)⟩\right)$$
6		fvex	$$⊢1^{st}\left(G\right)\in \mathrm{V}$$
7		fvex	$$⊢1^{st}\left(F\right)\in \mathrm{V}$$
8	6 7	coex	$$⊢1^{st}\left(G\right)\circ 1^{st}\left(F\right)\in \mathrm{V}$$
9	1	fvexi	$$⊢B\in \mathrm{V}$$
10	9 9	mpoex	$$⊢\left(x\in B,y\in B⟼\left(1^{st}\left(F\right)\left(x\right)2^{nd}\left(G\right)1^{st}\left(F\right)\left(y\right)\right)\circ \left(x{2}^{nd}\left(F\right)y\right)\right)\in \mathrm{V}$$
11	8 10	op1st	$$⊢1^{st}\left(⟨1^{st}\left(G\right)\circ 1^{st}\left(F\right),\left(x\in B,y\in B⟼\left(1^{st}\left(F\right)\left(x\right)2^{nd}\left(G\right)1^{st}\left(F\right)\left(y\right)\right)\circ \left(x{2}^{nd}\left(F\right)y\right)\right)⟩\right)=1^{st}\left(G\right)\circ 1^{st}\left(F\right)$$
12	5 11	eqtrdi	$$⊢\phi \to 1^{st}\left(G{\circ }_{\mathrm{func}}F\right)=1^{st}\left(G\right)\circ 1^{st}\left(F\right)$$