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 ) )