MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-1stf Unicode version

Definition df-1stf 13947
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
StepHypRef Expression
1 c1stf 13943 . 2  class  1stF
2 vr . . 3  set  r
3 vs . . 3  set  s
4 ccat 13566 . . 3  class  Cat
5 vb . . . 4  set  b
62cv 1622 . . . . . 6  class  r
7 cbs 13148 . . . . . 6  class  Base
86, 7cfv 5255 . . . . 5  class  ( Base `  r )
93cv 1622 . . . . . 6  class  s
109, 7cfv 5255 . . . . 5  class  ( Base `  s )
118, 10cxp 4687 . . . 4  class  ( (
Base `  r )  X.  ( Base `  s
) )
12 c1st 6120 . . . . . 6  class  1st
135cv 1622 . . . . . 6  class  b
1412, 13cres 4691 . . . . 5  class  ( 1st  |`  b )
15 vx . . . . . 6  set  x
16 vy . . . . . 6  set  y
1715cv 1622 . . . . . . . 8  class  x
1816cv 1622 . . . . . . . 8  class  y
19 cxpc 13942 . . . . . . . . . 10  class  X.c
206, 9, 19co 5858 . . . . . . . . 9  class  ( r  X.c  s )
21 chom 13219 . . . . . . . . 9  class  Hom
2220, 21cfv 5255 . . . . . . . 8  class  (  Hom  `  ( r  X.c  s ) )
2317, 18, 22co 5858 . . . . . . 7  class  ( x (  Hom  `  (
r  X.c  s ) ) y )
2412, 23cres 4691 . . . . . 6  class  ( 1st  |`  ( x (  Hom  `  ( r  X.c  s ) ) y ) )
2515, 16, 13, 13, 24cmpt2 5860 . . . . 5  class  ( x  e.  b ,  y  e.  b  |->  ( 1st  |`  ( x (  Hom  `  ( r  X.c  s ) ) y ) ) )
2614, 25cop 3643 . . . 4  class  <. ( 1st  |`  b ) ,  ( x  e.  b ,  y  e.  b 
|->  ( 1st  |`  (
x (  Hom  `  (
r  X.c  s ) ) y ) ) ) >.
275, 11, 26csb 3081 . . 3  class  [_ (
( Base `  r )  X.  ( Base `  s
) )  /  b ]_ <. ( 1st  |`  b
) ,  ( x  e.  b ,  y  e.  b  |->  ( 1st  |`  ( x (  Hom  `  ( r  X.c  s ) ) y ) ) ) >.
282, 3, 4, 4, 27cmpt2 5860 . 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 ) ) ) >. )
291, 28wceq 1623 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 ) ) ) >. )
Colors of variables: wff set class
This definition is referenced by:  1stfval  13965
  Copyright terms: Public domain W3C validator