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} = (r \in Cat, s \in Cat ⟼ ⦋ ({Base}_{r} \times {Base}_{s}) / b ⦌ ⟨{1^{st} ↾}_{b}, (x \in b, y \in b ⟼ {1^{st} ↾}_{(x Hom (r \times_{c} s) y)})⟩)$

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

Metamath Proof Explorer