Theorem funcoppc4

Description: A functor on opposite categories yields a functor on the original categories. (Contributed by Zhi Wang, 14-Nov-2025)

	Ref	Expression
Hypotheses	funcoppc2.o	|- O = ( oppCat ` C )
	funcoppc2.p	|- P = ( oppCat ` D )
	funcoppc2.c	|- ( ph -> C e. V )
	funcoppc2.d	|- ( ph -> D e. W )
	funcoppc4.f	|- ( ph -> ( F oppFunc G ) e. ( O Func P ) )
Assertion	funcoppc4	|- ( ph -> F ( C Func D ) G )

Proof

Step	Hyp	Ref	Expression
1		funcoppc2.o	|- O = ( oppCat ` C )
2		funcoppc2.p	|- P = ( oppCat ` D )
3		funcoppc2.c	|- ( ph -> C e. V )
4		funcoppc2.d	|- ( ph -> D e. W )
5		funcoppc4.f	|- ( ph -> ( F oppFunc G ) e. ( O Func P ) )
6	5	func1st2nd	|- ( ph -> ( 1st ` ( F oppFunc G ) ) ( O Func P ) ( 2nd ` ( F oppFunc G ) ) )
7	1 2 3 4 6	funcoppc2	|- ( ph -> ( 1st ` ( F oppFunc G ) ) ( C Func D ) tpos ( 2nd ` ( F oppFunc G ) ) )
8		relfunc	|- Rel ( O Func P )
9		df-ov	|- ( F oppFunc G ) = ( oppFunc ` <. F , G >. )
10		eqidd	|- ( ph -> <. F , G >. = <. F , G >. )
11	5 8 9 10	oppf1st2nd	|- ( ph -> ( ( F oppFunc G ) e. ( _V X. _V ) /\ ( ( 1st ` ( F oppFunc G ) ) = F /\ ( 2nd ` ( F oppFunc G ) ) = tpos G ) ) )
12	11	simprld	|- ( ph -> ( 1st ` ( F oppFunc G ) ) = F )
13	11	simprrd	|- ( ph -> ( 2nd ` ( F oppFunc G ) ) = tpos G )
14	13	tposeqd	|- ( ph -> tpos ( 2nd ` ( F oppFunc G ) ) = tpos tpos G )
15	5 8 9 10	oppfrcl3	|- ( ph -> ( Rel G /\ Rel dom G ) )
16		tpostpos2	|- ( ( Rel G /\ Rel dom G ) -> tpos tpos G = G )
17	15 16	syl	|- ( ph -> tpos tpos G = G )
18	14 17	eqtrd	|- ( ph -> tpos ( 2nd ` ( F oppFunc G ) ) = G )
19	7 12 18	3brtr3d	|- ( ph -> F ( C Func D ) G )