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

Definition df-coa 15237
 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 Nat Nat coda coda compcoda
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-coa
StepHypRef Expression
1 ccoa 15235 . 2 compa
2 vc . . 3
3 ccat 14915 . . 3
4 vg . . . 4
5 vf . . . 4
62cv 1378 . . . . 5
7 carw 15203 . . . . 5 Nat
86, 7cfv 5586 . . . 4 Nat
9 vh . . . . . . . 8
109cv 1378 . . . . . . 7
11 ccoda 15202 . . . . . . 7 coda
1210, 11cfv 5586 . . . . . 6 coda
134cv 1378 . . . . . . 7
14 cdoma 15201 . . . . . . 7
1513, 14cfv 5586 . . . . . 6
1612, 15wceq 1379 . . . . 5 coda
1716, 9, 8crab 2818 . . . 4 Nat coda
185cv 1378 . . . . . 6
1918, 14cfv 5586 . . . . 5
2013, 11cfv 5586 . . . . 5 coda
21 c2nd 6780 . . . . . . 7
2213, 21cfv 5586 . . . . . 6
2318, 21cfv 5586 . . . . . 6
2419, 15cop 4033 . . . . . . 7
25 cco 14563 . . . . . . . 8 comp
266, 25cfv 5586 . . . . . . 7 comp
2724, 20, 26co 6282 . . . . . 6 compcoda
2822, 23, 27co 6282 . . . . 5 compcoda
2919, 20, 28cotp 4035 . . . 4 coda compcoda
304, 5, 8, 17, 29cmpt2 6284 . . 3 Nat Nat coda coda compcoda
312, 3, 30cmpt 4505 . 2 Nat Nat coda coda compcoda
321, 31wceq 1379 1 compa Nat Nat coda coda compcoda
 Colors of variables: wff setvar class This definition is referenced by:  coafval  15245
 Copyright terms: Public domain W3C validator