Theorem 1stfval

Description: Value of the first projection functor. (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$$
Assertion	1stfval	$$⊢\phi \to P=⟨{1^{st}\upharpoonright }_B,\left(x\in B,y\in B⟼{1^{st}\upharpoonright }_{\left(xHy\right)}\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		fvex	$$⊢{\mathrm{Base}}_c\in \mathrm{V}$$
8		fvex	$$⊢{\mathrm{Base}}_d\in \mathrm{V}$$
9	7 8	xpex	$$⊢{\mathrm{Base}}_c\times {\mathrm{Base}}_d\in \mathrm{V}$$
10	9	a1i	$$⊢\left(c=C\wedge d=D\right)\to {\mathrm{Base}}_c\times {\mathrm{Base}}_d\in \mathrm{V}$$
11		simpl	$$⊢\left(c=C\wedge d=D\right)\to c=C$$
12	11	fveq2d	$$⊢\left(c=C\wedge d=D\right)\to {\mathrm{Base}}_c={\mathrm{Base}}_C$$
13		simpr	$$⊢\left(c=C\wedge d=D\right)\to d=D$$
14	13	fveq2d	$$⊢\left(c=C\wedge d=D\right)\to {\mathrm{Base}}_d={\mathrm{Base}}_D$$
15	12 14	xpeq12d	$$⊢\left(c=C\wedge d=D\right)\to {\mathrm{Base}}_c\times {\mathrm{Base}}_d={\mathrm{Base}}_C\times {\mathrm{Base}}_D$$
16		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
17		eqid	$$⊢{\mathrm{Base}}_D={\mathrm{Base}}_D$$
18	1 16 17	xpcbas	$$⊢{\mathrm{Base}}_C\times {\mathrm{Base}}_D={\mathrm{Base}}_T$$
19	18 2	eqtr4i	$$⊢{\mathrm{Base}}_C\times {\mathrm{Base}}_D=B$$
20	15 19	eqtrdi	$$⊢\left(c=C\wedge d=D\right)\to {\mathrm{Base}}_c\times {\mathrm{Base}}_d=B$$
21		simpr	$$⊢\left(\left(c=C\wedge d=D\right)\wedge b=B\right)\to b=B$$
22	21	reseq2d	$$⊢\left(\left(c=C\wedge d=D\right)\wedge b=B\right)\to {1^{st}\upharpoonright }_b={1^{st}\upharpoonright }_B$$
23		simpll	$$⊢\left(\left(c=C\wedge d=D\right)\wedge b=B\right)\to c=C$$
24		simplr	$$⊢\left(\left(c=C\wedge d=D\right)\wedge b=B\right)\to d=D$$
25	23 24	oveq12d	$$⊢\left(\left(c=C\wedge d=D\right)\wedge b=B\right)\to c{\times }_{c}d=C{\times }_{c}D$$
26	25 1	eqtr4di	$$⊢\left(\left(c=C\wedge d=D\right)\wedge b=B\right)\to c{\times }_{c}d=T$$
27	26	fveq2d	$$⊢\left(\left(c=C\wedge d=D\right)\wedge b=B\right)\to \mathrm{Hom}\left(c{\times }_{c}d\right)=\mathrm{Hom}\left(T\right)$$
28	27 3	eqtr4di	$$⊢\left(\left(c=C\wedge d=D\right)\wedge b=B\right)\to \mathrm{Hom}\left(c{\times }_{c}d\right)=H$$
29	28	oveqd	$$⊢\left(\left(c=C\wedge d=D\right)\wedge b=B\right)\to x\mathrm{Hom}\left(c{\times }_{c}d\right)y=xHy$$
30	29	reseq2d	$$⊢\left(\left(c=C\wedge d=D\right)\wedge b=B\right)\to {1^{st}\upharpoonright }_{\left(x\mathrm{Hom}\left(c{\times }_{c}d\right)y\right)}={1^{st}\upharpoonright }_{\left(xHy\right)}$$
31	21 21 30	mpoeq123dv	$$⊢\left(\left(c=C\wedge d=D\right)\wedge b=B\right)\to \left(x\in b,y\in b⟼{1^{st}\upharpoonright }_{\left(x\mathrm{Hom}\left(c{\times }_{c}d\right)y\right)}\right)=\left(x\in B,y\in B⟼{1^{st}\upharpoonright }_{\left(xHy\right)}\right)$$
32	22 31	opeq12d	$$⊢\left(\left(c=C\wedge d=D\right)\wedge b=B\right)\to ⟨{1^{st}\upharpoonright }_b,\left(x\in b,y\in b⟼{1^{st}\upharpoonright }_{\left(x\mathrm{Hom}\left(c{\times }_{c}d\right)y\right)}\right)⟩=⟨{1^{st}\upharpoonright }_B,\left(x\in B,y\in B⟼{1^{st}\upharpoonright }_{\left(xHy\right)}\right)⟩$$
33	10 20 32	csbied2	$$⊢\left(c=C\wedge d=D\right)\to ⦋\left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)/b⦌⟨{1^{st}\upharpoonright }_b,\left(x\in b,y\in b⟼{1^{st}\upharpoonright }_{\left(x\mathrm{Hom}\left(c{\times }_{c}d\right)y\right)}\right)⟩=⟨{1^{st}\upharpoonright }_B,\left(x\in B,y\in B⟼{1^{st}\upharpoonright }_{\left(xHy\right)}\right)⟩$$
34		df-1stf	$$⊢{1^{st}}_F=\left(c\in \mathrm{Cat},d\in \mathrm{Cat}⟼⦋\left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)/b⦌⟨{1^{st}\upharpoonright }_b,\left(x\in b,y\in b⟼{1^{st}\upharpoonright }_{\left(x\mathrm{Hom}\left(c{\times }_{c}d\right)y\right)}\right)⟩\right)$$
35		opex	$$⊢⟨{1^{st}\upharpoonright }_B,\left(x\in B,y\in B⟼{1^{st}\upharpoonright }_{\left(xHy\right)}\right)⟩\in \mathrm{V}$$
36	33 34 35	ovmpoa	$$⊢\left(C\in \mathrm{Cat}\wedge D\in \mathrm{Cat}\right)\to C{1^{st}}_{F}D=⟨{1^{st}\upharpoonright }_B,\left(x\in B,y\in B⟼{1^{st}\upharpoonright }_{\left(xHy\right)}\right)⟩$$
37	4 5 36	syl2anc	$$⊢\phi \to C{1^{st}}_{F}D=⟨{1^{st}\upharpoonright }_B,\left(x\in B,y\in B⟼{1^{st}\upharpoonright }_{\left(xHy\right)}\right)⟩$$
38	6 37	eqtrid	$$⊢\phi \to P=⟨{1^{st}\upharpoonright }_B,\left(x\in B,y\in B⟼{1^{st}\upharpoonright }_{\left(xHy\right)}\right)⟩$$