Metamath Proof Explorer

Definition df-cofu

Description: Define the composition of two functors. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Assertion df-cofu 
|- o.func = ( g e. _V , f e. _V |-> <. ( ( 1st ` g ) o. ( 1st ` f ) ) , ( x e. dom dom ( 2nd ` f ) , y e. dom dom ( 2nd ` f ) |-> ( ( ( ( 1st ` f ) ` x ) ( 2nd ` g ) ( ( 1st ` f ) ` y ) ) o. ( x ( 2nd ` f ) y ) ) ) >. )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccofu 
 |-  o.func
1 vg 
 |-  g
2 cvv 
 |-  _V
3 vf 
 |-  f
4 c1st 
 |-  1st
5 1 cv 
 |-  g
6 5 4 cfv 
 |-  ( 1st ` g )
7 3 cv 
 |-  f
8 7 4 cfv 
 |-  ( 1st ` f )
9 6 8 ccom 
 |-  ( ( 1st ` g ) o. ( 1st ` f ) )
10 vx 
 |-  x
11 c2nd 
 |-  2nd
12 7 11 cfv 
 |-  ( 2nd ` f )
13 12 cdm 
 |-  dom ( 2nd ` f )
14 13 cdm 
 |-  dom dom ( 2nd ` f )
15 vy 
 |-  y
16 10 cv 
 |-  x
17 16 8 cfv 
 |-  ( ( 1st ` f ) ` x )
18 5 11 cfv 
 |-  ( 2nd ` g )
19 15 cv 
 |-  y
20 19 8 cfv 
 |-  ( ( 1st ` f ) ` y )
21 17 20 18 co 
 |-  ( ( ( 1st ` f ) ` x ) ( 2nd ` g ) ( ( 1st ` f ) ` y ) )
22 16 19 12 co 
 |-  ( x ( 2nd ` f ) y )
23 21 22 ccom 
 |-  ( ( ( ( 1st ` f ) ` x ) ( 2nd ` g ) ( ( 1st ` f ) ` y ) ) o. ( x ( 2nd ` f ) y ) )
24 10 15 14 14 23 cmpo 
 |-  ( x e. dom dom ( 2nd ` f ) , y e. dom dom ( 2nd ` f ) |-> ( ( ( ( 1st ` f ) ` x ) ( 2nd ` g ) ( ( 1st ` f ) ` y ) ) o. ( x ( 2nd ` f ) y ) ) )
25 9 24 cop 
 |-  <. ( ( 1st ` g ) o. ( 1st ` f ) ) , ( x e. dom dom ( 2nd ` f ) , y e. dom dom ( 2nd ` f ) |-> ( ( ( ( 1st ` f ) ` x ) ( 2nd ` g ) ( ( 1st ` f ) ` y ) ) o. ( x ( 2nd ` f ) y ) ) ) >.
26 1 3 2 2 25 cmpo 
 |-  ( g e. _V , f e. _V |-> <. ( ( 1st ` g ) o. ( 1st ` f ) ) , ( x e. dom dom ( 2nd ` f ) , y e. dom dom ( 2nd ` f ) |-> ( ( ( ( 1st ` f ) ` x ) ( 2nd ` g ) ( ( 1st ` f ) ` y ) ) o. ( x ( 2nd ` f ) y ) ) ) >. )
27 0 26 wceq 
 |-  o.func = ( g e. _V , f e. _V |-> <. ( ( 1st ` g ) o. ( 1st ` f ) ) , ( x e. dom dom ( 2nd ` f ) , y e. dom dom ( 2nd ` f ) |-> ( ( ( ( 1st ` f ) ` x ) ( 2nd ` g ) ( ( 1st ` f ) ` y ) ) o. ( x ( 2nd ` f ) y ) ) ) >. )