Theorem oppfoppc2

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

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

Proof

Step	Hyp	Ref	Expression
1		oppfoppc.o	|- O = ( oppCat ` C )
2		oppfoppc.p	|- P = ( oppCat ` D )
3		oppfoppc2.f	|- ( ph -> F e. ( C Func D ) )
4		relfunc	|- Rel ( C Func D )
5		1st2nd	|- ( ( Rel ( C Func D ) /\ F e. ( C Func D ) ) -> F = <. ( 1st ` F ) , ( 2nd ` F ) >. )
6	4 3 5	sylancr	|- ( ph -> F = <. ( 1st ` F ) , ( 2nd ` F ) >. )
7	6	fveq2d	|- ( ph -> ( oppFunc ` F ) = ( oppFunc ` <. ( 1st ` F ) , ( 2nd ` F ) >. ) )
8		df-ov	|- ( ( 1st ` F ) oppFunc ( 2nd ` F ) ) = ( oppFunc ` <. ( 1st ` F ) , ( 2nd ` F ) >. )
9	7 8	eqtr4di	|- ( ph -> ( oppFunc ` F ) = ( ( 1st ` F ) oppFunc ( 2nd ` F ) ) )
10	3	func1st2nd	|- ( ph -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
11	1 2 10	oppfoppc	|- ( ph -> ( ( 1st ` F ) oppFunc ( 2nd ` F ) ) e. ( O Func P ) )
12	9 11	eqeltrd	|- ( ph -> ( oppFunc ` F ) e. ( O Func P ) )