Database
BASIC STRUCTURES
Extensible structures
Slot definitions
df-hom
Next ⟩
df-cco
Metamath Proof Explorer
Ascii
Unicode
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
14
Detailed syntax breakdown
Step
Hyp
Ref
Expression
0
chom
class
Hom
1
c1
class
1
2
c4
class
4
3
1
2
cdc
class
14
4
3
cslot
class
Slot
14
5
0
4
wceq
wff
Hom
=
Slot
14