Metamath Proof Explorer

Theorem isfth

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

Ref Expression
Hypothesis isfth.b 
|- B = ( Base ` C )
Assertion isfth 
|- ( F ( C Faith D ) G <-> ( F ( C Func D ) G /\ A. x e. B A. y e. B Fun `' ( x G y ) ) )

Proof

Step Hyp Ref Expression
1 isfth.b 
 |-  B = ( Base ` C )
2 fthfunc 
 |-  ( C Faith D ) C_ ( C Func D )
3 2 ssbri 
 |-  ( F ( C Faith D ) G -> F ( C Func D ) G )
4 df-br 
 |-  ( F ( C Func D ) G <-> <. F , G >. e. ( C Func D ) )
5 funcrcl 
 |-  ( <. F , G >. e. ( C Func D ) -> ( C e. Cat /\ D e. Cat ) )
6 4 5 sylbi 
 |-  ( F ( C Func D ) G -> ( C e. Cat /\ D e. Cat ) )
7 oveq12 
 |-  ( ( c = C /\ d = D ) -> ( c Func d ) = ( C Func D ) )
8 7 breqd 
 |-  ( ( c = C /\ d = D ) -> ( f ( c Func d ) g <-> f ( C Func D ) g ) )
9 simpl 
 |-  ( ( c = C /\ d = D ) -> c = C )
10 9 fveq2d 
 |-  ( ( c = C /\ d = D ) -> ( Base ` c ) = ( Base ` C ) )
11 10 1 eqtr4di 
 |-  ( ( c = C /\ d = D ) -> ( Base ` c ) = B )
12 11 raleqdv 
 |-  ( ( c = C /\ d = D ) -> ( A. y e. ( Base ` c ) Fun `' ( x g y ) <-> A. y e. B Fun `' ( x g y ) ) )
13 11 12 raleqbidv 
 |-  ( ( c = C /\ d = D ) -> ( A. x e. ( Base ` c ) A. y e. ( Base ` c ) Fun `' ( x g y ) <-> A. x e. B A. y e. B Fun `' ( x g y ) ) )
14 8 13 anbi12d 
 |-  ( ( c = C /\ d = D ) -> ( ( f ( c Func d ) g /\ A. x e. ( Base ` c ) A. y e. ( Base ` c ) Fun `' ( x g y ) ) <-> ( f ( C Func D ) g /\ A. x e. B A. y e. B Fun `' ( x g y ) ) ) )
15 14 opabbidv 
 |-  ( ( c = C /\ d = D ) -> { <. f , g >. | ( f ( c Func d ) g /\ A. x e. ( Base ` c ) A. y e. ( Base ` c ) Fun `' ( x g y ) ) } = { <. f , g >. | ( f ( C Func D ) g /\ A. x e. B A. y e. B Fun `' ( x g y ) ) } )
16 df-fth 
 |-  Faith = ( c e. Cat , d e. Cat |-> { <. f , g >. | ( f ( c Func d ) g /\ A. x e. ( Base ` c ) A. y e. ( Base ` c ) Fun `' ( x g y ) ) } )
17 ovex 
 |-  ( C Func D ) e. _V
18 simpl 
 |-  ( ( f ( C Func D ) g /\ A. x e. B A. y e. B Fun `' ( x g y ) ) -> f ( C Func D ) g )
19 18 ssopab2i 
 |-  { <. f , g >. | ( f ( C Func D ) g /\ A. x e. B A. y e. B Fun `' ( x g y ) ) } C_ { <. f , g >. | f ( C Func D ) g }
20 opabss 
 |-  { <. f , g >. | f ( C Func D ) g } C_ ( C Func D )
21 19 20 sstri 
 |-  { <. f , g >. | ( f ( C Func D ) g /\ A. x e. B A. y e. B Fun `' ( x g y ) ) } C_ ( C Func D )
22 17 21 ssexi 
 |-  { <. f , g >. | ( f ( C Func D ) g /\ A. x e. B A. y e. B Fun `' ( x g y ) ) } e. _V
23 15 16 22 ovmpoa 
 |-  ( ( C e. Cat /\ D e. Cat ) -> ( C Faith D ) = { <. f , g >. | ( f ( C Func D ) g /\ A. x e. B A. y e. B Fun `' ( x g y ) ) } )
24 6 23 syl 
 |-  ( F ( C Func D ) G -> ( C Faith D ) = { <. f , g >. | ( f ( C Func D ) g /\ A. x e. B A. y e. B Fun `' ( x g y ) ) } )
25 24 breqd 
 |-  ( F ( C Func D ) G -> ( F ( C Faith D ) G <-> F { <. f , g >. | ( f ( C Func D ) g /\ A. x e. B A. y e. B Fun `' ( x g y ) ) } G ) )
26 relfunc 
 |-  Rel ( C Func D )
27 26 brrelex12i 
 |-  ( F ( C Func D ) G -> ( F e. _V /\ G e. _V ) )
28 breq12 
 |-  ( ( f = F /\ g = G ) -> ( f ( C Func D ) g <-> F ( C Func D ) G ) )
29 simpr 
 |-  ( ( f = F /\ g = G ) -> g = G )
30 29 oveqd 
 |-  ( ( f = F /\ g = G ) -> ( x g y ) = ( x G y ) )
31 30 cnveqd 
 |-  ( ( f = F /\ g = G ) -> `' ( x g y ) = `' ( x G y ) )
32 31 funeqd 
 |-  ( ( f = F /\ g = G ) -> ( Fun `' ( x g y ) <-> Fun `' ( x G y ) ) )
33 32 2ralbidv 
 |-  ( ( f = F /\ g = G ) -> ( A. x e. B A. y e. B Fun `' ( x g y ) <-> A. x e. B A. y e. B Fun `' ( x G y ) ) )
34 28 33 anbi12d 
 |-  ( ( f = F /\ g = G ) -> ( ( f ( C Func D ) g /\ A. x e. B A. y e. B Fun `' ( x g y ) ) <-> ( F ( C Func D ) G /\ A. x e. B A. y e. B Fun `' ( x G y ) ) ) )
35 eqid 
 |-  { <. f , g >. | ( f ( C Func D ) g /\ A. x e. B A. y e. B Fun `' ( x g y ) ) } = { <. f , g >. | ( f ( C Func D ) g /\ A. x e. B A. y e. B Fun `' ( x g y ) ) }
36 34 35 brabga 
 |-  ( ( F e. _V /\ G e. _V ) -> ( F { <. f , g >. | ( f ( C Func D ) g /\ A. x e. B A. y e. B Fun `' ( x g y ) ) } G <-> ( F ( C Func D ) G /\ A. x e. B A. y e. B Fun `' ( x G y ) ) ) )
37 27 36 syl 
 |-  ( F ( C Func D ) G -> ( F { <. f , g >. | ( f ( C Func D ) g /\ A. x e. B A. y e. B Fun `' ( x g y ) ) } G <-> ( F ( C Func D ) G /\ A. x e. B A. y e. B Fun `' ( x G y ) ) ) )
38 25 37 bitrd 
 |-  ( F ( C Func D ) G -> ( F ( C Faith D ) G <-> ( F ( C Func D ) G /\ A. x e. B A. y e. B Fun `' ( x G y ) ) ) )
39 38 bianabs 
 |-  ( F ( C Func D ) G -> ( F ( C Faith D ) G <-> A. x e. B A. y e. B Fun `' ( x G y ) ) )
40 3 39 biadanii 
 |-  ( F ( C Faith D ) G <-> ( F ( C Func D ) G /\ A. x e. B A. y e. B Fun `' ( x G y ) ) )