Theorem 2ndf1

Description: Value of the first projection on an object. (Contributed by Mario Carneiro, 11-Jan-2017)

	Ref	Expression
Hypotheses	1stfval.t	$$⊢T=C{\times }_{c}D$$
	1stfval.b	$$⊢B={\mathrm{Base}}_T$$
	1stfval.h	$$⊢H=\mathrm{Hom}\left(T\right)$$
	1stfval.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	1stfval.d	$$⊢\phi \to D\in \mathrm{Cat}$$
	2ndfval.p	$$⊢Q=C{2^{nd}}_{F}D$$
	2ndf1.p	$$⊢\phi \to R\in B$$
Assertion	2ndf1	$$⊢\phi \to 1^{st}\left(Q\right)\left(R\right)=2^{nd}\left(R\right)$$

Proof

Step	Hyp	Ref	Expression
1		1stfval.t	$$⊢T=C{\times }_{c}D$$
2		1stfval.b	$$⊢B={\mathrm{Base}}_T$$
3		1stfval.h	$$⊢H=\mathrm{Hom}\left(T\right)$$
4		1stfval.c	$$⊢\phi \to C\in \mathrm{Cat}$$
5		1stfval.d	$$⊢\phi \to D\in \mathrm{Cat}$$
6		2ndfval.p	$$⊢Q=C{2^{nd}}_{F}D$$
7		2ndf1.p	$$⊢\phi \to R\in B$$
8	1 2 3 4 5 6	2ndfval	$$⊢\phi \to Q=⟨{2^{nd}\upharpoonright }_B,\left(x\in B,y\in B⟼{2^{nd}\upharpoonright }_{\left(xHy\right)}\right)⟩$$
9		fo2nd	$$⊢2^{nd}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}$$
10		fofun	$$⊢2^{nd}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}\to \mathrm{Fun}{2}^{nd}$$
11	9 10	ax-mp	$$⊢\mathrm{Fun}{2}^{nd}$$
12	2	fvexi	$$⊢B\in \mathrm{V}$$
13		resfunexg	$$⊢\left(\mathrm{Fun}{2}^{nd}\wedge B\in \mathrm{V}\right)\to {2^{nd}\upharpoonright }_B\in \mathrm{V}$$
14	11 12 13	mp2an	$$⊢{2^{nd}\upharpoonright }_B\in \mathrm{V}$$
15	12 12	mpoex	$$⊢\left(x\in B,y\in B⟼{2^{nd}\upharpoonright }_{\left(xHy\right)}\right)\in \mathrm{V}$$
16	14 15	op1std	$$⊢Q=⟨{2^{nd}\upharpoonright }_B,\left(x\in B,y\in B⟼{2^{nd}\upharpoonright }_{\left(xHy\right)}\right)⟩\to 1^{st}\left(Q\right)={2^{nd}\upharpoonright }_B$$
17	8 16	syl	$$⊢\phi \to 1^{st}\left(Q\right)={2^{nd}\upharpoonright }_B$$
18	17	fveq1d	$$⊢\phi \to 1^{st}\left(Q\right)\left(R\right)=\left({2^{nd}\upharpoonright }_B\right)\left(R\right)$$
19	7	fvresd	$$⊢\phi \to \left({2^{nd}\upharpoonright }_B\right)\left(R\right)=2^{nd}\left(R\right)$$
20	18 19	eqtrd	$$⊢\phi \to 1^{st}\left(Q\right)\left(R\right)=2^{nd}\left(R\right)$$