Theorem fucoppccic

Description: The opposite category of functors is isomorphic to the category of opposite functors. (Contributed by Zhi Wang, 18-Nov-2025)

	Ref	Expression
Hypotheses	fucoppccic.c	$$⊢C=\mathrm{CatCat}\left(U\right)$$
	fucoppccic.b	$$⊢B={\mathrm{Base}}_C$$
	fucoppccic.x	$$⊢X=\mathrm{oppCat}\left(D\mathrm{FuncCat}E\right)$$
	fucoppccic.y	$$⊢Y=\mathrm{oppCat}\left(D\right)\mathrm{FuncCat}\mathrm{oppCat}\left(E\right)$$
	fucoppccic.xb	$$⊢\phi \to X\in B$$
	fucoppccic.yb	$$⊢\phi \to Y\in B$$
	fucoppccic.d	$$⊢\phi \to D\in V$$
	fucoppccic.e	$$⊢\phi \to E\in W$$
Assertion	fucoppccic	$$⊢\phi \to X{\simeq }_{𝑐}\left(C\right)Y$$

Proof

Step	Hyp	Ref	Expression
1		fucoppccic.c	$$⊢C=\mathrm{CatCat}\left(U\right)$$
2		fucoppccic.b	$$⊢B={\mathrm{Base}}_C$$
3		fucoppccic.x	$$⊢X=\mathrm{oppCat}\left(D\mathrm{FuncCat}E\right)$$
4		fucoppccic.y	$$⊢Y=\mathrm{oppCat}\left(D\right)\mathrm{FuncCat}\mathrm{oppCat}\left(E\right)$$
5		fucoppccic.xb	$$⊢\phi \to X\in B$$
6		fucoppccic.yb	$$⊢\phi \to Y\in B$$
7		fucoppccic.d	$$⊢\phi \to D\in V$$
8		fucoppccic.e	$$⊢\phi \to E\in W$$
9		eqid	$$⊢\mathrm{Iso}\left(C\right)=\mathrm{Iso}\left(C\right)$$
10	1 2	elbasfv	$$⊢X\in B\to U\in \mathrm{V}$$
11	1	catccat	$$⊢U\in \mathrm{V}\to C\in \mathrm{Cat}$$
12	5 10 11	3syl	$$⊢\phi \to C\in \mathrm{Cat}$$
13		eqid	$$⊢\mathrm{oppCat}\left(D\right)=\mathrm{oppCat}\left(D\right)$$
14		eqid	$$⊢\mathrm{oppCat}\left(E\right)=\mathrm{oppCat}\left(E\right)$$
15		eqid	$$⊢D\mathrm{FuncCat}E=D\mathrm{FuncCat}E$$
16		eqid	$$⊢D\mathrm{Nat}E=D\mathrm{Nat}E$$
17		eqidd	Could not format ( ph -> ( oppFunc |` ( D Func E ) ) = ( oppFunc |` ( D Func E ) ) ) : No typesetting found for |- ( ph -> ( oppFunc |` ( D Func E ) ) = ( oppFunc |` ( D Func E ) ) ) with typecode |-
18		eqidd	$$⊢\phi \to \left(f\in \left(D\mathrm{Func}E\right),g\in \left(D\mathrm{Func}E\right)⟼{\mathrm{I}\upharpoonright }_{\left(g\left(D\mathrm{Nat}E\right)f\right)}\right)=\left(f\in \left(D\mathrm{Func}E\right),g\in \left(D\mathrm{Func}E\right)⟼{\mathrm{I}\upharpoonright }_{\left(g\left(D\mathrm{Nat}E\right)f\right)}\right)$$
19	13 14 15 3 4 16 17 18 1 2 9 7 8 5 6	fucoppc	Could not format ( ph -> ( oppFunc |` ( D Func E ) ) ( X ( Iso ` C ) Y ) ( f e. ( D Func E ) , g e. ( D Func E ) |-> ( _I |` ( g ( D Nat E ) f ) ) ) ) : No typesetting found for |- ( ph -> ( oppFunc |` ( D Func E ) ) ( X ( Iso ` C ) Y ) ( f e. ( D Func E ) , g e. ( D Func E ) |-> ( _I |` ( g ( D Nat E ) f ) ) ) ) with typecode |-
20		df-br	Could not format ( ( oppFunc |` ( D Func E ) ) ( X ( Iso ` C ) Y ) ( f e. ( D Func E ) , g e. ( D Func E ) |-> ( _I |` ( g ( D Nat E ) f ) ) ) <-> <. ( oppFunc |` ( D Func E ) ) , ( f e. ( D Func E ) , g e. ( D Func E ) |-> ( _I |` ( g ( D Nat E ) f ) ) ) >. e. ( X ( Iso ` C ) Y ) ) : No typesetting found for |- ( ( oppFunc |` ( D Func E ) ) ( X ( Iso ` C ) Y ) ( f e. ( D Func E ) , g e. ( D Func E ) |-> ( _I |` ( g ( D Nat E ) f ) ) ) <-> <. ( oppFunc |` ( D Func E ) ) , ( f e. ( D Func E ) , g e. ( D Func E ) |-> ( _I |` ( g ( D Nat E ) f ) ) ) >. e. ( X ( Iso ` C ) Y ) ) with typecode |-
21	19 20	sylib	Could not format ( ph -> <. ( oppFunc |` ( D Func E ) ) , ( f e. ( D Func E ) , g e. ( D Func E ) |-> ( _I |` ( g ( D Nat E ) f ) ) ) >. e. ( X ( Iso ` C ) Y ) ) : No typesetting found for |- ( ph -> <. ( oppFunc |` ( D Func E ) ) , ( f e. ( D Func E ) , g e. ( D Func E ) |-> ( _I |` ( g ( D Nat E ) f ) ) ) >. e. ( X ( Iso ` C ) Y ) ) with typecode |-
22	9 2 12 5 6 21	brcici	$$⊢\phi \to X{\simeq }_{𝑐}\left(C\right)Y$$