Metamath Proof Explorer

Theorem isfull

Description: Value of the set of full functors between two categories. (Contributed by Mario Carneiro, 27-Jan-2017)

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

Proof

Step Hyp Ref Expression
1 isfull.b 
 |-  B = ( Base ` C )
2 isfull.j 
 |-  J = ( Hom ` D )
3 fullfunc 
 |-  ( C Full D ) C_ ( C Func D )
4 3 ssbri 
 |-  ( F ( C Full D ) G -> F ( C Func D ) G )
5 df-br 
 |-  ( F ( C Func D ) G <-> <. F , G >. e. ( C Func D ) )
6 funcrcl 
 |-  ( <. F , G >. e. ( C Func D ) -> ( C e. Cat /\ D e. Cat ) )
7 5 6 sylbi 
 |-  ( F ( C Func D ) G -> ( C e. Cat /\ D e. Cat ) )
8 oveq12 
 |-  ( ( c = C /\ d = D ) -> ( c Func d ) = ( C Func D ) )
9 8 breqd 
 |-  ( ( c = C /\ d = D ) -> ( f ( c Func d ) g <-> f ( C Func D ) g ) )
10 simpl 
 |-  ( ( c = C /\ d = D ) -> c = C )
11 10 fveq2d 
 |-  ( ( c = C /\ d = D ) -> ( Base ` c ) = ( Base ` C ) )
12 11 1 eqtr4di 
 |-  ( ( c = C /\ d = D ) -> ( Base ` c ) = B )
13 simpr 
 |-  ( ( c = C /\ d = D ) -> d = D )
14 13 fveq2d 
 |-  ( ( c = C /\ d = D ) -> ( Hom ` d ) = ( Hom ` D ) )
15 14 2 eqtr4di 
 |-  ( ( c = C /\ d = D ) -> ( Hom ` d ) = J )
16 15 oveqd 
 |-  ( ( c = C /\ d = D ) -> ( ( f ` x ) ( Hom ` d ) ( f ` y ) ) = ( ( f ` x ) J ( f ` y ) ) )
17 16 eqeq2d 
 |-  ( ( c = C /\ d = D ) -> ( ran ( x g y ) = ( ( f ` x ) ( Hom ` d ) ( f ` y ) ) <-> ran ( x g y ) = ( ( f ` x ) J ( f ` y ) ) ) )
18 12 17 raleqbidv 
 |-  ( ( c = C /\ d = D ) -> ( A. y e. ( Base ` c ) ran ( x g y ) = ( ( f ` x ) ( Hom ` d ) ( f ` y ) ) <-> A. y e. B ran ( x g y ) = ( ( f ` x ) J ( f ` y ) ) ) )
19 12 18 raleqbidv 
 |-  ( ( c = C /\ d = D ) -> ( A. x e. ( Base ` c ) A. y e. ( Base ` c ) ran ( x g y ) = ( ( f ` x ) ( Hom ` d ) ( f ` y ) ) <-> A. x e. B A. y e. B ran ( x g y ) = ( ( f ` x ) J ( f ` y ) ) ) )
20 9 19 anbi12d 
 |-  ( ( c = C /\ d = D ) -> ( ( f ( c Func d ) g /\ A. x e. ( Base ` c ) A. y e. ( Base ` c ) ran ( x g y ) = ( ( f ` x ) ( Hom ` d ) ( f ` y ) ) ) <-> ( f ( C Func D ) g /\ A. x e. B A. y e. B ran ( x g y ) = ( ( f ` x ) J ( f ` y ) ) ) ) )
21 20 opabbidv 
 |-  ( ( c = C /\ d = D ) -> { <. f , g >. | ( f ( c Func d ) g /\ A. x e. ( Base ` c ) A. y e. ( Base ` c ) ran ( x g y ) = ( ( f ` x ) ( Hom ` d ) ( f ` y ) ) ) } = { <. f , g >. | ( f ( C Func D ) g /\ A. x e. B A. y e. B ran ( x g y ) = ( ( f ` x ) J ( f ` y ) ) ) } )
22 df-full 
 |-  Full = ( c e. Cat , d e. Cat |-> { <. f , g >. | ( f ( c Func d ) g /\ A. x e. ( Base ` c ) A. y e. ( Base ` c ) ran ( x g y ) = ( ( f ` x ) ( Hom ` d ) ( f ` y ) ) ) } )
23 ovex 
 |-  ( C Func D ) e. _V
24 simpl 
 |-  ( ( f ( C Func D ) g /\ A. x e. B A. y e. B ran ( x g y ) = ( ( f ` x ) J ( f ` y ) ) ) -> f ( C Func D ) g )
25 24 ssopab2i 
 |-  { <. f , g >. | ( f ( C Func D ) g /\ A. x e. B A. y e. B ran ( x g y ) = ( ( f ` x ) J ( f ` y ) ) ) } C_ { <. f , g >. | f ( C Func D ) g }
26 opabss 
 |-  { <. f , g >. | f ( C Func D ) g } C_ ( C Func D )
