Metamath Proof Explorer

Theorem fucoppcco

Description: The opposite category of functors is compatible with the category of opposite functors in terms of composition. (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 ) ) ) )
fucoppcco.a 
|- ( ph -> A e. ( X ( Hom ` R ) Y ) )
fucoppcco.b 
|- ( ph -> B e. ( Y ( Hom ` R ) Z ) )
Assertion fucoppcco 
|- ( ph -> ( ( X G Z ) ` ( B ( <. X , Y >. ( comp ` R ) Z ) A ) ) = ( ( ( Y G Z ) ` B ) ( <. ( F ` X ) , ( F ` Y ) >. ( comp ` S ) ( F ` Z ) ) ( ( X G Y ) ` A ) ) )

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 fucoppcco.a 
 |-  ( ph -> A e. ( X ( Hom ` R ) Y ) )
10 fucoppcco.b 
 |-  ( ph -> B e. ( Y ( Hom ` R ) Z ) )
11 eqid 
 |-  ( O Nat P ) = ( O Nat P )
12 eqid 
 |-  ( Base ` C ) = ( Base ` C )
13 1 12 oppcbas 
 |-  ( Base ` C ) = ( Base ` O )
14 eqid 
 |-  ( comp ` P ) = ( comp ` P )
15 eqid 
 |-  ( comp ` S ) = ( comp ` S )
16 3 6 fuchom 
 |-  N = ( Hom ` Q )
17 16 4 oppchom 
 |-  ( X ( Hom ` R ) Y ) = ( Y N X )
18 9 17 eleqtrdi 
 |-  ( ph -> A e. ( Y N X ) )
19 6 natrcl 
 |-  ( A e. ( Y N X ) -> ( Y e. ( C Func D ) /\ X e. ( C Func D ) ) )
20 18 19 syl 
 |-  ( ph -> ( Y e. ( C Func D ) /\ X e. ( C Func D ) ) )
21 20 simprd 
 |-  ( ph -> X e. ( C Func D ) )
22 20 simpld 
 |-  ( ph -> Y e. ( C Func D ) )
23 1 2 6 7 21 22 fucoppclem 
 |-  ( ph -> ( Y N X ) = ( ( F ` X ) ( O Nat P ) ( F ` Y ) ) )
24 18 23 eleqtrd 
 |-  ( ph -> A e. ( ( F ` X ) ( O Nat P ) ( F ` Y ) ) )
25 16 4 oppchom 
 |-  ( Y ( Hom ` R ) Z ) = ( Z N Y )
26 10 25 eleqtrdi 
 |-  ( ph -> B e. ( Z N Y ) )
27 6 natrcl 
 |-  ( B e. ( Z N Y ) -> ( Z e. ( C Func D ) /\ Y e. ( C Func D ) ) )
28 26 27 syl 
 |-  ( ph -> ( Z e. ( C Func D ) /\ Y e. ( C Func D ) ) )
29 28 simpld 
 |-  ( ph -> Z e. ( C Func D ) )
30 1 2 6 7 22 29 fucoppclem 
 |-  ( ph -> ( Z N Y ) = ( ( F ` Y ) ( O Nat P ) ( F ` Z ) ) )
31 26 30 eleqtrd 
 |-  ( ph -> B e. ( ( F ` Y ) ( O Nat P ) ( F ` Z ) ) )
32 5 11 13 14 15 24 31 fucco 
 |-  ( ph -> ( B ( <. ( F ` X ) , ( F ` Y ) >. ( comp ` S ) ( F ` Z ) ) A ) = ( z e. ( Base ` C ) |-> ( ( B ` z ) ( <. ( ( 1st ` ( F ` X ) ) ` z ) , ( ( 1st ` ( F ` Y ) ) ` z ) >. ( comp ` P ) ( ( 1st ` ( F ` Z ) ) ` z ) ) ( A ` z ) ) ) )
33 eqidd 
 |-  ( ph -> B = B )
34 8 22 29 33 26 opf2 
 |-  ( ph -> ( ( Y G Z ) ` B ) = B )
35 eqidd 
 |-  ( ph -> A = A )
36 8 21 22 35 18 opf2 
 |-  ( ph -> ( ( X G Y ) ` A ) = A )
