Metamath Proof Explorer

Theorem thincc

Description: A thin category is a category. (Contributed by Zhi Wang, 17-Sep-2024)

Ref Expression
Assertion thincc 
|- ( C e. ThinCat -> C e. Cat )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Base ` C ) = ( Base ` C )
2 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
3 1 2 isthinc 
 |-  ( C e. ThinCat <-> ( C e. Cat /\ A. x e. ( Base ` C ) A. y e. ( Base ` C ) E* f f e. ( x ( Hom ` C ) y ) ) )
4 3 simplbi 
 |-  ( C e. ThinCat -> C e. Cat )