Metamath Proof Explorer

Theorem fucoppc

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

Ref Expression
Hypotheses fucoppc.o 
|- O = ( oppCat ` C )
fucoppc.p 
|- P = ( oppCat ` D )
fucoppc.q 
|- Q = ( C FuncCat D )
fucoppc.r 
|- R = ( oppCat ` Q )
fucoppc.s 
|- S = ( O FuncCat P )
fucoppc.n 
|- N = ( C Nat D )
fucoppc.f 
|- ( ph -> F = ( oppFunc |` ( C Func D ) ) )
fucoppc.g 
|- ( ph -> G = ( x e. ( C Func D ) , y e. ( C Func D ) |-> ( _I |` ( y N x ) ) ) )
fucoppc.t 
|- T = ( CatCat ` U )
fucoppc.b 
|- B = ( Base ` T )
fucoppc.i 
|- I = ( Iso ` T )
fucoppc.c 
|- ( ph -> C e. V )
fucoppc.d 
|- ( ph -> D e. W )
fucoppc.1 
|- ( ph -> R e. B )
fucoppc.2 
|- ( ph -> S e. B )
Assertion fucoppc 
|- ( ph -> F ( R I S ) G )

Proof

Step Hyp Ref Expression
1 fucoppc.o 
 |-  O = ( oppCat ` C )
2 fucoppc.p 
 |-  P = ( oppCat ` D )
3 fucoppc.q 
 |-  Q = ( C FuncCat D )
4 fucoppc.r 
 |-  R = ( oppCat ` Q )
5 fucoppc.s 
 |-  S = ( O FuncCat P )
6 fucoppc.n 
 |-  N = ( C Nat D )
7 fucoppc.f 
 |-  ( ph -> F = ( oppFunc |` ( C Func D ) ) )
8 fucoppc.g 
 |-  ( ph -> G = ( x e. ( C Func D ) , y e. ( C Func D ) |-> ( _I |` ( y N x ) ) ) )
9 fucoppc.t 
 |-  T = ( CatCat ` U )
10 fucoppc.b 
 |-  B = ( Base ` T )
11 fucoppc.i 
 |-  I = ( Iso ` T )
12 fucoppc.c 
 |-  ( ph -> C e. V )
13 fucoppc.d 
 |-  ( ph -> D e. W )
14 fucoppc.1 
 |-  ( ph -> R e. B )
15 fucoppc.2 
 |-  ( ph -> S e. B )
16 3 fucbas 
 |-  ( C Func D ) = ( Base ` Q )
17 4 16 oppcbas 
 |-  ( C Func D ) = ( Base ` R )
18 5 fucbas 
 |-  ( O Func P ) = ( Base ` S )
19 eqid 
 |-  ( Hom ` R ) = ( Hom ` R )
20 eqid 
 |-  ( O Nat P ) = ( O Nat P )
21 5 20 fuchom 
 |-  ( O Nat P ) = ( Hom ` S )
22 eqid 
 |-  ( Id ` R ) = ( Id ` R )
23 eqid 
 |-  ( Id ` S ) = ( Id ` S )
24 eqid 
 |-  ( comp ` R ) = ( comp ` R )
25 eqid 
 |-  ( comp ` S ) = ( comp ` S )
26 9 10 elbasfv 
 |-  ( R e. B -> U e. _V )
27 14 26 syl 
 |-  ( ph -> U e. _V )
28 9 10 27 catcbas 
 |-  ( ph -> B = ( U i^i Cat ) )
29 14 28 eleqtrd 
 |-  ( ph -> R e. ( U i^i Cat ) )
30 29 elin2d 
 |-  ( ph -> R e. Cat )
31 15 28 eleqtrd 
 |-  ( ph -> S e. ( U i^i Cat ) )
32 31 elin2d 
 |-  ( ph -> S e. Cat )
33 1 2 12 13 oppff1o 
 |-  ( ph -> ( oppFunc |` ( C Func D ) ) : ( C Func D ) -1-1-onto-> ( O Func P ) )
34 7 f1oeq1d 
 |-  ( ph -> ( F : ( C Func D ) -1-1-onto-> ( O Func P ) <-> ( oppFunc |` ( C Func D ) ) : ( C Func D ) -1-1-onto-> ( O Func P ) ) )
35 33 34 mpbird 
 |-  ( ph -> F : ( C Func D ) -1-1-onto-> ( O Func P ) )
36 f1of 
 |-  ( F : ( C Func D ) -1-1-onto-> ( O Func P ) -> F : ( C Func D ) --> ( O Func P ) )
37 35 36 syl 
 |-  ( ph -> F : ( C Func D ) --> ( O Func P ) )
38 eqid 
 |-  ( x e. ( C Func D ) , y e. ( C Func D ) |-> ( _I |` ( y N x ) ) ) = ( x e. ( C Func D ) , y e. ( C Func D ) |-> ( _I |` ( y N x ) ) )
39 ovex 
 |-  ( y N x ) e. _V
40 resiexg 
 |-  ( ( y N x ) e. _V -> ( _I |` ( y N x ) ) e. _V )
41 39 40 ax-mp 
 |-  ( _I |` ( y N x ) ) e. _V
42 38 41 fnmpoi 
 |-  ( x e. ( C Func D ) , y e. ( C Func D ) |-> ( _I |` ( y N x ) ) ) Fn ( ( C Func D ) X. ( C Func D ) )
43 8 fneq1d 
 |-  ( ph -> ( G Fn ( ( C Func D ) X. ( C Func D ) ) <-> ( x e. ( C Func D ) , y e. ( C Func D ) |-> ( _I |` ( y N x ) ) ) Fn ( ( C Func D ) X. ( C Func D ) ) ) )
44 42 43 mpbiri 
 |-  ( ph -> G Fn ( ( C Func D ) X. ( C Func D ) ) )
45 f1oi 
 |-  ( _I |` ( g N f ) ) : ( g N f ) -1-1-onto-> ( g N f )
46 8 adantr 
 |-  ( ( ph /\ ( f e. ( C Func D ) /\ g e. ( C Func D ) ) ) -> G = ( x e. ( C Func D ) , y e. ( C Func D ) |-> ( _I |` ( y N x ) ) ) )