37 34 36 oveq12d 
 |-  ( ph -> ( ( ( Y G Z ) ` B ) ( <. ( F ` X ) , ( F ` Y ) >. ( comp ` S ) ( F ` Z ) ) ( ( X G Y ) ` A ) ) = ( B ( <. ( F ` X ) , ( F ` Y ) >. ( comp ` S ) ( F ` Z ) ) A ) )
38 eqid 
 |-  ( comp ` D ) = ( comp ` D )
39 eqid 
 |-  ( comp ` Q ) = ( comp ` Q )
40 3 6 12 38 39 26 18 fucco 
 |-  ( ph -> ( A ( <. Z , Y >. ( comp ` Q ) X ) B ) = ( z e. ( Base ` C ) |-> ( ( A ` z ) ( <. ( ( 1st ` Z ) ` z ) , ( ( 1st ` Y ) ` z ) >. ( comp ` D ) ( ( 1st ` X ) ` z ) ) ( B ` z ) ) ) )
41 3 fucbas 
 |-  ( C Func D ) = ( Base ` Q )
42 41 39 4 21 22 29 oppcco 
 |-  ( ph -> ( B ( <. X , Y >. ( comp ` R ) Z ) A ) = ( A ( <. Z , Y >. ( comp ` Q ) X ) B ) )
43 3 6 39 26 18 fuccocl 
 |-  ( ph -> ( A ( <. Z , Y >. ( comp ` Q ) X ) B ) e. ( Z N X ) )
44 8 21 29 42 43 opf2 
 |-  ( ph -> ( ( X G Z ) ` ( B ( <. X , Y >. ( comp ` R ) Z ) A ) ) = ( A ( <. Z , Y >. ( comp ` Q ) X ) B ) )
45 7 21 opf11 
 |-  ( ph -> ( 1st ` ( F ` X ) ) = ( 1st ` X ) )
46 45 fveq1d 
 |-  ( ph -> ( ( 1st ` ( F ` X ) ) ` z ) = ( ( 1st ` X ) ` z ) )
47 7 22 opf11 
 |-  ( ph -> ( 1st ` ( F ` Y ) ) = ( 1st ` Y ) )
48 47 fveq1d 
 |-  ( ph -> ( ( 1st ` ( F ` Y ) ) ` z ) = ( ( 1st ` Y ) ` z ) )
49 46 48 opeq12d 
 |-  ( ph -> <. ( ( 1st ` ( F ` X ) ) ` z ) , ( ( 1st ` ( F ` Y ) ) ` z ) >. = <. ( ( 1st ` X ) ` z ) , ( ( 1st ` Y ) ` z ) >. )
50 7 29 opf11 
 |-  ( ph -> ( 1st ` ( F ` Z ) ) = ( 1st ` Z ) )
51 50 fveq1d 
 |-  ( ph -> ( ( 1st ` ( F ` Z ) ) ` z ) = ( ( 1st ` Z ) ` z ) )
52 49 51 oveq12d 
 |-  ( ph -> ( <. ( ( 1st ` ( F ` X ) ) ` z ) , ( ( 1st ` ( F ` Y ) ) ` z ) >. ( comp ` P ) ( ( 1st ` ( F ` Z ) ) ` z ) ) = ( <. ( ( 1st ` X ) ` z ) , ( ( 1st ` Y ) ` z ) >. ( comp ` P ) ( ( 1st ` Z ) ` z ) ) )
53 52 oveqd 
 |-  ( ph -> ( ( B ` z ) ( <. ( ( 1st ` ( F ` X ) ) ` z ) , ( ( 1st ` ( F ` Y ) ) ` z ) >. ( comp ` P ) ( ( 1st ` ( F ` Z ) ) ` z ) ) ( A ` z ) ) = ( ( B ` z ) ( <. ( ( 1st ` X ) ` z ) , ( ( 1st ` Y ) ` z ) >. ( comp ` P ) ( ( 1st ` Z ) ` z ) ) ( A ` z ) ) )
54 53 adantr 
 |-  ( ( ph /\ z e. ( Base ` C ) ) -> ( ( B ` z ) ( <. ( ( 1st ` ( F ` X ) ) ` z ) , ( ( 1st ` ( F ` Y ) ) ` z ) >. ( comp ` P ) ( ( 1st ` ( F ` Z ) ) ` z ) ) ( A ` z ) ) = ( ( B ` z ) ( <. ( ( 1st ` X ) ` z ) , ( ( 1st ` Y ) ` z ) >. ( comp ` P ) ( ( 1st ` Z ) ` z ) ) ( A ` z ) ) )
55 eqid 
 |-  ( Base ` D ) = ( Base ` D )
56 21 func1st2nd 
 |-  ( ph -> ( 1st ` X ) ( C Func D ) ( 2nd ` X ) )
57 12 55 56 funcf1 
 |-  ( ph -> ( 1st ` X ) : ( Base ` C ) --> ( Base ` D ) )
58 57 ffvelcdmda 
 |-  ( ( ph /\ z e. ( Base ` C ) ) -> ( ( 1st ` X ) ` z ) e. ( Base ` D ) )
59 22 func1st2nd 
 |-  ( ph -> ( 1st ` Y ) ( C Func D ) ( 2nd ` Y ) )
60 12 55 59 funcf1 
 |-  ( ph -> ( 1st ` Y ) : ( Base ` C ) --> ( Base ` D ) )
61 60 ffvelcdmda 
 |-  ( ( ph /\ z e. ( Base ` C ) ) -> ( ( 1st ` Y ) ` z ) e. ( Base ` D ) )
62 29 func1st2nd 
 |-  ( ph -> ( 1st ` Z ) ( C Func D ) ( 2nd ` Z ) )
63 12 55 62 funcf1 
 |-  ( ph -> ( 1st ` Z ) : ( Base ` C ) --> ( Base ` D ) )
64 63 ffvelcdmda 
 |-  ( ( ph /\ z e. ( Base ` C ) ) -> ( ( 1st ` Z ) ` z ) e. ( Base ` D ) )
65 55 38 2 58 61 64 oppcco 
 |-  ( ( ph /\ z e. ( Base ` C ) ) -> ( ( B ` z ) ( <. ( ( 1st ` X ) ` z ) , ( ( 1st ` Y ) ` z ) >. ( comp ` P ) ( ( 1st ` Z ) ` z ) ) ( A ` z ) ) = ( ( A ` z ) ( <. ( ( 1st ` Z ) ` z ) , ( ( 1st ` Y ) ` z ) >. ( comp ` D ) ( ( 1st ` X ) ` z ) ) ( B ` z ) ) )
66 54 65 eqtrd 
 |-  ( ( ph /\ z e. ( Base ` C ) ) -> ( ( B ` z ) ( <. ( ( 1st ` ( F ` X ) ) ` z ) , ( ( 1st ` ( F ` Y ) ) ` z ) >. ( comp ` P ) ( ( 1st ` ( F ` Z ) ) ` z ) ) ( A ` z ) ) = ( ( A ` z ) ( <. ( ( 1st ` Z ) ` z ) , ( ( 1st ` Y ) ` z ) >. ( comp ` D ) ( ( 1st ` X ) ` z ) ) ( B ` z ) ) )
67 66 mpteq2dva 
 |-  ( ph -> ( z e. ( Base ` C ) |-> ( ( B ` z ) ( <. ( ( 1st ` ( F ` X ) ) ` z ) , ( ( 1st ` ( F ` Y ) ) ` z ) >. ( comp ` P ) ( ( 1st ` ( F ` Z ) ) ` z ) ) ( A ` z ) ) ) = ( z e. ( Base ` C ) |-> ( ( A ` z ) ( <. ( ( 1st ` Z ) ` z ) , ( ( 1st ` Y ) ` z ) >. ( comp ` D ) ( ( 1st ` X ) ` z ) ) ( B ` z ) ) ) )
68 40 44 67 3eqtr4d 
 |-  ( ph -> ( ( X G Z ) ` ( B ( <. X , Y >. ( comp ` R ) Z ) A ) ) = ( z e. ( Base ` C ) |-> ( ( B ` z ) ( <. ( ( 1st ` ( F ` X ) ) ` z ) , ( ( 1st ` ( F ` Y ) ) ` z ) >. ( comp ` P ) ( ( 1st ` ( F ` Z ) ) ` z ) ) ( A ` z ) ) ) )
69 32 37 68 3eqtr4rd 
 |-  ( ph -> ( ( X G Z ) ` ( B ( <. X , Y >. ( comp ` R ) Z ) A ) ) = ( ( ( Y G Z ) ` B ) ( <. ( F ` X ) , ( F ` Y ) >. ( comp ` S ) ( F ` Z ) ) ( ( X G Y ) ` A ) ) )