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=\mathrm{oppCat}\left(C\right)$$
	oppfoppc.p	$$⊢P=\mathrm{oppCat}\left(D\right)$$
	oppfoppc2.f	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
Assertion	oppfoppc2	Could not format assertion : No typesetting found for |- ( ph -> ( oppFunc ` F ) e. ( O Func P ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		oppfoppc.o	$$⊢O=\mathrm{oppCat}\left(C\right)$$
2		oppfoppc.p	$$⊢P=\mathrm{oppCat}\left(D\right)$$
3		oppfoppc2.f	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
4		relfunc	$$⊢\mathrm{Rel}\left(C\mathrm{Func}D\right)$$
5		1st2nd	$$⊢\left(\mathrm{Rel}\left(C\mathrm{Func}D\right)\wedge F\in \left(C\mathrm{Func}D\right)\right)\to F=⟨1^{st}\left(F\right),2^{nd}\left(F\right)⟩$$
6	4 3 5	sylancr	$$⊢\phi \to F=⟨1^{st}\left(F\right),2^{nd}\left(F\right)⟩$$
7	6	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 |-
8		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 |-
9	7 8	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 |-
10	3	func1st2nd	$$⊢\phi \to 1^{st}\left(F\right)\left(C\mathrm{Func}D\right)2^{nd}\left(F\right)$$
11	1 2 10	oppfoppc	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 |-
12	9 11	eqeltrd	Could not format ( ph -> ( oppFunc ` F ) e. ( O Func P ) ) : No typesetting found for |- ( ph -> ( oppFunc ` F ) e. ( O Func P ) ) with typecode |-