This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isthinc2

Description: A thin category is a category in which all hom-sets have cardinality less than or equal to the cardinality of 1o . (Contributed by Zhi Wang, 17-Sep-2024)

Ref Expression
Hypotheses isthinc.b 
|- B = ( Base ` C )
isthinc.h 
|- H = ( Hom ` C )
Assertion isthinc2 
|- ( C e. ThinCat <-> ( C e. Cat /\ A. x e. B A. y e. B ( x H y ) ~<_ 1o ) )

Proof

Step Hyp Ref Expression
1 isthinc.b 
 |-  B = ( Base ` C )
2 isthinc.h 
 |-  H = ( Hom ` C )
3 1 2 isthinc 
 |-  ( C e. ThinCat <-> ( C e. Cat /\ A. x e. B A. y e. B E* f f e. ( x H y ) ) )
4 modom2 
 |-  ( E* f f e. ( x H y ) <-> ( x H y ) ~<_ 1o )
5 4 2ralbii 
 |-  ( A. x e. B A. y e. B E* f f e. ( x H y ) <-> A. x e. B A. y e. B ( x H y ) ~<_ 1o )
6 5 anbi2i 
 |-  ( ( C e. Cat /\ A. x e. B A. y e. B E* f f e. ( x H y ) ) <-> ( C e. Cat /\ A. x e. B A. y e. B ( x H y ) ~<_ 1o ) )
7 3 6 bitri 
 |-  ( C e. ThinCat <-> ( C e. Cat /\ A. x e. B A. y e. B ( x H y ) ~<_ 1o ) )