Theorem funcoppc5

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=\mathrm{oppCat}\left(C\right)$$
	funcoppc2.p	$$⊢P=\mathrm{oppCat}\left(D\right)$$
	funcoppc2.c	$$⊢\phi \to C\in V$$
	funcoppc2.d	$$⊢\phi \to D\in W$$
	funcoppc5.f	No typesetting found for |- ( ph -> ( oppFunc ` F ) e. ( O Func P ) ) with typecode |-
Assertion	funcoppc5	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$

Proof

Step	Hyp	Ref	Expression
1		funcoppc2.o	$$⊢O=\mathrm{oppCat}\left(C\right)$$
2		funcoppc2.p	$$⊢P=\mathrm{oppCat}\left(D\right)$$
3		funcoppc2.c	$$⊢\phi \to C\in V$$
4		funcoppc2.d	$$⊢\phi \to D\in W$$
5		funcoppc5.f	Could not format ( ph -> ( oppFunc ` F ) e. ( O Func P ) ) : No typesetting found for |- ( ph -> ( oppFunc ` F ) e. ( O Func P ) ) with typecode |-
6		relfunc	$$⊢\mathrm{Rel}\left(O\mathrm{Func}P\right)$$
7		eqid	Could not format ( oppFunc ` F ) = ( oppFunc ` F ) : No typesetting found for |- ( oppFunc ` F ) = ( oppFunc ` F ) with typecode |-
8	5 6 7	oppfrcl	$$⊢\phi \to F\in \left(\mathrm{V}\times \mathrm{V}\right)$$
9		1st2nd2	$$⊢F\in \left(\mathrm{V}\times \mathrm{V}\right)\to F=⟨1^{st}\left(F\right),2^{nd}\left(F\right)⟩$$
10	8 9	syl	$$⊢\phi \to F=⟨1^{st}\left(F\right),2^{nd}\left(F\right)⟩$$
11	10	fveq2d	Could not format ( ph -> ( oppFunc ` F ) = ( oppFunc ` <. ( 1st ` F ) , ( 2nd ` F ) >. ) ) : No typesetting found for |- ( ph -> ( oppFunc ` F ) = ( oppFunc ` <. ( 1st ` F ) , ( 2nd ` F ) >. ) ) with typecode |-
12		df-ov	Could not format ( ( 1st ` F ) oppFunc ( 2nd ` F ) ) = ( oppFunc ` <. ( 1st ` F ) , ( 2nd ` F ) >. ) : No typesetting found for |- ( ( 1st ` F ) oppFunc ( 2nd ` F ) ) = ( oppFunc ` <. ( 1st ` F ) , ( 2nd ` F ) >. ) with typecode |-
13	11 12	eqtr4di	Could not format ( ph -> ( oppFunc ` F ) = ( ( 1st ` F ) oppFunc ( 2nd ` F ) ) ) : No typesetting found for |- ( ph -> ( oppFunc ` F ) = ( ( 1st ` F ) oppFunc ( 2nd ` F ) ) ) with typecode |-
14	13 5	eqeltrrd	Could not format ( ph -> ( ( 1st ` F ) oppFunc ( 2nd ` F ) ) e. ( O Func P ) ) : No typesetting found for |- ( ph -> ( ( 1st ` F ) oppFunc ( 2nd ` F ) ) e. ( O Func P ) ) with typecode |-
15	1 2 3 4 14	funcoppc4	$$⊢\phi \to 1^{st}\left(F\right)\left(C\mathrm{Func}D\right)2^{nd}\left(F\right)$$
16		df-br	$$⊢1^{st}\left(F\right)\left(C\mathrm{Func}D\right)2^{nd}\left(F\right)\leftrightarrow ⟨1^{st}\left(F\right),2^{nd}\left(F\right)⟩\in \left(C\mathrm{Func}D\right)$$
17	15 16	sylib	$$⊢\phi \to ⟨1^{st}\left(F\right),2^{nd}\left(F\right)⟩\in \left(C\mathrm{Func}D\right)$$
18	10 17	eqeltrd	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$