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

Metamath Proof Explorer

Theorem fucoppcfunc

Description: A 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 fucoppcfunc 
|- ( ph -> F ( R Func 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 1 2 3 4 5 6 7 8 9 10 fucoppcffth 
 |-  ( ph -> F ( ( R Full S ) i^i ( R Faith S ) ) G )
12 inss1 
 |-  ( ( R Full S ) i^i ( R Faith S ) ) C_ ( R Full S )
13 fullfunc 
 |-  ( R Full S ) C_ ( R Func S )
14 12 13 sstri 
 |-  ( ( R Full S ) i^i ( R Faith S ) ) C_ ( R Func S )
15 14 ssbri 
 |-  ( F ( ( R Full S ) i^i ( R Faith S ) ) G -> F ( R Func S ) G )
16 11 15 syl 
 |-  ( ph -> F ( R Func S ) G )