Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Zhi Wang
Examples of categories
Thin categories
thincc
Next ⟩
thinccd
Metamath Proof Explorer
Ascii
Unicode
Theorem
thincc
Description:
A thin category is a category.
(Contributed by
Zhi Wang
, 17-Sep-2024)
Ref
Expression
Assertion
thincc
⊢
C
∈
ThinCat
→
C
∈
Cat
Proof
Step
Hyp
Ref
Expression
1
eqid
⊢
Base
C
=
Base
C
2
eqid
⊢
Hom
⁡
C
=
Hom
⁡
C
3
1
2
isthinc
⊢
C
∈
ThinCat
↔
C
∈
Cat
∧
∀
x
∈
Base
C
∀
y
∈
Base
C
∃
*
f
f
∈
x
Hom
⁡
C
y
4
3
simplbi
⊢
C
∈
ThinCat
→
C
∈
Cat