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

Definition df-cco 13228
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 13215 . 2  class comp
2 c1 8734 . . . 4  class  1
3 c5 9794 . . . 4  class  5
42, 3cdc 10120 . . 3  class ; 1 5
54cslot 13142 . 2  class Slot ; 1 5
61, 5wceq 1624 1  wff comp  = Slot ; 1 5
Colors of variables: wff set class
This definition is referenced by:  ccondx  13316  ccoid  13317  ressco  13319  prdsvalstr  13348  oppchomfval  13612  oppccofval  13614  oppcbas  13616  rescco  13704  catstr  13826  fuccofval  13828  setccofval  13909  catccofval  13927  catcoppccl  13935  catcfuccl  13936  catcxpccl  13976
  Copyright terms: Public domain W3C validator