Theorem oppfoppc

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

	Ref	Expression
Hypotheses	oppfoppc.o	$$⊢O=\mathrm{oppCat}\left(C\right)$$
	oppfoppc.p	$$⊢P=\mathrm{oppCat}\left(D\right)$$
	oppfoppc.f	$$⊢\phi \to F\left(C\mathrm{Func}D\right)G$$
Assertion	oppfoppc	Could not format assertion : No typesetting found for |- ( ph -> ( F oppFunc G ) 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		oppfoppc.f	$$⊢\phi \to F\left(C\mathrm{Func}D\right)G$$
4		oppfval	Could not format ( F ( C Func D ) G -> ( F oppFunc G ) = <. F , tpos G >. ) : No typesetting found for |- ( F ( C Func D ) G -> ( F oppFunc G ) = <. F , tpos G >. ) with typecode |-
5	3 4	syl	Could not format ( ph -> ( F oppFunc G ) = <. F , tpos G >. ) : No typesetting found for |- ( ph -> ( F oppFunc G ) = <. F , tpos G >. ) with typecode |-
6	1 2 3	funcoppc	$$⊢\phi \to F\left(O\mathrm{Func}P\right)tposG$$
7		df-br	$$⊢F\left(O\mathrm{Func}P\right)tposG\leftrightarrow ⟨F,tposG⟩\in \left(O\mathrm{Func}P\right)$$
8	6 7	sylib	$$⊢\phi \to ⟨F,tposG⟩\in \left(O\mathrm{Func}P\right)$$
9	5 8	eqeltrd	Could not format ( ph -> ( F oppFunc G ) e. ( O Func P ) ) : No typesetting found for |- ( ph -> ( F oppFunc G ) e. ( O Func P ) ) with typecode |-