Metamath Proof Explorer

Definition df-fuc

Description: Definition of the category of functors between two fixed categories, with the objects being functors and the morphisms being natural transformations. Definition 6.15 in Adamek p. 87. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Assertion df-fuc 
|- FuncCat = ( t e. Cat , u e. Cat |-> { <. ( Base ` ndx ) , ( t Func u ) >. , <. ( Hom ` ndx ) , ( t Nat u ) >. , <. ( comp ` ndx ) , ( v e. ( ( t Func u ) X. ( t Func u ) ) , h e. ( t Func u ) |-> [_ ( 1st ` v ) / f ]_ [_ ( 2nd ` v ) / g ]_ ( b e. ( g ( t Nat u ) h ) , a e. ( f ( t Nat u ) g ) |-> ( x e. ( Base ` t ) |-> ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. ( comp ` u ) ( ( 1st ` h ) ` x ) ) ( a ` x ) ) ) ) ) >. } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfuc 
 |-  FuncCat
1 vt 
 |-  t
2 ccat 
 |-  Cat
3 vu 
 |-  u
4 cbs 
 |-  Base
5 cnx 
 |-  ndx
6 5 4 cfv 
 |-  ( Base ` ndx )
7 1 cv 
 |-  t
8 cfunc 
 |-  Func
9 3 cv 
 |-  u
10 7 9 8 co 
 |-  ( t Func u )
11 6 10 cop 
 |-  <. ( Base ` ndx ) , ( t Func u ) >.
12 chom 
 |-  Hom
13 5 12 cfv 
 |-  ( Hom ` ndx )
14 cnat 
 |-  Nat
15 7 9 14 co 
 |-  ( t Nat u )
16 13 15 cop 
 |-  <. ( Hom ` ndx ) , ( t Nat u ) >.
17 cco 
 |-  comp
18 5 17 cfv 
 |-  ( comp ` ndx )
19 vv 
 |-  v
20 10 10 cxp 
 |-  ( ( t Func u ) X. ( t Func u ) )
21 vh 
 |-  h
22 c1st 
 |-  1st
23 19 cv 
 |-  v
24 23 22 cfv 
 |-  ( 1st ` v )
25 vf 
 |-  f
26 c2nd 
 |-  2nd
27 23 26 cfv 
 |-  ( 2nd ` v )
28 vg 
 |-  g
29 vb 
 |-  b
30 28 cv 
 |-  g
31 21 cv 
 |-  h
32 30 31 15 co 
 |-  ( g ( t Nat u ) h )
33 va 
 |-  a
34 25 cv 
 |-  f
35 34 30 15 co 
 |-  ( f ( t Nat u ) g )
36 vx 
 |-  x
37 7 4 cfv 
 |-  ( Base ` t )
38 29 cv 
 |-  b
39 36 cv 
 |-  x
40 39 38 cfv 
 |-  ( b ` x )
41 34 22 cfv 
 |-  ( 1st ` f )
42 39 41 cfv 
 |-  ( ( 1st ` f ) ` x )
43 30 22 cfv 
 |-  ( 1st ` g )
44 39 43 cfv 
 |-  ( ( 1st ` g ) ` x )
45 42 44 cop 
 |-  <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >.
46 9 17 cfv 
 |-  ( comp ` u )
47 31 22 cfv 
 |-  ( 1st ` h )
48 39 47 cfv 
 |-  ( ( 1st ` h ) ` x )
49 45 48 46 co 
 |-  ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. ( comp ` u ) ( ( 1st ` h ) ` x ) )
50 33 cv 
 |-  a
51 39 50 cfv 
 |-  ( a ` x )
52 40 51 49 co 
 |-  ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. ( comp ` u ) ( ( 1st ` h ) ` x ) ) ( a ` x ) )
53 36 37 52 cmpt 
 |-  ( x e. ( Base ` t ) |-> ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. ( comp ` u ) ( ( 1st ` h ) ` x ) ) ( a ` x ) ) )
