Metamath Proof Explorer

Definition df-coa

Description: Definition of the composition of arrows. Since arrows are tagged with domain and codomain, this does not need to be a quinary operation like the regular composition in a category comp . Instead, it is a partial binary operation on arrows, which is defined when the domain of the first arrow matches the codomain of the second. (Contributed by Mario Carneiro, 11-Jan-2017)

Ref Expression
Assertion df-coa 
|- compA = ( c e. Cat |-> ( g e. ( Arrow ` c ) , f e. { h e. ( Arrow ` c ) | ( codA ` h ) = ( domA ` g ) } |-> <. ( domA ` f ) , ( codA ` g ) , ( ( 2nd ` g ) ( <. ( domA ` f ) , ( domA ` g ) >. ( comp ` c ) ( codA ` g ) ) ( 2nd ` f ) ) >. ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccoa 
 |-  compA
1 vc 
 |-  c
2 ccat 
 |-  Cat
3 vg 
 |-  g
4 carw 
 |-  Arrow
5 1 cv 
 |-  c
6 5 4 cfv 
 |-  ( Arrow ` c )
7 vf 
 |-  f
8 vh 
 |-  h
9 ccoda 
 |-  codA
10 8 cv 
 |-  h
11 10 9 cfv 
 |-  ( codA ` h )
12 cdoma 
 |-  domA
13 3 cv 
 |-  g
14 13 12 cfv 
 |-  ( domA ` g )
15 11 14 wceq 
 |-  ( codA ` h ) = ( domA ` g )
16 15 8 6 crab 
 |-  { h e. ( Arrow ` c ) | ( codA ` h ) = ( domA ` g ) }
17 7 cv 
 |-  f
18 17 12 cfv 
 |-  ( domA ` f )
19 13 9 cfv 
 |-  ( codA ` g )
20 c2nd 
 |-  2nd
21 13 20 cfv 
 |-  ( 2nd ` g )
22 18 14 cop 
 |-  <. ( domA ` f ) , ( domA ` g ) >.
23 cco 
 |-  comp
24 5 23 cfv 
 |-  ( comp ` c )
25 22 19 24 co 
 |-  ( <. ( domA ` f ) , ( domA ` g ) >. ( comp ` c ) ( codA ` g ) )
26 17 20 cfv 
 |-  ( 2nd ` f )
27 21 26 25 co 
 |-  ( ( 2nd ` g ) ( <. ( domA ` f ) , ( domA ` g ) >. ( comp ` c ) ( codA ` g ) ) ( 2nd ` f ) )
28 18 19 27 cotp 
 |-  <. ( domA ` f ) , ( codA ` g ) , ( ( 2nd ` g ) ( <. ( domA ` f ) , ( domA ` g ) >. ( comp ` c ) ( codA ` g ) ) ( 2nd ` f ) ) >.
29 3 7 6 16 28 cmpo 
 |-  ( g e. ( Arrow ` c ) , f e. { h e. ( Arrow ` c ) | ( codA ` h ) = ( domA ` g ) } |-> <. ( domA ` f ) , ( codA ` g ) , ( ( 2nd ` g ) ( <. ( domA ` f ) , ( domA ` g ) >. ( comp ` c ) ( codA ` g ) ) ( 2nd ` f ) ) >. )
30 1 2 29 cmpt 
 |-  ( c e. Cat |-> ( g e. ( Arrow ` c ) , f e. { h e. ( Arrow ` c ) | ( codA ` h ) = ( domA ` g ) } |-> <. ( domA ` f ) , ( codA ` g ) , ( ( 2nd ` g ) ( <. ( domA ` f ) , ( domA ` g ) >. ( comp ` c ) ( codA ` g ) ) ( 2nd ` f ) ) >. ) )
31 0 30 wceq 
 |-  compA = ( c e. Cat |-> ( g e. ( Arrow ` c ) , f e. { h e. ( Arrow ` c ) | ( codA ` h ) = ( domA ` g ) } |-> <. ( domA ` f ) , ( codA ` g ) , ( ( 2nd ` g ) ( <. ( domA ` f ) , ( domA ` g ) >. ( comp ` c ) ( codA ` g ) ) ( 2nd ` f ) ) >. ) )