Theorem cofu1

Description: Value of the object part of the functor composition. (Contributed by Mario Carneiro, 28-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)$$
	cofu2nd.x	$$⊢\phi \to X\in B$$
Assertion	cofu1	$$⊢\phi \to 1^{st}\left(G{\circ }_{\mathrm{func}}F\right)\left(X\right)=1^{st}\left(G\right)\left(1^{st}\left(F\right)\left(X\right)\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		cofu2nd.x	$$⊢\phi \to X\in B$$
5	1 2 3	cofu1st	$$⊢\phi \to 1^{st}\left(G{\circ }_{\mathrm{func}}F\right)=1^{st}\left(G\right)\circ 1^{st}\left(F\right)$$
6	5	fveq1d	$$⊢\phi \to 1^{st}\left(G{\circ }_{\mathrm{func}}F\right)\left(X\right)=\left(1^{st}\left(G\right)\circ 1^{st}\left(F\right)\right)\left(X\right)$$
7		eqid	$$⊢{\mathrm{Base}}_D={\mathrm{Base}}_D$$
8		relfunc	$$⊢\mathrm{Rel}\left(C\mathrm{Func}D\right)$$
9		1st2ndbr	$$⊢\left(\mathrm{Rel}\left(C\mathrm{Func}D\right)\wedge F\in \left(C\mathrm{Func}D\right)\right)\to 1^{st}\left(F\right)\left(C\mathrm{Func}D\right)2^{nd}\left(F\right)$$
10	8 2 9	sylancr	$$⊢\phi \to 1^{st}\left(F\right)\left(C\mathrm{Func}D\right)2^{nd}\left(F\right)$$
11	1 7 10	funcf1	$$⊢\phi \to 1^{st}\left(F\right):B⟶{\mathrm{Base}}_D$$
12		fvco3	$$⊢\left(1^{st}\left(F\right):B⟶{\mathrm{Base}}_D\wedge X\in B\right)\to \left(1^{st}\left(G\right)\circ 1^{st}\left(F\right)\right)\left(X\right)=1^{st}\left(G\right)\left(1^{st}\left(F\right)\left(X\right)\right)$$
13	11 4 12	syl2anc	$$⊢\phi \to \left(1^{st}\left(G\right)\circ 1^{st}\left(F\right)\right)\left(X\right)=1^{st}\left(G\right)\left(1^{st}\left(F\right)\left(X\right)\right)$$
14	6 13	eqtrd	$$⊢\phi \to 1^{st}\left(G{\circ }_{\mathrm{func}}F\right)\left(X\right)=1^{st}\left(G\right)\left(1^{st}\left(F\right)\left(X\right)\right)$$