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 ) )