Metamath Proof Explorer

Theorem oppfdiag

Description: A diagonal functor for opposite categories is the opposite functor of the diagonal functor for original categories post-composed by an isomorphism ( fucoppc ). (Contributed by Zhi Wang, 19-Nov-2025)

Ref Expression
Hypotheses oppfdiag.o 
|- O = ( oppCat ` C )
oppfdiag.p 
|- P = ( oppCat ` D )
oppfdiag.l 
|- L = ( C DiagFunc D )
oppfdiag.c 
|- ( ph -> C e. Cat )
oppfdiag.d 
|- ( ph -> D e. Cat )
oppfdiag.f 
|- ( ph -> F = ( oppFunc |` ( D Func C ) ) )
oppfdiag.n 
|- N = ( D Nat C )
oppfdiag.g 
|- ( ph -> G = ( m e. ( D Func C ) , n e. ( D Func C ) |-> ( _I |` ( n N m ) ) ) )
Assertion oppfdiag 
|- ( ph -> ( <. F , G >. o.func ( oppFunc ` L ) ) = ( O DiagFunc P ) )

Proof

Step Hyp Ref Expression
1 oppfdiag.o 
 |-  O = ( oppCat ` C )
2 oppfdiag.p 
 |-  P = ( oppCat ` D )
3 oppfdiag.l 
 |-  L = ( C DiagFunc D )
4 oppfdiag.c 
 |-  ( ph -> C e. Cat )
5 oppfdiag.d 
 |-  ( ph -> D e. Cat )
6 oppfdiag.f 
 |-  ( ph -> F = ( oppFunc |` ( D Func C ) ) )
7 oppfdiag.n 
 |-  N = ( D Nat C )
8 oppfdiag.g 
 |-  ( ph -> G = ( m e. ( D Func C ) , n e. ( D Func C ) |-> ( _I |` ( n N m ) ) ) )
9 eqid 
 |-  ( Base ` C ) = ( Base ` C )
10 1 9 oppcbas 
 |-  ( Base ` C ) = ( Base ` O )
11 eqid 
 |-  ( P FuncCat O ) = ( P FuncCat O )
12 11 fucbas 
 |-  ( P Func O ) = ( Base ` ( P FuncCat O ) )
13 eqid 
 |-  ( oppCat ` ( D FuncCat C ) ) = ( oppCat ` ( D FuncCat C ) )
14 eqid 
 |-  ( D FuncCat C ) = ( D FuncCat C )
15 3 4 5 14 diagcl 
 |-  ( ph -> L e. ( C Func ( D FuncCat C ) ) )
16 1 13 15 oppfoppc2 
 |-  ( ph -> ( oppFunc ` L ) e. ( O Func ( oppCat ` ( D FuncCat C ) ) ) )
17 2 1 14 13 11 7 6 8 5 4 fucoppcfunc 
 |-  ( ph -> F ( ( oppCat ` ( D FuncCat C ) ) Func ( P FuncCat O ) ) G )
18 df-br 
 |-  ( F ( ( oppCat ` ( D FuncCat C ) ) Func ( P FuncCat O ) ) G <-> <. F , G >. e. ( ( oppCat ` ( D FuncCat C ) ) Func ( P FuncCat O ) ) )
19 17 18 sylib 
 |-  ( ph -> <. F , G >. e. ( ( oppCat ` ( D FuncCat C ) ) Func ( P FuncCat O ) ) )
20 16 19 cofucl 
 |-  ( ph -> ( <. F , G >. o.func ( oppFunc ` L ) ) e. ( O Func ( P FuncCat O ) ) )
21 20 func1st2nd 
 |-  ( ph -> ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) ( O Func ( P FuncCat O ) ) ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) )
22 10 12 21 funcf1 
 |-  ( ph -> ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) : ( Base ` C ) --> ( P Func O ) )
23 22 ffnd 
 |-  ( ph -> ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) Fn ( Base ` C ) )
24 eqid 
 |-  ( O DiagFunc P ) = ( O DiagFunc P )
25 1 oppccat 
 |-  ( C e. Cat -> O e. Cat )
26 4 25 syl 
 |-  ( ph -> O e. Cat )
27 2 oppccat 
 |-  ( D e. Cat -> P e. Cat )
28 5 27 syl 
 |-  ( ph -> P e. Cat )
29 24 26 28 11 diagcl 
 |-  ( ph -> ( O DiagFunc P ) e. ( O Func ( P FuncCat O ) ) )
30 29 func1st2nd 
 |-  ( ph -> ( 1st ` ( O DiagFunc P ) ) ( O Func ( P FuncCat O ) ) ( 2nd ` ( O DiagFunc P ) ) )
31 10 12 30 funcf1 
 |-  ( ph -> ( 1st ` ( O DiagFunc P ) ) : ( Base ` C ) --> ( P Func O ) )
32 31 ffnd 
 |-  ( ph -> ( 1st ` ( O DiagFunc P ) ) Fn ( Base ` C ) )
33 16 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( oppFunc ` L ) e. ( O Func ( oppCat ` ( D FuncCat C ) ) ) )
34 19 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> <. F , G >. e. ( ( oppCat ` ( D FuncCat C ) ) Func ( P FuncCat O ) ) )
35 simpr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> x e. ( Base ` C ) )
36 10 33 34 35 cofu1 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) ` x ) = ( ( 1st ` <. F , G >. ) ` ( ( 1st ` ( oppFunc ` L ) ) ` x ) ) )
37 17 func1st 
 |-  ( ph -> ( 1st ` <. F , G >. ) = F )
38 15 oppf1 
 |-  ( ph -> ( 1st ` ( oppFunc ` L ) ) = ( 1st ` L ) )
39 38 fveq1d 
 |-  ( ph -> ( ( 1st ` ( oppFunc ` L ) ) ` x ) = ( ( 1st ` L ) ` x ) )
40 37 39 fveq12d 
 |-  ( ph -> ( ( 1st ` <. F , G >. ) ` ( ( 1st ` ( oppFunc ` L ) ) ` x ) ) = ( F ` ( ( 1st ` L ) ` x ) ) )
41 40 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` <. F , G >. ) ` ( ( 1st ` ( oppFunc ` L ) ) ` x ) ) = ( F ` ( ( 1st ` L ) ` x ) ) )
42 4 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> C e. Cat )
43 5 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> D e. Cat )
44 6 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> F = ( oppFunc |` ( D Func C ) ) )
45 1 2 3 42 43 44 9 35 oppfdiag1 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( F ` ( ( 1st ` L ) ` x ) ) = ( ( 1st ` ( O DiagFunc P ) ) ` x ) )
46 36 41 45 3eqtrd 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) ` x ) = ( ( 1st ` ( O DiagFunc P ) ) ` x ) )
47 23 32 46 eqfnfvd 
 |-  ( ph -> ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) = ( 1st ` ( O DiagFunc P ) ) )
