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

Metamath Proof Explorer

Theorem fucoppcffth

Description: A fully faithful functor from the opposite category of functors to the category of opposite functors. (Contributed by Zhi Wang, 19-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 ) ) ) )
fucoppcffth.c 
|- ( ph -> C e. Cat )
fucoppcffth.d 
|- ( ph -> D e. Cat )
Assertion fucoppcffth 
|- ( ph -> F ( ( R Full S ) i^i ( R Faith 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 fucoppcffth.c 
 |-  ( ph -> C e. Cat )
10 fucoppcffth.d 
 |-  ( ph -> D e. Cat )
11 eqid 
 |-  ( CatCat ` { R , S } ) = ( CatCat ` { R , S } )
12 eqid 
 |-  ( Base ` R ) = ( Base ` R )
13 eqid 
 |-  ( Base ` S ) = ( Base ` S )
14 eqid 
 |-  ( Iso ` ( CatCat ` { R , S } ) ) = ( Iso ` ( CatCat ` { R , S } ) )
15 eqid 
 |-  ( Base ` ( CatCat ` { R , S } ) ) = ( Base ` ( CatCat ` { R , S } ) )
16 3 9 10 fuccat 
 |-  ( ph -> Q e. Cat )
17 4 oppccat 
 |-  ( Q e. Cat -> R e. Cat )
18 16 17 syl 
 |-  ( ph -> R e. Cat )
19 prid1g 
 |-  ( R e. Cat -> R e. { R , S } )
20 18 19 syl 
 |-  ( ph -> R e. { R , S } )
21 20 18 elind 
 |-  ( ph -> R e. ( { R , S } i^i Cat ) )
22 prex 
 |-  { R , S } e. _V
23 22 a1i 
 |-  ( ph -> { R , S } e. _V )
24 11 15 23 catcbas 
 |-  ( ph -> ( Base ` ( CatCat ` { R , S } ) ) = ( { R , S } i^i Cat ) )
25 21 24 eleqtrrd 
 |-  ( ph -> R e. ( Base ` ( CatCat ` { R , S } ) ) )
26 1 oppccat 
 |-  ( C e. Cat -> O e. Cat )
27 9 26 syl 
 |-  ( ph -> O e. Cat )
28 2 oppccat 
 |-  ( D e. Cat -> P e. Cat )
29 10 28 syl 
 |-  ( ph -> P e. Cat )
30 5 27 29 fuccat 
 |-  ( ph -> S e. Cat )
31 prid2g 
 |-  ( S e. Cat -> S e. { R , S } )
32 30 31 syl 
 |-  ( ph -> S e. { R , S } )
33 32 30 elind 
 |-  ( ph -> S e. ( { R , S } i^i Cat ) )
34 33 24 eleqtrrd 
 |-  ( ph -> S e. ( Base ` ( CatCat ` { R , S } ) ) )
35 1 2 3 4 5 6 7 8 11 15 14 9 10 25 34 fucoppc 
 |-  ( ph -> F ( R ( Iso ` ( CatCat ` { R , S } ) ) S ) G )
36 df-br 
 |-  ( F ( R ( Iso ` ( CatCat ` { R , S } ) ) S ) G <-> <. F , G >. e. ( R ( Iso ` ( CatCat ` { R , S } ) ) S ) )
37 35 36 sylib 
 |-  ( ph -> <. F , G >. e. ( R ( Iso ` ( CatCat ` { R , S } ) ) S ) )
38 11 12 13 14 37 catcisoi 
 |-  ( ph -> ( <. F , G >. e. ( ( R Full S ) i^i ( R Faith S ) ) /\ ( 1st ` <. F , G >. ) : ( Base ` R ) -1-1-onto-> ( Base ` S ) ) )
39 38 simpld 
 |-  ( ph -> <. F , G >. e. ( ( R Full S ) i^i ( R Faith S ) ) )
40 df-br 
 |-  ( F ( ( R Full S ) i^i ( R Faith S ) ) G <-> <. F , G >. e. ( ( R Full S ) i^i ( R Faith S ) ) )
41 39 40 sylibr 
 |-  ( ph -> F ( ( R Full S ) i^i ( R Faith S ) ) G )