Metamath Proof Explorer

Theorem fthf1

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 )
Assertion fthf1 
|- ( ph -> ( X G Y ) : ( X H Y ) -1-1-> ( ( F ` X ) J ( F ` Y ) ) )

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 1 2 3 isfth2 
 |-  ( F ( C Faith D ) G <-> ( F ( C Func D ) G /\ A. x e. B A. y e. B ( x G y ) : ( x H y ) -1-1-> ( ( F ` x ) J ( F ` y ) ) ) )
8 7 simprbi 
 |-  ( F ( C Faith D ) G -> A. x e. B A. y e. B ( x G y ) : ( x H y ) -1-1-> ( ( F ` x ) J ( F ` y ) ) )
9 4 8 syl 
 |-  ( ph -> A. x e. B A. y e. B ( x G y ) : ( x H y ) -1-1-> ( ( F ` x ) J ( F ` y ) ) )
10 6 adantr 
 |-  ( ( ph /\ x = X ) -> Y e. B )
11 simplr 
 |-  ( ( ( ph /\ x = X ) /\ y = Y ) -> x = X )
12 simpr 
 |-  ( ( ( ph /\ x = X ) /\ y = Y ) -> y = Y )
13 11 12 oveq12d 
 |-  ( ( ( ph /\ x = X ) /\ y = Y ) -> ( x G y ) = ( X G Y ) )
14 11 12 oveq12d 
 |-  ( ( ( ph /\ x = X ) /\ y = Y ) -> ( x H y ) = ( X H Y ) )
15 11 fveq2d 
 |-  ( ( ( ph /\ x = X ) /\ y = Y ) -> ( F ` x ) = ( F ` X ) )
16 12 fveq2d 
 |-  ( ( ( ph /\ x = X ) /\ y = Y ) -> ( F ` y ) = ( F ` Y ) )
17 15 16 oveq12d 
 |-  ( ( ( ph /\ x = X ) /\ y = Y ) -> ( ( F ` x ) J ( F ` y ) ) = ( ( F ` X ) J ( F ` Y ) ) )
18 13 14 17 f1eq123d 
 |-  ( ( ( ph /\ x = X ) /\ y = Y ) -> ( ( x G y ) : ( x H y ) -1-1-> ( ( F ` x ) J ( F ` y ) ) <-> ( X G Y ) : ( X H Y ) -1-1-> ( ( F ` X ) J ( F ` Y ) ) ) )
19 10 18 rspcdv 
 |-  ( ( ph /\ x = X ) -> ( A. y e. B ( x G y ) : ( x H y ) -1-1-> ( ( F ` x ) J ( F ` y ) ) -> ( X G Y ) : ( X H Y ) -1-1-> ( ( F ` X ) J ( F ` Y ) ) ) )
20 5 19 rspcimdv 
 |-  ( ph -> ( A. x e. B A. y e. B ( x G y ) : ( x H y ) -1-1-> ( ( F ` x ) J ( F ` y ) ) -> ( X G Y ) : ( X H Y ) -1-1-> ( ( F ` X ) J ( F ` Y ) ) ) )
21 9 20 mpd 
 |-  ( ph -> ( X G Y ) : ( X H Y ) -1-1-> ( ( F ` X ) J ( F ` Y ) ) )