47 simprl 
 |-  ( ( ph /\ ( f e. ( C Func D ) /\ g e. ( C Func D ) ) ) -> f e. ( C Func D ) )
48 simprr 
 |-  ( ( ph /\ ( f e. ( C Func D ) /\ g e. ( C Func D ) ) ) -> g e. ( C Func D ) )
49 46 47 48 opf2fval 
 |-  ( ( ph /\ ( f e. ( C Func D ) /\ g e. ( C Func D ) ) ) -> ( f G g ) = ( _I |` ( g N f ) ) )
50 3 6 fuchom 
 |-  N = ( Hom ` Q )
51 50 4 oppchom 
 |-  ( f ( Hom ` R ) g ) = ( g N f )
52 51 a1i 
 |-  ( ( ph /\ ( f e. ( C Func D ) /\ g e. ( C Func D ) ) ) -> ( f ( Hom ` R ) g ) = ( g N f ) )
53 7 adantr 
 |-  ( ( ph /\ ( f e. ( C Func D ) /\ g e. ( C Func D ) ) ) -> F = ( oppFunc |` ( C Func D ) ) )
54 1 2 6 53 47 48 fucoppclem 
 |-  ( ( ph /\ ( f e. ( C Func D ) /\ g e. ( C Func D ) ) ) -> ( g N f ) = ( ( F ` f ) ( O Nat P ) ( F ` g ) ) )
55 54 eqcomd 
 |-  ( ( ph /\ ( f e. ( C Func D ) /\ g e. ( C Func D ) ) ) -> ( ( F ` f ) ( O Nat P ) ( F ` g ) ) = ( g N f ) )
56 49 52 55 f1oeq123d 
 |-  ( ( ph /\ ( f e. ( C Func D ) /\ g e. ( C Func D ) ) ) -> ( ( f G g ) : ( f ( Hom ` R ) g ) -1-1-onto-> ( ( F ` f ) ( O Nat P ) ( F ` g ) ) <-> ( _I |` ( g N f ) ) : ( g N f ) -1-1-onto-> ( g N f ) ) )
57 45 56 mpbiri 
 |-  ( ( ph /\ ( f e. ( C Func D ) /\ g e. ( C Func D ) ) ) -> ( f G g ) : ( f ( Hom ` R ) g ) -1-1-onto-> ( ( F ` f ) ( O Nat P ) ( F ` g ) ) )
58 f1of 
 |-  ( ( f G g ) : ( f ( Hom ` R ) g ) -1-1-onto-> ( ( F ` f ) ( O Nat P ) ( F ` g ) ) -> ( f G g ) : ( f ( Hom ` R ) g ) --> ( ( F ` f ) ( O Nat P ) ( F ` g ) ) )
