Theorem 2oppffunc

Description: The opposite functor of an opposite functor is 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$$
	2oppffunc.f	No typesetting found for |- G = ( oppFunc ` F ) with typecode |-
	2oppffunc.g	$$⊢\phi \to G\in \left(O\mathrm{Func}P\right)$$
Assertion	2oppffunc	Could not format assertion : No typesetting found for |- ( ph -> ( oppFunc ` G ) e. ( C Func D ) ) with typecode |-

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		2oppffunc.f	Could not format G = ( oppFunc ` F ) : No typesetting found for |- G = ( oppFunc ` F ) with typecode |-
6		2oppffunc.g	$$⊢\phi \to G\in \left(O\mathrm{Func}P\right)$$
7		relfunc	$$⊢\mathrm{Rel}\left(O\mathrm{Func}P\right)$$
8	6 7 5	2oppf	Could not format ( ph -> ( oppFunc ` G ) = F ) : No typesetting found for |- ( ph -> ( oppFunc ` G ) = F ) with typecode |-
9	5 6	eqeltrrid	Could not format ( ph -> ( oppFunc ` F ) e. ( O Func P ) ) : No typesetting found for |- ( ph -> ( oppFunc ` F ) e. ( O Func P ) ) with typecode |-
10	1 2 3 4 9	funcoppc5	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
11	8 10	eqeltrd	Could not format ( ph -> ( oppFunc ` G ) e. ( C Func D ) ) : No typesetting found for |- ( ph -> ( oppFunc ` G ) e. ( C Func D ) ) with typecode |-