Theorem oppfoppc

Description: The opposite functor is a functor on opposite categories. (Contributed by Zhi Wang, 4-Nov-2025)

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

Proof

Step	Hyp	Ref	Expression
1		oppfoppc.o	|- O = ( oppCat ` C )
2		oppfoppc.p	|- P = ( oppCat ` D )
3		oppfoppc.f	|- ( ph -> F ( C Func D ) G )
4		oppfval	|- ( F ( C Func D ) G -> ( F oppFunc G ) = <. F , tpos G >. )
5	3 4	syl	|- ( ph -> ( F oppFunc G ) = <. F , tpos G >. )
6	1 2 3	funcoppc	|- ( ph -> F ( O Func P ) tpos G )
7		df-br	|- ( F ( O Func P ) tpos G <-> <. F , tpos G >. e. ( O Func P ) )
8	6 7	sylib	|- ( ph -> <. F , tpos G >. e. ( O Func P ) )
9	5 8	eqeltrd	|- ( ph -> ( F oppFunc G ) e. ( O Func P ) )