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 = ( CatCat ` U )
	fucoppccic.b	\|- B = ( Base ` C )
	fucoppccic.x	\|- X = ( oppCat ` ( D FuncCat E ) )
	fucoppccic.y	\|- Y = ( ( oppCat ` D ) FuncCat ( oppCat ` E ) )
	fucoppccic.xb	\|- ( ph -> X e. B )
	fucoppccic.yb	\|- ( ph -> Y e. B )
	fucoppccic.d	\|- ( ph -> D e. V )
	fucoppccic.e	\|- ( ph -> E e. W )
Assertion	fucoppccic	\|- ( ph -> X ( ~=c ` C ) Y )

Proof

Step	Hyp	Ref	Expression
1		fucoppccic.c	\|- C = ( CatCat ` U )
2		fucoppccic.b	\|- B = ( Base ` C )
3		fucoppccic.x	\|- X = ( oppCat ` ( D FuncCat E ) )
4		fucoppccic.y	\|- Y = ( ( oppCat ` D ) FuncCat ( oppCat ` E ) )
5		fucoppccic.xb	\|- ( ph -> X e. B )
6		fucoppccic.yb	\|- ( ph -> Y e. B )
7		fucoppccic.d	\|- ( ph -> D e. V )
8		fucoppccic.e	\|- ( ph -> E e. W )
9		eqid	\|- ( Iso ` C ) = ( Iso ` C )
10	1 2	elbasfv	\|- ( X e. B -> U e. _V )
11	1	catccat	\|- ( U e. _V -> C e. Cat )
12	5 10 11	3syl	\|- ( ph -> C e. Cat )
13		eqid	\|- ( oppCat ` D ) = ( oppCat ` D )
14		eqid	\|- ( oppCat ` E ) = ( oppCat ` E )
15		eqid	\|- ( D FuncCat E ) = ( D FuncCat E )
16		eqid	\|- ( D Nat E ) = ( D Nat E )
17		eqidd	\|- ( ph -> ( oppFunc \|` ( D Func E ) ) = ( oppFunc \|` ( D Func E ) ) )
18		eqidd	\|- ( ph -> ( f e. ( D Func E ) , g e. ( D Func E ) \|-> ( _I \|` ( g ( D Nat E ) f ) ) ) = ( f e. ( D Func E ) , g e. ( D Func E ) \|-> ( _I \|` ( g ( D Nat E ) f ) ) ) )
19	13 14 15 3 4 16 17 18 1 2 9 7 8 5 6	fucoppc	\|- ( 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 ) ) ) )
20		df-br	\|- ( ( 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 ) )
21	19 20	sylib	\|- ( 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 ) )
22	9 2 12 5 6 21	brcici	\|- ( ph -> X ( ~=c ` C ) Y )

Metamath Proof Explorer

Theorem fucoppccic

Proof