This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = ( 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 )