Theorem isthinc3

Description: A thin category is a category in which, given a pair of objects x and y and any two morphisms f , g from x to y , the morphisms are equal. (Contributed by Zhi Wang, 17-Sep-2024)

	Ref	Expression
Hypotheses	isthinc.b	|- B = ( Base ` C )
	isthinc.h	|- H = ( Hom ` C )
Assertion	isthinc3	|- ( C e. ThinCat <-> ( C e. Cat /\ A. x e. B A. y e. B A. f e. ( x H y ) A. g e. ( x H y ) f = g ) )

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		moel	|- ( E* f f e. ( x H y ) <-> A. f e. ( x H y ) A. g e. ( x H y ) f = g )
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 A. f e. ( x H y ) A. g e. ( x H y ) f = g )
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 A. f e. ( x H y ) A. g e. ( x H y ) f = g ) )
7	3 6	bitri	|- ( C e. ThinCat <-> ( C e. Cat /\ A. x e. B A. y e. B A. f e. ( x H y ) A. g e. ( x H y ) f = g ) )