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

Metamath Proof Explorer

Theorem ffthf1o

Description: The morphism map of a fully faithful functor is a bijection. (Contributed by Mario Carneiro, 29-Jan-2017)

Ref Expression
Hypotheses isfth.b 
|- B = ( Base ` C )
isfth.h 
|- H = ( Hom ` C )
isfth.j 
|- J = ( Hom ` D )
ffthf1o.f 
|- ( ph -> F ( ( C Full D ) i^i ( C Faith D ) ) G )
ffthf1o.x 
|- ( ph -> X e. B )
ffthf1o.y 
|- ( ph -> Y e. B )
Assertion ffthf1o 
|- ( ph -> ( X G Y ) : ( X H Y ) -1-1-onto-> ( ( 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 ffthf1o.f 
 |-  ( ph -> F ( ( C Full D ) i^i ( C Faith D ) ) G )
5 ffthf1o.x 
 |-  ( ph -> X e. B )
6 ffthf1o.y 
 |-  ( ph -> Y e. B )
7 brin 
 |-  ( F ( ( C Full D ) i^i ( C Faith D ) ) G <-> ( F ( C Full D ) G /\ F ( C Faith D ) G ) )
8 4 7 sylib 
 |-  ( ph -> ( F ( C Full D ) G /\ F ( C Faith D ) G ) )
9 8 simprd 
 |-  ( ph -> F ( C Faith D ) G )
10 1 2 3 9 5 6 fthf1 
 |-  ( ph -> ( X G Y ) : ( X H Y ) -1-1-> ( ( F ` X ) J ( F ` Y ) ) )
11 8 simpld 
 |-  ( ph -> F ( C Full D ) G )
12 1 3 2 11 5 6 fullfo 
 |-  ( ph -> ( X G Y ) : ( X H Y ) -onto-> ( ( F ` X ) J ( F ` Y ) ) )
13 df-f1o 
 |-  ( ( X G Y ) : ( X H Y ) -1-1-onto-> ( ( F ` X ) J ( F ` Y ) ) <-> ( ( X G Y ) : ( X H Y ) -1-1-> ( ( F ` X ) J ( F ` Y ) ) /\ ( X G Y ) : ( X H Y ) -onto-> ( ( F ` X ) J ( F ` Y ) ) ) )
14 10 12 13 sylanbrc 
 |-  ( ph -> ( X G Y ) : ( X H Y ) -1-1-onto-> ( ( F ` X ) J ( F ` Y ) ) )