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

Metamath Proof Explorer

Theorem fucoppcid

Description: The opposite category of functors is compatible with the category of opposite functors in terms of identity morphism. (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 ) ) ) )
fucoppcid.x 
|- ( ph -> X e. ( C Func D ) )
Assertion fucoppcid 
|- ( ph -> ( ( X G X ) ` ( ( Id ` R ) ` X ) ) = ( ( Id ` S ) ` ( F ` X ) ) )

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 fucoppcid.x 
 |-  ( ph -> X e. ( C Func D ) )
10 9 func1st2nd 
 |-  ( ph -> ( 1st ` X ) ( C Func D ) ( 2nd ` X ) )
11 10 funcrcl3 
 |-  ( ph -> D e. Cat )
12 eqid 
 |-  ( Id ` D ) = ( Id ` D )
13 2 12 oppcid 
 |-  ( D e. Cat -> ( Id ` P ) = ( Id ` D ) )
14 11 13 syl 
 |-  ( ph -> ( Id ` P ) = ( Id ` D ) )
15 7 9 opf11 
 |-  ( ph -> ( 1st ` ( F ` X ) ) = ( 1st ` X ) )
16 14 15 coeq12d 
 |-  ( ph -> ( ( Id ` P ) o. ( 1st ` ( F ` X ) ) ) = ( ( Id ` D ) o. ( 1st ` X ) ) )
17 eqid 
 |-  ( Id ` S ) = ( Id ` S )
18 eqid 
 |-  ( Id ` P ) = ( Id ` P )
19 1 2 oppff1 
 |-  ( oppFunc |` ( C Func D ) ) : ( C Func D ) -1-1-> ( O Func P )
20 f1f 
 |-  ( ( oppFunc |` ( C Func D ) ) : ( C Func D ) -1-1-> ( O Func P ) -> ( oppFunc |` ( C Func D ) ) : ( C Func D ) --> ( O Func P ) )
21 19 20 ax-mp 
 |-  ( oppFunc |` ( C Func D ) ) : ( C Func D ) --> ( O Func P )
22 7 feq1d 
 |-  ( ph -> ( F : ( C Func D ) --> ( O Func P ) <-> ( oppFunc |` ( C Func D ) ) : ( C Func D ) --> ( O Func P ) ) )
23 21 22 mpbiri 
 |-  ( ph -> F : ( C Func D ) --> ( O Func P ) )
24 23 9 ffvelcdmd 
 |-  ( ph -> ( F ` X ) e. ( O Func P ) )
25 5 17 18 24 fucid 
 |-  ( ph -> ( ( Id ` S ) ` ( F ` X ) ) = ( ( Id ` P ) o. ( 1st ` ( F ` X ) ) ) )
26 10 funcrcl2 
 |-  ( ph -> C e. Cat )
27 3 26 11 fuccat 
 |-  ( ph -> Q e. Cat )
28 eqid 
 |-  ( Id ` Q ) = ( Id ` Q )
29 4 28 oppcid 
 |-  ( Q e. Cat -> ( Id ` R ) = ( Id ` Q ) )
30 27 29 syl 
 |-  ( ph -> ( Id ` R ) = ( Id ` Q ) )
31 30 fveq1d 
 |-  ( ph -> ( ( Id ` R ) ` X ) = ( ( Id ` Q ) ` X ) )
32 3 28 12 9 fucid 
 |-  ( ph -> ( ( Id ` Q ) ` X ) = ( ( Id ` D ) o. ( 1st ` X ) ) )
33 31 32 eqtrd 
 |-  ( ph -> ( ( Id ` R ) ` X ) = ( ( Id ` D ) o. ( 1st ` X ) ) )
34 3 6 12 9 fucidcl 
 |-  ( ph -> ( ( Id ` D ) o. ( 1st ` X ) ) e. ( X N X ) )
35 8 9 9 33 34 opf2 
 |-  ( ph -> ( ( X G X ) ` ( ( Id ` R ) ` X ) ) = ( ( Id ` D ) o. ( 1st ` X ) ) )
36 16 25 35 3eqtr4rd 
 |-  ( ph -> ( ( X G X ) ` ( ( Id ` R ) ` X ) ) = ( ( Id ` S ) ` ( F ` X ) ) )