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

Definition df-coa 14201
 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 14199 . 2 compa
2 vc . . 3
3 ccat 13879 . . 3
4 vg . . . 4
5 vf . . . 4
62cv 1651 . . . . 5
7 carw 14167 . . . . 5 Nat
86, 7cfv 5446 . . . 4 Nat
9 vh . . . . . . . 8
109cv 1651 . . . . . . 7
11 ccoda 14166 . . . . . . 7 coda
1210, 11cfv 5446 . . . . . 6 coda
134cv 1651 . . . . . . 7
14 cdoma 14165 . . . . . . 7
1513, 14cfv 5446 . . . . . 6
1612, 15wceq 1652 . . . . 5 coda
1716, 9, 8crab 2701 . . . 4 Nat coda
185cv 1651 . . . . . 6
1918, 14cfv 5446 . . . . 5
2013, 11cfv 5446 . . . . 5 coda
21 c2nd 6340 . . . . . . 7
2213, 21cfv 5446 . . . . . 6
2318, 21cfv 5446 . . . . . 6
2419, 15cop 3809 . . . . . . 7
25 cco 13531 . . . . . . . 8 comp
266, 25cfv 5446 . . . . . . 7 comp
2724, 20, 26co 6073 . . . . . 6 compcoda
2822, 23, 27co 6073 . . . . 5 compcoda
2919, 20, 28cotp 3810 . . . 4 coda compcoda
304, 5, 8, 17, 29cmpt2 6075 . . 3 Nat Nat coda coda compcoda
312, 3, 30cmpt 4258 . 2 Nat Nat coda coda compcoda
321, 31wceq 1652 1 compa Nat Nat coda coda compcoda
 Colors of variables: wff set class This definition is referenced by:  coafval  14209
 Copyright terms: Public domain W3C validator