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

Metamath Proof Explorer

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 ) )