48 10 21 funcfn2 
 |-  ( ph -> ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) Fn ( ( Base ` C ) X. ( Base ` C ) ) )
49 10 30 funcfn2 
 |-  ( ph -> ( 2nd ` ( O DiagFunc P ) ) Fn ( ( Base ` C ) X. ( Base ` C ) ) )
50 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
51 50 1 oppchom 
 |-  ( x ( Hom ` O ) y ) = ( y ( Hom ` C ) x )
52 51 a1i 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x ( Hom ` O ) y ) = ( y ( Hom ` C ) x ) )
53 eqid 
 |-  ( Hom ` O ) = ( Hom ` O )
54 eqid 
 |-  ( P Nat O ) = ( P Nat O )
55 11 54 fuchom 
 |-  ( P Nat O ) = ( Hom ` ( P FuncCat O ) )
56 21 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) ( O Func ( P FuncCat O ) ) ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) )
57 simprl 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> x e. ( Base ` C ) )
58 simprr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> y e. ( Base ` C ) )
59 10 53 55 56 57 58 funcf2 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) y ) : ( x ( Hom ` O ) y ) --> ( ( ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) ` x ) ( P Nat O ) ( ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) ` y ) ) )
60 52 59 feq2dd 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) y ) : ( y ( Hom ` C ) x ) --> ( ( ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) ` x ) ( P Nat O ) ( ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) ` y ) ) )
61 60 ffnd 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) y ) Fn ( y ( Hom ` C ) x ) )
62 30 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( 1st ` ( O DiagFunc P ) ) ( O Func ( P FuncCat O ) ) ( 2nd ` ( O DiagFunc P ) ) )
63 10 53 55 62 57 58 funcf2 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x ( 2nd ` ( O DiagFunc P ) ) y ) : ( x ( Hom ` O ) y ) --> ( ( ( 1st ` ( O DiagFunc P ) ) ` x ) ( P Nat O ) ( ( 1st ` ( O DiagFunc P ) ) ` y ) ) )
64 52 63 feq2dd 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x ( 2nd ` ( O DiagFunc P ) ) y ) : ( y ( Hom ` C ) x ) --> ( ( ( 1st ` ( O DiagFunc P ) ) ` x ) ( P Nat O ) ( ( 1st ` ( O DiagFunc P ) ) ` y ) ) )
65 64 ffnd 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x ( 2nd ` ( O DiagFunc P ) ) y ) Fn ( y ( Hom ` C ) x ) )
66 16 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( y ( Hom ` C ) x ) ) -> ( oppFunc ` L ) e. ( O Func ( oppCat ` ( D FuncCat C ) ) ) )
67 19 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( y ( Hom ` C ) x ) ) -> <. F , G >. e. ( ( oppCat ` ( D FuncCat C ) ) Func ( P FuncCat O ) ) )
68 57 adantr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( y ( Hom ` C ) x ) ) -> x e. ( Base ` C ) )
69 58 adantr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( y ( Hom ` C ) x ) ) -> y e. ( Base ` C ) )
70 simpr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( y ( Hom ` C ) x ) ) -> f e. ( y ( Hom ` C ) x ) )
71 70 51 eleqtrrdi 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( y ( Hom ` C ) x ) ) -> f e. ( x ( Hom ` O ) y ) )
72 10 66 67 68 69 53 71 cofu2 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( y ( Hom ` C ) x ) ) -> ( ( x ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) y ) ` f ) = ( ( ( ( 1st ` ( oppFunc ` L ) ) ` x ) ( 2nd ` <. F , G >. ) ( ( 1st ` ( oppFunc ` L ) ) ` y ) ) ` ( ( x ( 2nd ` ( oppFunc ` L ) ) y ) ` f ) ) )
73 17 func2nd 
 |-  ( ph -> ( 2nd ` <. F , G >. ) = G )
