Metamath Proof Explorer

Definition df-hom

Description: Define the hom-set component of a category. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Assertion df-hom 
|- Hom = Slot ; 1 4

Detailed syntax breakdown

Step Hyp Ref Expression
0 chom 
 |-  Hom
1 c1 
 |-  1
2 c4 
 |-  4
3 1 2 cdc 
 |-  ; 1 4
4 3 cslot 
 |-  Slot ; 1 4
5 0 4 wceq 
 |-  Hom = Slot ; 1 4