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

Definition df-coa 13904
Description: Definition of the composition of arrows. Since arrows are tagged with domain and codomain, this does not need to be a 5-ary 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.)
Assertion
Ref Expression
df-coa  |- compa  =  ( c  e. 
Cat  |->  ( g  e.  (Nat `  c ) ,  f  e.  { h  e.  (Nat `  c )  |  (coda
`  h )  =  (domA `  g ) }  |->  <.
(domA `  f ) ,  (coda `  g ) ,  ( ( 2nd `  g
) ( <. (domA `  f ) ,  (domA `  g ) >. (comp `  c ) (coda `  g
) ) ( 2nd `  f ) ) >.
) )
Distinct variable group:    f, c, g, h

Detailed syntax breakdown of Definition df-coa
StepHypRef Expression
1 ccoa 13902 . 2  class compa
2 vc . . 3  set  c
3 ccat 13582 . . 3  class  Cat
4 vg . . . 4  set  g
5 vf . . . 4  set  f
62cv 1631 . . . . 5  class  c
7 carw 13870 . . . . 5  class Nat
86, 7cfv 5271 . . . 4  class  (Nat `  c )
9 vh . . . . . . . 8  set  h
109cv 1631 . . . . . . 7  class  h
11 ccoda 13869 . . . . . . 7  class coda
1210, 11cfv 5271 . . . . . 6  class  (coda `  h
)
134cv 1631 . . . . . . 7  class  g
14 cdoma 13868 . . . . . . 7  class domA
1513, 14cfv 5271 . . . . . 6  class  (domA `  g )
1612, 15wceq 1632 . . . . 5  wff  (coda `  h
)  =  (domA `  g )
1716, 9, 8crab 2560 . . . 4  class  { h  e.  (Nat `  c )  |  (coda
`  h )  =  (domA `  g ) }
185cv 1631 . . . . . 6  class  f
1918, 14cfv 5271 . . . . 5  class  (domA `  f )
2013, 11cfv 5271 . . . . 5  class  (coda `  g
)
21 c2nd 6137 . . . . . . 7  class  2nd
2213, 21cfv 5271 . . . . . 6  class  ( 2nd `  g )
2318, 21cfv 5271 . . . . . 6  class  ( 2nd `  f )
2419, 15cop 3656 . . . . . . 7  class  <. (domA `  f ) ,  (domA `  g ) >.
25 cco 13236 . . . . . . . 8  class comp
266, 25cfv 5271 . . . . . . 7  class  (comp `  c )
2724, 20, 26co 5874 . . . . . 6  class  ( <.
(domA `  f ) ,  (domA `  g
) >. (comp `  c
) (coda
`  g ) )
2822, 23, 27co 5874 . . . . 5  class  ( ( 2nd `  g ) ( <. (domA `  f ) ,  (domA `  g
) >. (comp `  c
) (coda
`  g ) ) ( 2nd `  f
) )
2919, 20, 28cotp 3657 . . . 4  class  <. (domA `  f ) ,  (coda
`  g ) ,  ( ( 2nd `  g
) ( <. (domA `  f ) ,  (domA `  g ) >. (comp `  c ) (coda `  g
) ) ( 2nd `  f ) ) >.
304, 5, 8, 17, 29cmpt2 5876 . . 3  class  ( g  e.  (Nat `  c
) ,  f  e. 
{ h  e.  (Nat
`  c )  |  (coda
`  h )  =  (domA `  g ) }  |->  <.
(domA `  f ) ,  (coda `  g ) ,  ( ( 2nd `  g
) ( <. (domA `  f ) ,  (domA `  g ) >. (comp `  c ) (coda `  g
) ) ( 2nd `  f ) ) >.
)
312, 3, 30cmpt 4093 . 2  class  ( c  e.  Cat  |->  ( g  e.  (Nat `  c
) ,  f  e. 
{ h  e.  (Nat
`  c )  |  (coda
`  h )  =  (domA `  g ) }  |->  <.
(domA `  f ) ,  (coda `  g ) ,  ( ( 2nd `  g
) ( <. (domA `  f ) ,  (domA `  g ) >. (comp `  c ) (coda `  g
) ) ( 2nd `  f ) ) >.
) )
321, 31wceq 1632 1  wff compa  =  ( c  e. 
Cat  |->  ( g  e.  (Nat `  c ) ,  f  e.  { h  e.  (Nat `  c )  |  (coda
`  h )  =  (domA `  g ) }  |->  <.
(domA `  f ) ,  (coda `  g ) ,  ( ( 2nd `  g
) ( <. (domA `  f ) ,  (domA `  g ) >. (comp `  c ) (coda `  g
) ) ( 2nd `  f ) ) >.
) )
Colors of variables: wff set class
This definition is referenced by:  coafval  13912
  Copyright terms: Public domain W3C validator