Theorem fthi

Description: The morphism map of a faithful functor is an injection. (Contributed by Mario Carneiro, 27-Jan-2017)

	Ref	Expression
Hypotheses	isfth.b	|- B = ( Base ` C )
	isfth.h	|- H = ( Hom ` C )
	isfth.j	|- J = ( Hom ` D )
	fthf1.f	|- ( ph -> F ( C Faith D ) G )
	fthf1.x	|- ( ph -> X e. B )
	fthf1.y	|- ( ph -> Y e. B )
	fthi.r	|- ( ph -> R e. ( X H Y ) )
	fthi.s	|- ( ph -> S e. ( X H Y ) )
Assertion	fthi	|- ( ph -> ( ( ( X G Y ) ` R ) = ( ( X G Y ) ` S ) <-> R = S ) )

Proof

Step	Hyp	Ref	Expression
1		isfth.b	|- B = ( Base ` C )
2		isfth.h	|- H = ( Hom ` C )
3		isfth.j	|- J = ( Hom ` D )
4		fthf1.f	|- ( ph -> F ( C Faith D ) G )
5		fthf1.x	|- ( ph -> X e. B )
6		fthf1.y	|- ( ph -> Y e. B )
7		fthi.r	|- ( ph -> R e. ( X H Y ) )
8		fthi.s	|- ( ph -> S e. ( X H Y ) )
9	1 2 3 4 5 6	fthf1	|- ( ph -> ( X G Y ) : ( X H Y ) -1-1-> ( ( F ` X ) J ( F ` Y ) ) )
10		f1fveq	|- ( ( ( X G Y ) : ( X H Y ) -1-1-> ( ( F ` X ) J ( F ` Y ) ) /\ ( R e. ( X H Y ) /\ S e. ( X H Y ) ) ) -> ( ( ( X G Y ) ` R ) = ( ( X G Y ) ` S ) <-> R = S ) )
11	9 7 8 10	syl12anc	|- ( ph -> ( ( ( X G Y ) ` R ) = ( ( X G Y ) ` S ) <-> R = S ) )