Theorem isthincd

Description: The predicate "is a thin category" (deduction form). (Contributed by Zhi Wang, 17-Sep-2024)

	Ref	Expression
Hypotheses	isthincd.b	|- ( ph -> B = ( Base ` C ) )
	isthincd.h	|- ( ph -> H = ( Hom ` C ) )
	isthincd.t	|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> E* f f e. ( x H y ) )
	isthincd.c	|- ( ph -> C e. Cat )
Assertion	isthincd	|- ( ph -> C e. ThinCat )

Proof

Step	Hyp	Ref	Expression
1		isthincd.b	|- ( ph -> B = ( Base ` C ) )
2		isthincd.h	|- ( ph -> H = ( Hom ` C ) )
3		isthincd.t	|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> E* f f e. ( x H y ) )
4		isthincd.c	|- ( ph -> C e. Cat )
5	3	ralrimivva	|- ( ph -> A. x e. B A. y e. B E* f f e. ( x H y ) )
6	2	oveqd	|- ( ph -> ( x H y ) = ( x ( Hom ` C ) y ) )
7	6	eleq2d	|- ( ph -> ( f e. ( x H y ) <-> f e. ( x ( Hom ` C ) y ) ) )
8	7	mobidv	|- ( ph -> ( E* f f e. ( x H y ) <-> E* f f e. ( x ( Hom ` C ) y ) ) )
9	1 8	raleqbidv	|- ( ph -> ( A. y e. B E* f f e. ( x H y ) <-> A. y e. ( Base ` C ) E* f f e. ( x ( Hom ` C ) y ) ) )
10	1 9	raleqbidv	|- ( ph -> ( A. x e. B A. y e. B E* f f e. ( x H y ) <-> A. x e. ( Base ` C ) A. y e. ( Base ` C ) E* f f e. ( x ( Hom ` C ) y ) ) )
11	5 10	mpbid	|- ( ph -> A. x e. ( Base ` C ) A. y e. ( Base ` C ) E* f f e. ( x ( Hom ` C ) y ) )
12		eqid	|- ( Base ` C ) = ( Base ` C )
13		eqid	|- ( Hom ` C ) = ( Hom ` C )
14	12 13	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 ) ) )
15	4 11 14	sylanbrc	|- ( ph -> C e. ThinCat )