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

Definition df-cco 13249
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 13236 . 2  class comp
2 c1 8754 . . . 4  class  1
3 c5 9814 . . . 4  class  5
42, 3cdc 10140 . . 3  class ; 1 5
54cslot 13163 . 2  class Slot ; 1 5
61, 5wceq 1632 1  wff comp  = Slot ; 1 5
Colors of variables: wff set class
This definition is referenced by:  ccondx  13337  ccoid  13338  ressco  13340  prdsvalstr  13369  oppchomfval  13633  oppccofval  13635  oppcbas  13637  rescco  13725  catstr  13847  fuccofval  13849  setccofval  13930  catccofval  13948  catcoppccl  13956  catcfuccl  13957  catcxpccl  13997
  Copyright terms: Public domain W3C validator