Metamath Proof Explorer

Definition df-fuco

Description: Definition of functor composition bifunctors. Given three categories C , D , and E , ( <. C , D >. o.F E ) is a functor from the product category of two categories of functors to a category of functors ( fucofunc ). The object part maps two functors to their composition ( fuco11 and fuco11b ). The morphism part defines the "composition" of two natural transformations ( fuco22 ) into another natural transformation ( fuco22nat ) such that a "cube-like" diagram commutes. The naturality property also gives an alternate definition ( fuco23a ). Note that such "composition" is different from fucco because they "compose" along different "axes". (Contributed by Zhi Wang, 29-Sep-2025)

Ref Expression
Assertion df-fuco 
|- o.F = ( p e. _V , e e. _V |-> [_ ( 1st ` p ) / c ]_ [_ ( 2nd ` p ) / d ]_ [_ ( ( d Func e ) X. ( c Func d ) ) / w ]_ <. ( o.func |` w ) , ( u e. w , v e. w |-> [_ ( 1st ` ( 2nd ` u ) ) / f ]_ [_ ( 1st ` ( 1st ` u ) ) / k ]_ [_ ( 2nd ` ( 1st ` u ) ) / l ]_ [_ ( 1st ` ( 2nd ` v ) ) / m ]_ [_ ( 1st ` ( 1st ` v ) ) / r ]_ ( b e. ( ( 1st ` u ) ( d Nat e ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( c Nat d ) ( 2nd ` v ) ) |-> ( x e. ( Base ` c ) |-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` e ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) ) ) >. )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfuco 
 |-  o.F
1 vp 
 |-  p
2 cvv 
 |-  _V
3 ve 
 |-  e
4 c1st 
 |-  1st
5 1 cv 
 |-  p
6 5 4 cfv 
 |-  ( 1st ` p )
7 vc 
 |-  c
8 c2nd 
 |-  2nd
9 5 8 cfv 
 |-  ( 2nd ` p )
10 vd 
 |-  d
11 10 cv 
 |-  d
12 cfunc 
 |-  Func
13 3 cv 
 |-  e
14 11 13 12 co 
 |-  ( d Func e )
15 7 cv 
 |-  c
16 15 11 12 co 
 |-  ( c Func d )
17 14 16 cxp 
 |-  ( ( d Func e ) X. ( c Func d ) )
18 vw 
 |-  w
19 ccofu 
 |-  o.func
20 18 cv 
 |-  w
21 19 20 cres 
 |-  ( o.func |` w )
22 vu 
 |-  u
23 vv 
 |-  v
24 22 cv 
 |-  u
25 24 8 cfv 
 |-  ( 2nd ` u )
26 25 4 cfv 
 |-  ( 1st ` ( 2nd ` u ) )
27 vf 
 |-  f
28 24 4 cfv 
 |-  ( 1st ` u )
29 28 4 cfv 
 |-  ( 1st ` ( 1st ` u ) )
30 vk 
 |-  k
31 28 8 cfv 
 |-  ( 2nd ` ( 1st ` u ) )
32 vl 
 |-  l
33 23 cv 
 |-  v
34 33 8 cfv 
 |-  ( 2nd ` v )
35 34 4 cfv 
 |-  ( 1st ` ( 2nd ` v ) )
36 vm 
 |-  m
37 33 4 cfv 
 |-  ( 1st ` v )
38 37 4 cfv 
 |-  ( 1st ` ( 1st ` v ) )
39 vr 
 |-  r
40 vb 
 |-  b
41 cnat 
 |-  Nat
42 11 13 41 co 
 |-  ( d Nat e )
43 28 37 42 co 
 |-  ( ( 1st ` u ) ( d Nat e ) ( 1st ` v ) )
44 va 
 |-  a
45 15 11 41 co 
 |-  ( c Nat d )
46 25 34 45 co 
 |-  ( ( 2nd ` u ) ( c Nat d ) ( 2nd ` v ) )
47 vx 
 |-  x
48 cbs 
 |-  Base
49 15 48 cfv 
 |-  ( Base ` c )
50 40 cv 
 |-  b
51 36 cv 
 |-  m
52 47 cv 
 |-  x
53 52 51 cfv 
 |-  ( m ` x )
54 53 50 cfv 
 |-  ( b ` ( m ` x ) )
55 30 cv 
 |-  k
56 27 cv 
 |-  f
57 52 56 cfv 
 |-  ( f ` x )
58 57 55 cfv 
 |-  ( k ` ( f ` x ) )
59 53 55 cfv 
 |-  ( k ` ( m ` x ) )
60 58 59 cop 
 |-  <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >.
61 cco 
 |-  comp
62 13 61 cfv 
 |-  ( comp ` e )
63 39 cv 
 |-  r
64 53 63 cfv 
 |-  ( r ` ( m ` x ) )
65 60 64 62 co 
 |-  ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` e ) ( r ` ( m ` x ) ) )
66 32 cv 
 |-  l
67 57 53 66 co 
 |-  ( ( f ` x ) l ( m ` x ) )
68 44 cv 
 |-  a
69 52 68 cfv 
 |-  ( a ` x )
70 69 67 cfv 
 |-  ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) )
71 54 70 65 co 
 |-  ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` e ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) )
72 47 49 71 cmpt 
 |-  ( x e. ( Base ` c ) |-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` e ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) )
73 40 44 43 46 72 cmpo 
 |-  ( b e. ( ( 1st ` u ) ( d Nat e ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( c Nat d ) ( 2nd ` v ) ) |-> ( x e. ( Base ` c ) |-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` e ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) )
74 39 38 73 csb 
 |-  [_ ( 1st ` ( 1st ` v ) ) / r ]_ ( b e. ( ( 1st ` u ) ( d Nat e ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( c Nat d ) ( 2nd ` v ) ) |-> ( x e. ( Base ` c ) |-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` e ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) )
75 36 35 74 csb 
 |-  [_ ( 1st ` ( 2nd ` v ) ) / m ]_ [_ ( 1st ` ( 1st ` v ) ) / r ]_ ( b e. ( ( 1st ` u ) ( d Nat e ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( c Nat d ) ( 2nd ` v ) ) |-> ( x e. ( Base ` c ) |-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` e ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) )
76 32 31 75 csb 
 |-  [_ ( 2nd ` ( 1st ` u ) ) / l ]_ [_ ( 1st ` ( 2nd ` v ) ) / m ]_ [_ ( 1st ` ( 1st ` v ) ) / r ]_ ( b e. ( ( 1st ` u ) ( d Nat e ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( c Nat d ) ( 2nd ` v ) ) |-> ( x e. ( Base ` c ) |-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` e ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) )
77 30 29 76 csb 
 |-  [_ ( 1st ` ( 1st ` u ) ) / k ]_ [_ ( 2nd ` ( 1st ` u ) ) / l ]_ [_ ( 1st ` ( 2nd ` v ) ) / m ]_ [_ ( 1st ` ( 1st ` v ) ) / r ]_ ( b e. ( ( 1st ` u ) ( d Nat e ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( c Nat d ) ( 2nd ` v ) ) |-> ( x e. ( Base ` c ) |-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` e ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) )
78 27 26 77 csb 
 |-  [_ ( 1st ` ( 2nd ` u ) ) / f ]_ [_ ( 1st ` ( 1st ` u ) ) / k ]_ [_ ( 2nd ` ( 1st ` u ) ) / l ]_ [_ ( 1st ` ( 2nd ` v ) ) / m ]_ [_ ( 1st ` ( 1st ` v ) ) / r ]_ ( b e. ( ( 1st ` u ) ( d Nat e ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( c Nat d ) ( 2nd ` v ) ) |-> ( x e. ( Base ` c ) |-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` e ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) )
79 22 23 20 20 78 cmpo 
 |-  ( u e. w , v e. w |-> [_ ( 1st ` ( 2nd ` u ) ) / f ]_ [_ ( 1st ` ( 1st ` u ) ) / k ]_ [_ ( 2nd ` ( 1st ` u ) ) / l ]_ [_ ( 1st ` ( 2nd ` v ) ) / m ]_ [_ ( 1st ` ( 1st ` v ) ) / r ]_ ( b e. ( ( 1st ` u ) ( d Nat e ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( c Nat d ) ( 2nd ` v ) ) |-> ( x e. ( Base ` c ) |-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` e ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) ) )
80 21 79 cop 
 |-  <. ( o.func |` w ) , ( u e. w , v e. w |-> [_ ( 1st ` ( 2nd ` u ) ) / f ]_ [_ ( 1st ` ( 1st ` u ) ) / k ]_ [_ ( 2nd ` ( 1st ` u ) ) / l ]_ [_ ( 1st ` ( 2nd ` v ) ) / m ]_ [_ ( 1st ` ( 1st ` v ) ) / r ]_ ( b e. ( ( 1st ` u ) ( d Nat e ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( c Nat d ) ( 2nd ` v ) ) |-> ( x e. ( Base ` c ) |-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` e ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) ) ) >.
81 18 17 80 csb 
 |-  [_ ( ( d Func e ) X. ( c Func d ) ) / w ]_ <. ( o.func |` w ) , ( u e. w , v e. w |-> [_ ( 1st ` ( 2nd ` u ) ) / f ]_ [_ ( 1st ` ( 1st ` u ) ) / k ]_ [_ ( 2nd ` ( 1st ` u ) ) / l ]_ [_ ( 1st ` ( 2nd ` v ) ) / m ]_ [_ ( 1st ` ( 1st ` v ) ) / r ]_ ( b e. ( ( 1st ` u ) ( d Nat e ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( c Nat d ) ( 2nd ` v ) ) |-> ( x e. ( Base ` c ) |-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` e ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) ) ) >.
82 10 9 81 csb 
 |-  [_ ( 2nd ` p ) / d ]_ [_ ( ( d Func e ) X. ( c Func d ) ) / w ]_ <. ( o.func |` w ) , ( u e. w , v e. w |-> [_ ( 1st ` ( 2nd ` u ) ) / f ]_ [_ ( 1st ` ( 1st ` u ) ) / k ]_ [_ ( 2nd ` ( 1st ` u ) ) / l ]_ [_ ( 1st ` ( 2nd ` v ) ) / m ]_ [_ ( 1st ` ( 1st ` v ) ) / r ]_ ( b e. ( ( 1st ` u ) ( d Nat e ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( c Nat d ) ( 2nd ` v ) ) |-> ( x e. ( Base ` c ) |-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` e ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) ) ) >.
83 7 6 82 csb 
 |-  [_ ( 1st ` p ) / c ]_ [_ ( 2nd ` p ) / d ]_ [_ ( ( d Func e ) X. ( c Func d ) ) / w ]_ <. ( o.func |` w ) , ( u e. w , v e. w |-> [_ ( 1st ` ( 2nd ` u ) ) / f ]_ [_ ( 1st ` ( 1st ` u ) ) / k ]_ [_ ( 2nd ` ( 1st ` u ) ) / l ]_ [_ ( 1st ` ( 2nd ` v ) ) / m ]_ [_ ( 1st ` ( 1st ` v ) ) / r ]_ ( b e. ( ( 1st ` u ) ( d Nat e ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( c Nat d ) ( 2nd ` v ) ) |-> ( x e. ( Base ` c ) |-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` e ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) ) ) >.
84 1 3 2 2 83 cmpo 
 |-  ( p e. _V , e e. _V |-> [_ ( 1st ` p ) / c ]_ [_ ( 2nd ` p ) / d ]_ [_ ( ( d Func e ) X. ( c Func d ) ) / w ]_ <. ( o.func |` w ) , ( u e. w , v e. w |-> [_ ( 1st ` ( 2nd ` u ) ) / f ]_ [_ ( 1st ` ( 1st ` u ) ) / k ]_ [_ ( 2nd ` ( 1st ` u ) ) / l ]_ [_ ( 1st ` ( 2nd ` v ) ) / m ]_ [_ ( 1st ` ( 1st ` v ) ) / r ]_ ( b e. ( ( 1st ` u ) ( d Nat e ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( c Nat d ) ( 2nd ` v ) ) |-> ( x e. ( Base ` c ) |-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` e ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) ) ) >. )
85 0 84 wceq 
 |-  o.F = ( p e. _V , e e. _V |-> [_ ( 1st ` p ) / c ]_ [_ ( 2nd ` p ) / d ]_ [_ ( ( d Func e ) X. ( c Func d ) ) / w ]_ <. ( o.func |` w ) , ( u e. w , v e. w |-> [_ ( 1st ` ( 2nd ` u ) ) / f ]_ [_ ( 1st ` ( 1st ` u ) ) / k ]_ [_ ( 2nd ` ( 1st ` u ) ) / l ]_ [_ ( 1st ` ( 2nd ` v ) ) / m ]_ [_ ( 1st ` ( 1st ` v ) ) / r ]_ ( b e. ( ( 1st ` u ) ( d Nat e ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( c Nat d ) ( 2nd ` v ) ) |-> ( x e. ( Base ` c ) |-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` e ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) ) ) >. )