Theorem thincfth

Description: A functor from a thin category is faithful. (Contributed by Zhi Wang, 1-Oct-2024)

	Ref	Expression
Hypotheses	thincfth.c	|- ( ph -> C e. ThinCat )
	thincfth.f	|- ( ph -> F ( C Func D ) G )
Assertion	thincfth	|- ( ph -> F ( C Faith D ) G )

Proof

Step	Hyp	Ref	Expression
1		thincfth.c	|- ( ph -> C e. ThinCat )
2		thincfth.f	|- ( ph -> F ( C Func D ) G )
3	1	adantr	|- ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> C e. ThinCat )
4		simprl	|- ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> x e. ( Base ` C ) )
5		simprr	|- ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> y e. ( Base ` C ) )
6		eqid	|- ( Base ` C ) = ( Base ` C )
7		eqid	|- ( Hom ` C ) = ( Hom ` C )
8	3 4 5 6 7	thincmo	|- ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> E* f f e. ( x ( Hom ` C ) y ) )
9		eqid	|- ( Hom ` D ) = ( Hom ` D )
10	2	adantr	|- ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> F ( C Func D ) G )
11	6 7 9 10 4 5	funcf2	|- ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x G y ) : ( x ( Hom ` C ) y ) --> ( ( F ` x ) ( Hom ` D ) ( F ` y ) ) )
12		f1mo	|- ( ( E* f f e. ( x ( Hom ` C ) y ) /\ ( x G y ) : ( x ( Hom ` C ) y ) --> ( ( F ` x ) ( Hom ` D ) ( F ` y ) ) ) -> ( x G y ) : ( x ( Hom ` C ) y ) -1-1-> ( ( F ` x ) ( Hom ` D ) ( F ` y ) ) )
13	8 11 12	syl2anc	|- ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x G y ) : ( x ( Hom ` C ) y ) -1-1-> ( ( F ` x ) ( Hom ` D ) ( F ` y ) ) )
14	13	ralrimivva	|- ( ph -> A. x e. ( Base ` C ) A. y e. ( Base ` C ) ( x G y ) : ( x ( Hom ` C ) y ) -1-1-> ( ( F ` x ) ( Hom ` D ) ( F ` y ) ) )
15	6 7 9	isfth2	|- ( F ( C Faith D ) G <-> ( F ( C Func D ) G /\ A. x e. ( Base ` C ) A. y e. ( Base ` C ) ( x G y ) : ( x ( Hom ` C ) y ) -1-1-> ( ( F ` x ) ( Hom ` D ) ( F ` y ) ) ) )
16	2 14 15	sylanbrc	|- ( ph -> F ( C Faith D ) G )