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

Definition df-cco 13233
Description: Define the composition operation of a category. (Contributed by Mario Carneiro, 2-Jan-2017.)
Assertion
Ref Expression
df-cco  |- comp  = Slot ; 1 5

Detailed syntax breakdown of Definition df-cco
StepHypRef Expression
1 cco 13220 . 2  class comp
2 c1 8738 . . . 4  class  1
3 c5 9798 . . . 4  class  5
42, 3cdc 10124 . . 3  class ; 1 5
54cslot 13147 . 2  class Slot ; 1 5
61, 5wceq 1623 1  wff comp  = Slot ; 1 5
Colors of variables: wff set class
This definition is referenced by:  ccondx  13321  ccoid  13322  ressco  13324  prdsvalstr  13353  oppchomfval  13617  oppccofval  13619  oppcbas  13621  rescco  13709  catstr  13831  fuccofval  13833  setccofval  13914  catccofval  13932  catcoppccl  13940  catcfuccl  13941  catcxpccl  13981
  Copyright terms: Public domain W3C validator