Metamath Proof Explorer


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