54 29 33 32 35 53 cmpo 
 |-  ( b e. ( g ( t Nat u ) h ) , a e. ( f ( t Nat u ) g ) |-> ( x e. ( Base ` t ) |-> ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. ( comp ` u ) ( ( 1st ` h ) ` x ) ) ( a ` x ) ) ) )
55 28 27 54 csb 
 |-  [_ ( 2nd ` v ) / g ]_ ( b e. ( g ( t Nat u ) h ) , a e. ( f ( t Nat u ) g ) |-> ( x e. ( Base ` t ) |-> ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. ( comp ` u ) ( ( 1st ` h ) ` x ) ) ( a ` x ) ) ) )
56 25 24 55 csb 
 |-  [_ ( 1st ` v ) / f ]_ [_ ( 2nd ` v ) / g ]_ ( b e. ( g ( t Nat u ) h ) , a e. ( f ( t Nat u ) g ) |-> ( x e. ( Base ` t ) |-> ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. ( comp ` u ) ( ( 1st ` h ) ` x ) ) ( a ` x ) ) ) )
57 19 21 20 10 56 cmpo 
 |-  ( v e. ( ( t Func u ) X. ( t Func u ) ) , h e. ( t Func u ) |-> [_ ( 1st ` v ) / f ]_ [_ ( 2nd ` v ) / g ]_ ( b e. ( g ( t Nat u ) h ) , a e. ( f ( t Nat u ) g ) |-> ( x e. ( Base ` t ) |-> ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. ( comp ` u ) ( ( 1st ` h ) ` x ) ) ( a ` x ) ) ) ) )
58 18 57 cop 
 |-  <. ( comp ` ndx ) , ( v e. ( ( t Func u ) X. ( t Func u ) ) , h e. ( t Func u ) |-> [_ ( 1st ` v ) / f ]_ [_ ( 2nd ` v ) / g ]_ ( b e. ( g ( t Nat u ) h ) , a e. ( f ( t Nat u ) g ) |-> ( x e. ( Base ` t ) |-> ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. ( comp ` u ) ( ( 1st ` h ) ` x ) ) ( a ` x ) ) ) ) ) >.
59 11 16 58 ctp 
 |-  { <. ( Base ` ndx ) , ( t Func u ) >. , <. ( Hom ` ndx ) , ( t Nat u ) >. , <. ( comp ` ndx ) , ( v e. ( ( t Func u ) X. ( t Func u ) ) , h e. ( t Func u ) |-> [_ ( 1st ` v ) / f ]_ [_ ( 2nd ` v ) / g ]_ ( b e. ( g ( t Nat u ) h ) , a e. ( f ( t Nat u ) g ) |-> ( x e. ( Base ` t ) |-> ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. ( comp ` u ) ( ( 1st ` h ) ` x ) ) ( a ` x ) ) ) ) ) >. }
60 1 3 2 2 59 cmpo 
 |-  ( t e. Cat , u e. Cat |-> { <. ( Base ` ndx ) , ( t Func u ) >. , <. ( Hom ` ndx ) , ( t Nat u ) >. , <. ( comp ` ndx ) , ( v e. ( ( t Func u ) X. ( t Func u ) ) , h e. ( t Func u ) |-> [_ ( 1st ` v ) / f ]_ [_ ( 2nd ` v ) / g ]_ ( b e. ( g ( t Nat u ) h ) , a e. ( f ( t Nat u ) g ) |-> ( x e. ( Base ` t ) |-> ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. ( comp ` u ) ( ( 1st ` h ) ` x ) ) ( a ` x ) ) ) ) ) >. } )
61 0 60 wceq 
 |-  FuncCat = ( t e. Cat , u e. Cat |-> { <. ( Base ` ndx ) , ( t Func u ) >. , <. ( Hom ` ndx ) , ( t Nat u ) >. , <. ( comp ` ndx ) , ( v e. ( ( t Func u ) X. ( t Func u ) ) , h e. ( t Func u ) |-> [_ ( 1st ` v ) / f ]_ [_ ( 2nd ` v ) / g ]_ ( b e. ( g ( t Nat u ) h ) , a e. ( f ( t Nat u ) g ) |-> ( x e. ( Base ` t ) |-> ( ( b ` x ) ( <. ( ( 1st ` f ) ` x ) , ( ( 1st ` g ) ` x ) >. ( comp ` u ) ( ( 1st ` h ) ` x ) ) ( a ` x ) ) ) ) ) >. } )