This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fthoppf

Description: The opposite functor of a faithful functor is also faithful. Proposition 3.43(c) in Adamek p. 39. (Contributed by Zhi Wang, 26-Nov-2025)

Ref Expression
Hypotheses fulloppf.o 
|- O = ( oppCat ` C )
fulloppf.p 
|- P = ( oppCat ` D )
fthoppf.f 
|- ( ph -> F e. ( C Faith D ) )
Assertion fthoppf 
|- ( ph -> ( oppFunc ` F ) e. ( O Faith P ) )

Proof

Step Hyp Ref Expression
1 fulloppf.o 
 |-  O = ( oppCat ` C )
2 fulloppf.p 
 |-  P = ( oppCat ` D )
3 fthoppf.f 
 |-  ( ph -> F e. ( C Faith D ) )
4 fthfunc 
 |-  ( C Faith D ) C_ ( C Func D )
5 4 sseli 
 |-  ( F e. ( C Faith D ) -> F e. ( C Func D ) )
6 oppfval2 
 |-  ( F e. ( C Func D ) -> ( oppFunc ` F ) = <. ( 1st ` F ) , tpos ( 2nd ` F ) >. )
7 3 5 6 3syl 
 |-  ( ph -> ( oppFunc ` F ) = <. ( 1st ` F ) , tpos ( 2nd ` F ) >. )
8 relfth 
 |-  Rel ( C Faith D )
9 1st2ndbr 
 |-  ( ( Rel ( C Faith D ) /\ F e. ( C Faith D ) ) -> ( 1st ` F ) ( C Faith D ) ( 2nd ` F ) )
10 8 3 9 sylancr 
 |-  ( ph -> ( 1st ` F ) ( C Faith D ) ( 2nd ` F ) )
11 1 2 10 fthoppc 
 |-  ( ph -> ( 1st ` F ) ( O Faith P ) tpos ( 2nd ` F ) )
12 df-br 
 |-  ( ( 1st ` F ) ( O Faith P ) tpos ( 2nd ` F ) <-> <. ( 1st ` F ) , tpos ( 2nd ` F ) >. e. ( O Faith P ) )
13 11 12 sylib 
 |-  ( ph -> <. ( 1st ` F ) , tpos ( 2nd ` F ) >. e. ( O Faith P ) )
14 7 13 eqeltrd 
 |-  ( ph -> ( oppFunc ` F ) e. ( O Faith P ) )