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

Metamath Proof Explorer

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 )