Definition df-1stf

Description: Define the first projection functor out of the product of categories. (Contributed by Mario Carneiro, 11-Jan-2017)

	Ref	Expression
Assertion	df-1stf	$$⊢{1^{st}}_F=\left(r\in \mathrm{Cat},s\in \mathrm{Cat}⟼⦋\left({\mathrm{Base}}_r\times {\mathrm{Base}}_s\right)/b⦌⟨{1^{st}\upharpoonright }_b,\left(x\in b,y\in b⟼{1^{st}\upharpoonright }_{\left(x\mathrm{Hom}\left(r{\times }_{c}s\right)y\right)}\right)⟩\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		c1stf	$$class{1^{st}}_F$$
1		vr	$$setvarr$$
2		ccat	$$class\mathrm{Cat}$$
3		vs	$$setvars$$
4		cbs	$$class\mathrm{Base}$$
5	1	cv	$$setvarr$$
6	5 4	cfv	$$class{\mathrm{Base}}_r$$
7	3	cv	$$setvars$$
8	7 4	cfv	$$class{\mathrm{Base}}_s$$
9	6 8	cxp	$$class\left({\mathrm{Base}}_r\times {\mathrm{Base}}_s\right)$$
10		vb	$$setvarb$$
11		c1st	$$class{1}^{st}$$
12	10	cv	$$setvarb$$
13	11 12	cres	$$class\left({1^{st}\upharpoonright }_b\right)$$
14		vx	$$setvarx$$
15		vy	$$setvary$$
16	14	cv	$$setvarx$$
17		chom	$$class\mathrm{Hom}$$
18		cxpc	$$class{\times }_c$$
19	5 7 18	co	$$class\left(r{\times }_{c}s\right)$$
20	19 17	cfv	$$class\mathrm{Hom}\left(r{\times }_{c}s\right)$$
21	15	cv	$$setvary$$
22	16 21 20	co	$$class\left(x\mathrm{Hom}\left(r{\times }_{c}s\right)y\right)$$
23	11 22	cres	$$class\left({1^{st}\upharpoonright }_{\left(x\mathrm{Hom}\left(r{\times }_{c}s\right)y\right)}\right)$$
24	14 15 12 12 23	cmpo	$$class\left(x\in b,y\in b⟼{1^{st}\upharpoonright }_{\left(x\mathrm{Hom}\left(r{\times }_{c}s\right)y\right)}\right)$$
25	13 24	cop	$$class⟨{1^{st}\upharpoonright }_b,\left(x\in b,y\in b⟼{1^{st}\upharpoonright }_{\left(x\mathrm{Hom}\left(r{\times }_{c}s\right)y\right)}\right)⟩$$
26	10 9 25	csb	$$class⦋\left({\mathrm{Base}}_r\times {\mathrm{Base}}_s\right)/b⦌⟨{1^{st}\upharpoonright }_b,\left(x\in b,y\in b⟼{1^{st}\upharpoonright }_{\left(x\mathrm{Hom}\left(r{\times }_{c}s\right)y\right)}\right)⟩$$
27	1 3 2 2 26	cmpo	$$class\left(r\in \mathrm{Cat},s\in \mathrm{Cat}⟼⦋\left({\mathrm{Base}}_r\times {\mathrm{Base}}_s\right)/b⦌⟨{1^{st}\upharpoonright }_b,\left(x\in b,y\in b⟼{1^{st}\upharpoonright }_{\left(x\mathrm{Hom}\left(r{\times }_{c}s\right)y\right)}\right)⟩\right)$$
28	0 27	wceq	$$wff{1^{st}}_F=\left(r\in \mathrm{Cat},s\in \mathrm{Cat}⟼⦋\left({\mathrm{Base}}_r\times {\mathrm{Base}}_s\right)/b⦌⟨{1^{st}\upharpoonright }_b,\left(x\in b,y\in b⟼{1^{st}\upharpoonright }_{\left(x\mathrm{Hom}\left(r{\times }_{c}s\right)y\right)}\right)⟩\right)$$