Metamath Proof Explorer

Theorem isffth2

Description: A fully faithful functor is a functor which is bijective on hom-sets. (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 )
Assertion isffth2 
|- ( F ( ( C Full D ) i^i ( 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-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 1 3 2 isfull2 
 |-  ( F ( C Full D ) G <-> ( F ( C Func D ) G /\ A. x e. B A. y e. B ( x G y ) : ( x H y ) -onto-> ( ( F ` x ) J ( F ` y ) ) ) )
5 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 ) ) ) )
6 4 5 anbi12i 
 |-  ( ( F ( C Full D ) G /\ F ( C Faith D ) G ) <-> ( ( F ( C Func D ) G /\ A. x e. B A. y e. B ( x G y ) : ( x H y ) -onto-> ( ( F ` x ) J ( F ` y ) ) ) /\ ( 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 ) ) ) ) )
7 brin 
 |-  ( F ( ( C Full D ) i^i ( C Faith D ) ) G <-> ( F ( C Full D ) G /\ F ( C Faith D ) G ) )
8 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 ) ) ) )
9 8 biancomi 
 |-  ( ( x G y ) : ( x H y ) -1-1-onto-> ( ( F ` x ) J ( F ` y ) ) <-> ( ( x G y ) : ( x H y ) -onto-> ( ( F ` x ) J ( F ` y ) ) /\ ( x G y ) : ( x H y ) -1-1-> ( ( F ` x ) J ( F ` y ) ) ) )
10 9 2ralbii 
 |-  ( A. x e. B A. y e. B ( x G y ) : ( x H y ) -1-1-onto-> ( ( F ` x ) J ( F ` y ) ) <-> A. x e. B A. y e. B ( ( x G y ) : ( x H y ) -onto-> ( ( F ` x ) J ( F ` y ) ) /\ ( x G y ) : ( x H y ) -1-1-> ( ( F ` x ) J ( F ` y ) ) ) )
11 r19.26-2 
 |-  ( A. x e. B A. y e. B ( ( x G y ) : ( x H y ) -onto-> ( ( F ` x ) J ( F ` y ) ) /\ ( x G y ) : ( x H y ) -1-1-> ( ( F ` x ) J ( F ` y ) ) ) <-> ( A. x e. B A. y e. B ( x G y ) : ( x H y ) -onto-> ( ( F ` x ) J ( F ` y ) ) /\ A. x e. B A. y e. B ( x G y ) : ( x H y ) -1-1-> ( ( F ` x ) J ( F ` y ) ) ) )
12 10 11 bitri 
 |-  ( A. x e. B A. y e. B ( x G y ) : ( x H y ) -1-1-onto-> ( ( F ` x ) J ( F ` y ) ) <-> ( A. x e. B A. y e. B ( x G y ) : ( x H y ) -onto-> ( ( F ` x ) J ( F ` y ) ) /\ A. x e. B A. y e. B ( x G y ) : ( x H y ) -1-1-> ( ( F ` x ) J ( F ` y ) ) ) )
13 12 anbi2i 
 |-  ( ( F ( C Func D ) G /\ A. x e. B A. y e. B ( x G y ) : ( x H y ) -1-1-onto-> ( ( F ` x ) J ( F ` y ) ) ) <-> ( F ( C Func D ) G /\ ( A. x e. B A. y e. B ( x G y ) : ( x H y ) -onto-> ( ( F ` x ) J ( F ` y ) ) /\ A. x e. B A. y e. B ( x G y ) : ( x H y ) -1-1-> ( ( F ` x ) J ( F ` y ) ) ) ) )
14 anandi 
 |-  ( ( F ( C Func D ) G /\ ( A. x e. B A. y e. B ( x G y ) : ( x H y ) -onto-> ( ( F ` x ) J ( F ` y ) ) /\ A. x e. B A. y e. B ( x G y ) : ( x H y ) -1-1-> ( ( F ` x ) J ( F ` y ) ) ) ) <-> ( ( F ( C Func D ) G /\ A. x e. B A. y e. B ( x G y ) : ( x H y ) -onto-> ( ( F ` x ) J ( F ` y ) ) ) /\ ( 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 ) ) ) ) )
15 13 14 bitri 
 |-  ( ( F ( C Func D ) G /\ A. x e. B A. y e. B ( x G y ) : ( x H y ) -1-1-onto-> ( ( F ` x ) J ( F ` y ) ) ) <-> ( ( F ( C Func D ) G /\ A. x e. B A. y e. B ( x G y ) : ( x H y ) -onto-> ( ( F ` x ) J ( F ` y ) ) ) /\ ( 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 ) ) ) ) )
16 6 7 15 3bitr4i 
 |-  ( F ( ( C Full D ) i^i ( 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-onto-> ( ( F ` x ) J ( F ` y ) ) ) )