Metamath Proof Explorer

Theorem 0thincg

Description: Any structure with an empty set of objects is a thin category. (Contributed by Zhi Wang, 17-Sep-2024)

Ref Expression
Assertion 0thincg 
|- ( ( C e. V /\ (/) = ( Base ` C ) ) -> C e. ThinCat )

Proof

Step Hyp Ref Expression
1 0catg 
 |-  ( ( C e. V /\ (/) = ( Base ` C ) ) -> C e. Cat )
2 ral0 
 |-  A. x e. (/) A. y e. ( Base ` C ) E* f f e. ( x ( Hom ` C ) y )
3 raleq 
 |-  ( (/) = ( Base ` C ) -> ( A. x e. (/) A. y e. ( Base ` C ) E* f f e. ( x ( Hom ` C ) y ) <-> A. x e. ( Base ` C ) A. y e. ( Base ` C ) E* f f e. ( x ( Hom ` C ) y ) ) )
4 2 3 mpbii 
 |-  ( (/) = ( Base ` C ) -> A. x e. ( Base ` C ) A. y e. ( Base ` C ) E* f f e. ( x ( Hom ` C ) y ) )
5 4 adantl 
 |-  ( ( C e. V /\ (/) = ( Base ` C ) ) -> A. x e. ( Base ` C ) A. y e. ( Base ` C ) E* f f e. ( x ( Hom ` C ) y ) )
6 eqid 
 |-  ( Base ` C ) = ( Base ` C )
7 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
8 6 7 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 ) ) )
9 1 5 8 sylanbrc 
 |-  ( ( C e. V /\ (/) = ( Base ` C ) ) -> C e. ThinCat )