Definition df-1stf 16813

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

Assertion

Ref	Expression
df-1stf	|- 1stF = ( r e. Cat , s e. Cat |-> [_ ( ( Base ` r ) X. ( Base ` s ) ) / b ]_ <. ( 1st |` b ) , ( x e. b , y e. b |-> ( 1st |` ( x ( Hom ` ( r X.c s ) ) y ) ) ) >. )

Distinct variable group:   r, b, s, x, y

Detailed syntax breakdown of Definition df-1stf

Step	Hyp	Ref	Expression
1		c1stf 16809	. 2 class 1stF
2		vr	. . 3 setvar r
3		vs	. . 3 setvar s
4		ccat 16325	. . 3 class Cat
5		vb	. . . 4 setvar b
6	2	cv 1482	. . . . . 6 class r
7		cbs 15857	. . . . . 6 class Base
8	6, 7	cfv 5888	. . . . 5 class ( Base ` r )
9	3	cv 1482	. . . . . 6 class s
10	9, 7	cfv 5888	. . . . 5 class ( Base ` s )
11	8, 10	cxp 5112	. . . 4 class ( ( Base ` r ) X. ( Base ` s ) )
12		c1st 7166	. . . . . 6 class 1st
13	5	cv 1482	. . . . . 6 class b
14	12, 13	cres 5116	. . . . 5 class ( 1st |` b )
15		vx	. . . . . 6 setvar x
16		vy	. . . . . 6 setvar y
17	15	cv 1482	. . . . . . . 8 class x
18	16	cv 1482	. . . . . . . 8 class y
19		cxpc 16808	. . . . . . . . . 10 class X.c
20	6, 9, 19	co 6650	. . . . . . . . 9 class ( r X.c s )
21		chom 15952	. . . . . . . . 9 class Hom
22	20, 21	cfv 5888	. . . . . . . 8 class ( Hom ` ( r X.c s ) )
23	17, 18, 22	co 6650	. . . . . . 7 class ( x ( Hom ` ( r X.c s ) ) y )
24	12, 23	cres 5116	. . . . . 6 class ( 1st |` ( x ( Hom ` ( r X.c s ) ) y ) )
25	15, 16, 13, 13, 24	cmpt2 6652	. . . . 5 class ( x e. b , y e. b |-> ( 1st |` ( x ( Hom ` ( r X.c s ) ) y ) ) )
26	14, 25	cop 4183	. . . 4 class <. ( 1st |` b ) , ( x e. b , y e. b |-> ( 1st |` ( x ( Hom ` ( r X.c s ) ) y ) ) ) >.
27	5, 11, 26	csb 3533	. . 3 class [_ ( ( Base ` r ) X. ( Base ` s ) ) / b ]_ <. ( 1st |` b ) , ( x e. b , y e. b |-> ( 1st |` ( x ( Hom ` ( r X.c s ) ) y ) ) ) >.
28	2, 3, 4, 4, 27	cmpt2 6652	. 2 class ( r e. Cat , s e. Cat |-> [_ ( ( Base ` r ) X. ( Base ` s ) ) / b ]_ <. ( 1st |` b ) , ( x e. b , y e. b |-> ( 1st |` ( x ( Hom ` ( r X.c s ) ) y ) ) ) >. )
29	1, 28	wceq 1483	1 wff 1stF = ( r e. Cat , s e. Cat |-> [_ ( ( Base ` r ) X. ( Base ` s ) ) / b ]_ <. ( 1st |` b ) , ( x e. b , y e. b |-> ( 1st |` ( x ( Hom ` ( r X.c s ) ) y ) ) ) >. )

This definition is referenced by:  1stfval  16831