Metamath Proof Explorer

Theorem fthoppc

Description: The opposite functor of a faithful functor is also faithful. Proposition 3.43(c) in Adamek p. 39. (Contributed by Mario Carneiro, 27-Jan-2017)

Ref Expression
Hypotheses fulloppc.o 
|- O = ( oppCat ` C )
fulloppc.p 
|- P = ( oppCat ` D )
fthoppc.f 
|- ( ph -> F ( C Faith D ) G )
Assertion fthoppc 
|- ( ph -> F ( O Faith P ) tpos G )

Proof

Step Hyp Ref Expression
1 fulloppc.o 
 |-  O = ( oppCat ` C )
2 fulloppc.p 
 |-  P = ( oppCat ` D )
3 fthoppc.f 
 |-  ( ph -> F ( C Faith D ) G )
4 fthfunc 
 |-  ( C Faith D ) C_ ( C Func D )
5 4 ssbri 
 |-  ( F ( C Faith D ) G -> F ( C Func D ) G )
6 3 5 syl 
 |-  ( ph -> F ( C Func D ) G )
7 1 2 6 funcoppc 
 |-  ( ph -> F ( O Func P ) tpos G )
8 eqid 
 |-  ( Base ` C ) = ( Base ` C )
9 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
10 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
11 3 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> F ( C Faith D ) G )
12 simprr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> y e. ( Base ` C ) )
13 simprl 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> x e. ( Base ` C ) )
14 8 9 10 11 12 13 fthf1 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( y G x ) : ( y ( Hom ` C ) x ) -1-1-> ( ( F ` y ) ( Hom ` D ) ( F ` x ) ) )
15 df-f1 
 |-  ( ( y G x ) : ( y ( Hom ` C ) x ) -1-1-> ( ( F ` y ) ( Hom ` D ) ( F ` x ) ) <-> ( ( y G x ) : ( y ( Hom ` C ) x ) --> ( ( F ` y ) ( Hom ` D ) ( F ` x ) ) /\ Fun `' ( y G x ) ) )
16 15 simprbi 
 |-  ( ( y G x ) : ( y ( Hom ` C ) x ) -1-1-> ( ( F ` y ) ( Hom ` D ) ( F ` x ) ) -> Fun `' ( y G x ) )
17 14 16 syl 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> Fun `' ( y G x ) )
18 ovtpos 
 |-  ( x tpos G y ) = ( y G x )
19 18 cnveqi 
 |-  `' ( x tpos G y ) = `' ( y G x )
20 19 funeqi 
 |-  ( Fun `' ( x tpos G y ) <-> Fun `' ( y G x ) )
21 17 20 sylibr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> Fun `' ( x tpos G y ) )
22 21 ralrimivva 
 |-  ( ph -> A. x e. ( Base ` C ) A. y e. ( Base ` C ) Fun `' ( x tpos G y ) )
23 1 8 oppcbas 
 |-  ( Base ` C ) = ( Base ` O )
24 23 isfth 
 |-  ( F ( O Faith P ) tpos G <-> ( F ( O Func P ) tpos G /\ A. x e. ( Base ` C ) A. y e. ( Base ` C ) Fun `' ( x tpos G y ) ) )
25 7 22 24 sylanbrc 
 |-  ( ph -> F ( O Faith P ) tpos G )