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

Definition df-hom 13227
Description: Define the hom-set component of a category. (Contributed by Mario Carneiro, 2-Jan-2017.)
Assertion
Ref Expression
df-hom  |-  Hom  = Slot ; 1 4

Detailed syntax breakdown of Definition df-hom
StepHypRef Expression
1 chom 13214 . 2  class  Hom
2 c1 8734 . . . 4  class  1
3 c4 9793 . . . 4  class  4
42, 3cdc 10120 . . 3  class ; 1 4
54cslot 13142 . 2  class Slot ; 1 4
61, 5wceq 1624 1  wff  Hom  = Slot ; 1 4
Colors of variables: wff set class
This definition is referenced by:  homndx  13314  homid  13315  resshom  13318  prdsvalstr  13348  prdsval  13350  oppchomfval  13612  oppcbas  13616  rescbas  13701  reschom  13702  rescco  13704  rescabs  13705  wunfunc  13768  wunnat  13825  catstr  13826  fuchom  13830  setchomfval  13906  catchomfval  13925  catcoppccl  13935  catcfuccl  13936  catcxpccl  13976
  Copyright terms: Public domain W3C validator