27 25 26 sstri 
 |-  { <. f , g >. | ( f ( C Func D ) g /\ A. x e. B A. y e. B ran ( x g y ) = ( ( f ` x ) J ( f ` y ) ) ) } C_ ( C Func D )
28 23 27 ssexi 
 |-  { <. f , g >. | ( f ( C Func D ) g /\ A. x e. B A. y e. B ran ( x g y ) = ( ( f ` x ) J ( f ` y ) ) ) } e. _V
29 21 22 28 ovmpoa 
 |-  ( ( C e. Cat /\ D e. Cat ) -> ( C Full D ) = { <. f , g >. | ( f ( C Func D ) g /\ A. x e. B A. y e. B ran ( x g y ) = ( ( f ` x ) J ( f ` y ) ) ) } )
30 7 29 syl 
 |-  ( F ( C Func D ) G -> ( C Full D ) = { <. f , g >. | ( f ( C Func D ) g /\ A. x e. B A. y e. B ran ( x g y ) = ( ( f ` x ) J ( f ` y ) ) ) } )
31 30 breqd 
 |-  ( F ( C Func D ) G -> ( F ( C Full D ) G <-> F { <. f , g >. | ( f ( C Func D ) g /\ A. x e. B A. y e. B ran ( x g y ) = ( ( f ` x ) J ( f ` y ) ) ) } G ) )
32 relfunc 
 |-  Rel ( C Func D )
33 32 brrelex12i 
 |-  ( F ( C Func D ) G -> ( F e. _V /\ G e. _V ) )
34 breq12 
 |-  ( ( f = F /\ g = G ) -> ( f ( C Func D ) g <-> F ( C Func D ) G ) )
35 simpr 
 |-  ( ( f = F /\ g = G ) -> g = G )
36 35 oveqd 
 |-  ( ( f = F /\ g = G ) -> ( x g y ) = ( x G y ) )
37 36 rneqd 
 |-  ( ( f = F /\ g = G ) -> ran ( x g y ) = ran ( x G y ) )
38 simpl 
 |-  ( ( f = F /\ g = G ) -> f = F )
39 38 fveq1d 
 |-  ( ( f = F /\ g = G ) -> ( f ` x ) = ( F ` x ) )
40 38 fveq1d 
 |-  ( ( f = F /\ g = G ) -> ( f ` y ) = ( F ` y ) )
41 39 40 oveq12d 
 |-  ( ( f = F /\ g = G ) -> ( ( f ` x ) J ( f ` y ) ) = ( ( F ` x ) J ( F ` y ) ) )
42 37 41 eqeq12d 
 |-  ( ( f = F /\ g = G ) -> ( ran ( x g y ) = ( ( f ` x ) J ( f ` y ) ) <-> ran ( x G y ) = ( ( F ` x ) J ( F ` y ) ) ) )
43 42 2ralbidv 
 |-  ( ( f = F /\ g = G ) -> ( A. x e. B A. y e. B ran ( x g y ) = ( ( f ` x ) J ( f ` y ) ) <-> A. x e. B A. y e. B ran ( x G y ) = ( ( F ` x ) J ( F ` y ) ) ) )
44 34 43 anbi12d 
 |-  ( ( f = F /\ g = G ) -> ( ( f ( C Func D ) g /\ A. x e. B A. y e. B ran ( x g y ) = ( ( 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 ) ) ) ) )
45 eqid 
 |-  { <. f , g >. | ( f ( C Func D ) g /\ A. x e. B A. y e. B ran ( x g y ) = ( ( f ` x ) J ( f ` y ) ) ) } = { <. f , g >. | ( f ( C Func D ) g /\ A. x e. B A. y e. B ran ( x g y ) = ( ( f ` x ) J ( f ` y ) ) ) }
46 44 45 brabga 
 |-  ( ( F e. _V /\ G e. _V ) -> ( F { <. f , g >. | ( f ( C Func D ) g /\ A. x e. B A. y e. B ran ( x g y ) = ( ( f ` x ) J ( f ` y ) ) ) } G <-> ( F ( C Func D ) G /\ A. x e. B A. y e. B ran ( x G y ) = ( ( F ` x ) J ( F ` y ) ) ) ) )
47 33 46 syl 
 |-  ( F ( C Func D ) G -> ( F { <. f , g >. | ( f ( C Func D ) g /\ A. x e. B A. y e. B ran ( x g y ) = ( ( f ` x ) J ( f ` y ) ) ) } G <-> ( F ( C Func D ) G /\ A. x e. B A. y e. B ran ( x G y ) = ( ( F ` x ) J ( F ` y ) ) ) ) )
48 31 47 bitrd 
 |-  ( F ( C Func D ) G -> ( 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 ) ) ) ) )
49 48 bianabs 
 |-  ( F ( C Func D ) G -> ( F ( C Full D ) G <-> A. x e. B A. y e. B ran ( x G y ) = ( ( F ` x ) J ( F ` y ) ) ) )
50 4 49 biadanii 
 |-  ( 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 ) ) ) )