74 38 fveq1d 
 |-  ( ph -> ( ( 1st ` ( oppFunc ` L ) ) ` y ) = ( ( 1st ` L ) ` y ) )
75 73 39 74 oveq123d 
 |-  ( ph -> ( ( ( 1st ` ( oppFunc ` L ) ) ` x ) ( 2nd ` <. F , G >. ) ( ( 1st ` ( oppFunc ` L ) ) ` y ) ) = ( ( ( 1st ` L ) ` x ) G ( ( 1st ` L ) ` y ) ) )
76 15 oppf2 
 |-  ( ph -> ( x ( 2nd ` ( oppFunc ` L ) ) y ) = ( y ( 2nd ` L ) x ) )
77 76 fveq1d 
 |-  ( ph -> ( ( x ( 2nd ` ( oppFunc ` L ) ) y ) ` f ) = ( ( y ( 2nd ` L ) x ) ` f ) )
78 75 77 fveq12d 
 |-  ( ph -> ( ( ( ( 1st ` ( oppFunc ` L ) ) ` x ) ( 2nd ` <. F , G >. ) ( ( 1st ` ( oppFunc ` L ) ) ` y ) ) ` ( ( x ( 2nd ` ( oppFunc ` L ) ) y ) ` f ) ) = ( ( ( ( 1st ` L ) ` x ) G ( ( 1st ` L ) ` y ) ) ` ( ( y ( 2nd ` L ) x ) ` f ) ) )
79 78 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( y ( Hom ` C ) x ) ) -> ( ( ( ( 1st ` ( oppFunc ` L ) ) ` x ) ( 2nd ` <. F , G >. ) ( ( 1st ` ( oppFunc ` L ) ) ` y ) ) ` ( ( x ( 2nd ` ( oppFunc ` L ) ) y ) ` f ) ) = ( ( ( ( 1st ` L ) ` x ) G ( ( 1st ` L ) ` y ) ) ` ( ( y ( 2nd ` L ) x ) ` f ) ) )
80 8 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( y ( Hom ` C ) x ) ) -> G = ( m e. ( D Func C ) , n e. ( D Func C ) |-> ( _I |` ( n N m ) ) ) )
81 4 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( y ( Hom ` C ) x ) ) -> C e. Cat )
82 5 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( y ( Hom ` C ) x ) ) -> D e. Cat )
83 eqid 
 |-  ( ( 1st ` L ) ` x ) = ( ( 1st ` L ) ` x )
84 3 81 82 9 68 83 diag1cl 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( y ( Hom ` C ) x ) ) -> ( ( 1st ` L ) ` x ) e. ( D Func C ) )
85 eqid 
 |-  ( ( 1st ` L ) ` y ) = ( ( 1st ` L ) ` y )
86 3 81 82 9 69 85 diag1cl 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( y ( Hom ` C ) x ) ) -> ( ( 1st ` L ) ` y ) e. ( D Func C ) )
87 eqid 
 |-  ( Base ` D ) = ( Base ` D )
88 3 9 87 50 81 82 69 68 70 diag2 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( y ( Hom ` C ) x ) ) -> ( ( y ( 2nd ` L ) x ) ` f ) = ( ( Base ` D ) X. { f } ) )
89 3 9 87 50 81 82 69 68 70 7 diag2cl 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( y ( Hom ` C ) x ) ) -> ( ( Base ` D ) X. { f } ) e. ( ( ( 1st ` L ) ` y ) N ( ( 1st ` L ) ` x ) ) )
90 80 84 86 88 89 opf2 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( y ( Hom ` C ) x ) ) -> ( ( ( ( 1st ` L ) ` x ) G ( ( 1st ` L ) ` y ) ) ` ( ( y ( 2nd ` L ) x ) ` f ) ) = ( ( Base ` D ) X. { f } ) )
91 72 79 90 3eqtrd 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( y ( Hom ` C ) x ) ) -> ( ( x ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) y ) ` f ) = ( ( Base ` D ) X. { f } ) )
92 2 87 oppcbas 
 |-  ( Base ` D ) = ( Base ` P )
93 81 25 syl 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( y ( Hom ` C ) x ) ) -> O e. Cat )
94 82 27 syl 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( y ( Hom ` C ) x ) ) -> P e. Cat )
95 24 10 92 53 93 94 68 69 71 diag2 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( y ( Hom ` C ) x ) ) -> ( ( x ( 2nd ` ( O DiagFunc P ) ) y ) ` f ) = ( ( Base ` D ) X. { f } ) )
96 91 95 eqtr4d 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ f e. ( y ( Hom ` C ) x ) ) -> ( ( x ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) y ) ` f ) = ( ( x ( 2nd ` ( O DiagFunc P ) ) y ) ` f ) )
97 61 65 96 eqfnfvd 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) y ) = ( x ( 2nd ` ( O DiagFunc P ) ) y ) )
98 48 49 97 eqfnovd 
 |-  ( ph -> ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) = ( 2nd ` ( O DiagFunc P ) ) )
99 47 98 opeq12d 
 |-  ( ph -> <. ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) , ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) >. = <. ( 1st ` ( O DiagFunc P ) ) , ( 2nd ` ( O DiagFunc P ) ) >. )
100 relfunc 
 |-  Rel ( O Func ( P FuncCat O ) )
101 1st2nd 
 |-  ( ( Rel ( O Func ( P FuncCat O ) ) /\ ( <. F , G >. o.func ( oppFunc ` L ) ) e. ( O Func ( P FuncCat O ) ) ) -> ( <. F , G >. o.func ( oppFunc ` L ) ) = <. ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) , ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) >. )
102 100 20 101 sylancr 
 |-  ( ph -> ( <. F , G >. o.func ( oppFunc ` L ) ) = <. ( 1st ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) , ( 2nd ` ( <. F , G >. o.func ( oppFunc ` L ) ) ) >. )
103 1st2nd 
 |-  ( ( Rel ( O Func ( P FuncCat O ) ) /\ ( O DiagFunc P ) e. ( O Func ( P FuncCat O ) ) ) -> ( O DiagFunc P ) = <. ( 1st ` ( O DiagFunc P ) ) , ( 2nd ` ( O DiagFunc P ) ) >. )
104 100 29 103 sylancr 
 |-  ( ph -> ( O DiagFunc P ) = <. ( 1st ` ( O DiagFunc P ) ) , ( 2nd ` ( O DiagFunc P ) ) >. )
105 99 102 104 3eqtr4d 
 |-  ( ph -> ( <. F , G >. o.func ( oppFunc ` L ) ) = ( O DiagFunc P ) )