59 57 58 syl 
 |-  ( ( ph /\ ( f e. ( C Func D ) /\ g e. ( C Func D ) ) ) -> ( f G g ) : ( f ( Hom ` R ) g ) --> ( ( F ` f ) ( O Nat P ) ( F ` g ) ) )
60 7 adantr 
 |-  ( ( ph /\ f e. ( C Func D ) ) -> F = ( oppFunc |` ( C Func D ) ) )
61 8 adantr 
 |-  ( ( ph /\ f e. ( C Func D ) ) -> G = ( x e. ( C Func D ) , y e. ( C Func D ) |-> ( _I |` ( y N x ) ) ) )
62 simpr 
 |-  ( ( ph /\ f e. ( C Func D ) ) -> f e. ( C Func D ) )
63 1 2 3 4 5 6 60 61 62 fucoppcid 
 |-  ( ( ph /\ f e. ( C Func D ) ) -> ( ( f G f ) ` ( ( Id ` R ) ` f ) ) = ( ( Id ` S ) ` ( F ` f ) ) )
64 7 3ad2ant1 
 |-  ( ( ph /\ ( f e. ( C Func D ) /\ g e. ( C Func D ) /\ k e. ( C Func D ) ) /\ ( a e. ( f ( Hom ` R ) g ) /\ b e. ( g ( Hom ` R ) k ) ) ) -> F = ( oppFunc |` ( C Func D ) ) )
65 8 3ad2ant1 
 |-  ( ( ph /\ ( f e. ( C Func D ) /\ g e. ( C Func D ) /\ k e. ( C Func D ) ) /\ ( a e. ( f ( Hom ` R ) g ) /\ b e. ( g ( Hom ` R ) k ) ) ) -> G = ( x e. ( C Func D ) , y e. ( C Func D ) |-> ( _I |` ( y N x ) ) ) )
66 simp3l 
 |-  ( ( ph /\ ( f e. ( C Func D ) /\ g e. ( C Func D ) /\ k e. ( C Func D ) ) /\ ( a e. ( f ( Hom ` R ) g ) /\ b e. ( g ( Hom ` R ) k ) ) ) -> a e. ( f ( Hom ` R ) g ) )
67 simp3r 
 |-  ( ( ph /\ ( f e. ( C Func D ) /\ g e. ( C Func D ) /\ k e. ( C Func D ) ) /\ ( a e. ( f ( Hom ` R ) g ) /\ b e. ( g ( Hom ` R ) k ) ) ) -> b e. ( g ( Hom ` R ) k ) )
68 1 2 3 4 5 6 64 65 66 67 fucoppcco 
 |-  ( ( ph /\ ( f e. ( C Func D ) /\ g e. ( C Func D ) /\ k e. ( C Func D ) ) /\ ( a e. ( f ( Hom ` R ) g ) /\ b e. ( g ( Hom ` R ) k ) ) ) -> ( ( f G k ) ` ( b ( <. f , g >. ( comp ` R ) k ) a ) ) = ( ( ( g G k ) ` b ) ( <. ( F ` f ) , ( F ` g ) >. ( comp ` S ) ( F ` k ) ) ( ( f G g ) ` a ) ) )
69 17 18 19 21 22 23 24 25 30 32 37 44 59 63 68 isfuncd 
 |-  ( ph -> F ( R Func S ) G )
70 57 ralrimivva 
 |-  ( ph -> A. f e. ( C Func D ) A. g e. ( C Func D ) ( f G g ) : ( f ( Hom ` R ) g ) -1-1-onto-> ( ( F ` f ) ( O Nat P ) ( F ` g ) ) )
71 17 19 21 isffth2 
 |-  ( F ( ( R Full S ) i^i ( R Faith S ) ) G <-> ( F ( R Func S ) G /\ A. f e. ( C Func D ) A. g e. ( C Func D ) ( f G g ) : ( f ( Hom ` R ) g ) -1-1-onto-> ( ( F ` f ) ( O Nat P ) ( F ` g ) ) ) )
72 69 70 71 sylanbrc 
 |-  ( ph -> F ( ( R Full S ) i^i ( R Faith S ) ) G )
73 df-br 
 |-  ( F ( ( R Full S ) i^i ( R Faith S ) ) G <-> <. F , G >. e. ( ( R Full S ) i^i ( R Faith S ) ) )
74 72 73 sylib 
 |-  ( ph -> <. F , G >. e. ( ( R Full S ) i^i ( R Faith S ) ) )
75 69 func1st 
 |-  ( ph -> ( 1st ` <. F , G >. ) = F )
76 75 f1oeq1d 
 |-  ( ph -> ( ( 1st ` <. F , G >. ) : ( C Func D ) -1-1-onto-> ( O Func P ) <-> F : ( C Func D ) -1-1-onto-> ( O Func P ) ) )
77 35 76 mpbird 
 |-  ( ph -> ( 1st ` <. F , G >. ) : ( C Func D ) -1-1-onto-> ( O Func P ) )
78 9 10 17 18 27 14 15 11 catciso 
 |-  ( ph -> ( <. F , G >. e. ( R I S ) <-> ( <. F , G >. e. ( ( R Full S ) i^i ( R Faith S ) ) /\ ( 1st ` <. F , G >. ) : ( C Func D ) -1-1-onto-> ( O Func P ) ) ) )
79 74 77 78 mpbir2and 
 |-  ( ph -> <. F , G >. e. ( R I S ) )
80 df-br 
 |-  ( F ( R I S ) G <-> <. F , G >. e. ( R I S ) )
81 79 80 sylibr 
 |-  ( ph -> F ( R I S ) G )