Metamath Proof Explorer

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 
|- 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 Xc. s ) ) y ) ) ) >. )

Detailed syntax breakdown

Step Hyp Ref Expression
0 c1stf 
 |-  1stF
1 vr 
 |-  r
2 ccat 
 |-  Cat
3 vs 
 |-  s
4 cbs 
 |-  Base
5 1 cv 
 |-  r
6 5 4 cfv 
 |-  ( Base ` r )
7 3 cv 
 |-  s
8 7 4 cfv 
 |-  ( Base ` s )
9 6 8 cxp 
 |-  ( ( Base ` r ) X. ( Base ` s ) )
10 vb 
 |-  b
11 c1st 
 |-  1st
12 10 cv 
 |-  b
13 11 12 cres 
 |-  ( 1st |` b )
14 vx 
 |-  x
15 vy 
 |-  y
16 14 cv 
 |-  x
17 chom 
 |-  Hom
18 cxpc 
 |-  Xc.
19 5 7 18 co 
 |-  ( r Xc. s )
20 19 17 cfv 
 |-  ( Hom ` ( r Xc. s ) )
21 15 cv 
 |-  y
22 16 21 20 co 
 |-  ( x ( Hom ` ( r Xc. s ) ) y )
23 11 22 cres 
 |-  ( 1st |` ( x ( Hom ` ( r Xc. s ) ) y ) )
24 14 15 12 12 23 cmpo 
 |-  ( x e. b , y e. b |-> ( 1st |` ( x ( Hom ` ( r Xc. s ) ) y ) ) )
25 13 24 cop 
 |-  <. ( 1st |` b ) , ( x e. b , y e. b |-> ( 1st |` ( x ( Hom ` ( r Xc. s ) ) y ) ) ) >.
26 10 9 25 csb 
 |-  [_ ( ( Base ` r ) X. ( Base ` s ) ) / b ]_ <. ( 1st |` b ) , ( x e. b , y e. b |-> ( 1st |` ( x ( Hom ` ( r Xc. s ) ) y ) ) ) >.
27 1 3 2 2 26 cmpo 
 |-  ( r e. Cat , s e. Cat |-> [_ ( ( Base ` r ) X. ( Base ` s ) ) / b ]_ <. ( 1st |` b ) , ( x e. b , y e. b |-> ( 1st |` ( x ( Hom ` ( r Xc. s ) ) y ) ) ) >. )
28 0 27 wceq 
 |-  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 Xc. s ) ) y ) ) ) >. )