Metamath Proof Explorer

Theorem isfull2

Description: Equivalent condition for a full functor. (Contributed by Mario Carneiro, 27-Jan-2017)

Ref Expression
Hypotheses isfull.b 
|- B = ( Base ` C )
isfull.j 
|- J = ( Hom ` D )
isfull.h 
|- H = ( Hom ` C )
Assertion 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 ) ) ) )

Proof

Step Hyp Ref Expression
1 isfull.b 
 |-  B = ( Base ` C )
2 isfull.j 
 |-  J = ( Hom ` D )
3 isfull.h 
 |-  H = ( Hom ` C )
4 1 2 isfull 
 |-  ( F ( C Full D ) G <-> ( F ( C Func D ) G /\ A. x e. B A. y e. B ran ( x G y ) = ( ( F ` x ) J ( F ` y ) ) ) )
5 simpll 
 |-  ( ( ( F ( C Func D ) G /\ x e. B ) /\ y e. B ) -> F ( C Func D ) G )
6 simplr 
 |-  ( ( ( F ( C Func D ) G /\ x e. B ) /\ y e. B ) -> x e. B )
7 simpr 
 |-  ( ( ( F ( C Func D ) G /\ x e. B ) /\ y e. B ) -> y e. B )
8 1 3 2 5 6 7 funcf2 
 |-  ( ( ( F ( C Func D ) G /\ x e. B ) /\ y e. B ) -> ( x G y ) : ( x H y ) --> ( ( F ` x ) J ( F ` y ) ) )
9 ffn 
 |-  ( ( x G y ) : ( x H y ) --> ( ( F ` x ) J ( F ` y ) ) -> ( x G y ) Fn ( x H y ) )
10 df-fo 
 |-  ( ( x G y ) : ( x H y ) -onto-> ( ( F ` x ) J ( F ` y ) ) <-> ( ( x G y ) Fn ( x H y ) /\ ran ( x G y ) = ( ( F ` x ) J ( F ` y ) ) ) )
11 10 baib 
 |-  ( ( x G y ) Fn ( x H y ) -> ( ( x G y ) : ( x H y ) -onto-> ( ( F ` x ) J ( F ` y ) ) <-> ran ( x G y ) = ( ( F ` x ) J ( F ` y ) ) ) )
12 8 9 11 3syl 
 |-  ( ( ( F ( C Func D ) G /\ x e. B ) /\ y e. B ) -> ( ( x G y ) : ( x H y ) -onto-> ( ( F ` x ) J ( F ` y ) ) <-> ran ( x G y ) = ( ( F ` x ) J ( F ` y ) ) ) )
13 12 ralbidva 
 |-  ( ( F ( C Func D ) G /\ x e. B ) -> ( A. y e. B ( x G y ) : ( x H y ) -onto-> ( ( F ` x ) J ( F ` y ) ) <-> A. y e. B ran ( x G y ) = ( ( F ` x ) J ( F ` y ) ) ) )
14 13 ralbidva 
 |-  ( 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 ran ( x G y ) = ( ( F ` x ) J ( F ` y ) ) ) )
15 14 pm5.32i 
 |-  ( ( 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 ran ( x G y ) = ( ( F ` x ) J ( F ` y ) ) ) )
16 4 15 bitr4i 
 |-  ( 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 ) ) ) )