Description: Define the composition operation of a category. (Contributed by Mario Carneiro, 2-Jan-2017) Use its index-independent form ccoid instead. (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-cco | |- comp = Slot ; 1 5 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cco | |- comp |
|
| 1 | c1 | |- 1 |
|
| 2 | c5 | |- 5 |
|
| 3 | 1 2 | cdc | |- ; 1 5 |
| 4 | 3 | cslot | |- Slot ; 1 5 |
| 5 | 0 4 | wceq | |- comp = Slot ; 1 5 |