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 |