Metamath Proof Explorer

Definition df-cco

Description: Define the composition operation of a category. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Assertion df-cco 
|- comp = Slot ; 1 5

Detailed syntax breakdown

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