Theorem 1stf1

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}$$
	1stfval.p	$$⊢P=C{1^{st}}_{F}D$$
	1stf1.p	$$⊢\phi \to R\in B$$
Assertion	1stf1	$$⊢\phi \to 1^{st}\left(P\right)\left(R\right)=1^{st}\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		1stfval.p	$$⊢P=C{1^{st}}_{F}D$$
7		1stf1.p	$$⊢\phi \to R\in B$$
8	1 2 3 4 5 6	1stfval	$$⊢\phi \to P=⟨{1^{st}\upharpoonright }_B,\left(x\in B,y\in B⟼{1^{st}\upharpoonright }_{\left(xHy\right)}\right)⟩$$
9		fo1st	$$⊢1^{st}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}$$
10		fofun	$$⊢1^{st}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}\to \mathrm{Fun}{1}^{st}$$
11	9 10	ax-mp	$$⊢\mathrm{Fun}{1}^{st}$$
12	2	fvexi	$$⊢B\in \mathrm{V}$$
13		resfunexg	$$⊢\left(\mathrm{Fun}{1}^{st}\wedge B\in \mathrm{V}\right)\to {1^{st}\upharpoonright }_B\in \mathrm{V}$$
14	11 12 13	mp2an	$$⊢{1^{st}\upharpoonright }_B\in \mathrm{V}$$
15	12 12	mpoex	$$⊢\left(x\in B,y\in B⟼{1^{st}\upharpoonright }_{\left(xHy\right)}\right)\in \mathrm{V}$$
16	14 15	op1std	$$⊢P=⟨{1^{st}\upharpoonright }_B,\left(x\in B,y\in B⟼{1^{st}\upharpoonright }_{\left(xHy\right)}\right)⟩\to 1^{st}\left(P\right)={1^{st}\upharpoonright }_B$$
17	8 16	syl	$$⊢\phi \to 1^{st}\left(P\right)={1^{st}\upharpoonright }_B$$
18	17	fveq1d	$$⊢\phi \to 1^{st}\left(P\right)\left(R\right)=\left({1^{st}\upharpoonright }_B\right)\left(R\right)$$
19	7	fvresd	$$⊢\phi \to \left({1^{st}\upharpoonright }_B\right)\left(R\right)=1^{st}\left(R\right)$$
20	18 19	eqtrd	$$⊢\phi \to 1^{st}\left(P\right)\left(R\right)=1^{st}\left(R\right)$$