Theorem funcoppc3

Description: A functor on opposite categories yields a functor on the original categories. (Contributed by Zhi Wang, 4-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 )
	funcoppc3.f	|- ( ph -> F ( O Func P ) tpos G )
	funcoppc3.g	|- ( ph -> G Fn ( A X. B ) )
Assertion	funcoppc3	|- ( 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		funcoppc3.f	|- ( ph -> F ( O Func P ) tpos G )
6		funcoppc3.g	|- ( ph -> G Fn ( A X. B ) )
7	1 2 3 4 5	funcoppc2	|- ( ph -> F ( C Func D ) tpos tpos G )
8		fnrel	|- ( G Fn ( A X. B ) -> Rel G )
9	6 8	syl	|- ( ph -> Rel G )
10		relxp	|- Rel ( A X. B )
11	6	fndmd	|- ( ph -> dom G = ( A X. B ) )
12	11	releqd	|- ( ph -> ( Rel dom G <-> Rel ( A X. B ) ) )
13	10 12	mpbiri	|- ( ph -> Rel dom G )
14		tpostpos2	|- ( ( Rel G /\ Rel dom G ) -> tpos tpos G = G )
15	9 13 14	syl2anc	|- ( ph -> tpos tpos G = G )
16	7 15	breqtrd	|- ( ph -> F ( C Func D ) G )