Metamath Proof Explorer

Theorem cmddu

Description: The duality of limits and colimits: colimits of a diagram are limits of an opposite diagram in opposite categories. (Contributed by Zhi Wang, 20-Nov-2025)

Ref Expression
Hypotheses lmddu.o 
|- O = ( oppCat ` C )
lmddu.p 
|- P = ( oppCat ` D )
lmddu.g 
|- G = ( oppFunc ` F )
lmddu.c 
|- ( ph -> C e. V )
lmddu.d 
|- ( ph -> D e. W )
Assertion cmddu 
|- ( ph -> ( ( C Colimit D ) ` F ) = ( ( O Limit P ) ` G ) )

Proof

Step Hyp Ref Expression
1 lmddu.o 
 |-  O = ( oppCat ` C )
2 lmddu.p 
 |-  P = ( oppCat ` D )
3 lmddu.g 
 |-  G = ( oppFunc ` F )
4 lmddu.c 
 |-  ( ph -> C e. V )
5 lmddu.d 
 |-  ( ph -> D e. W )
6 relup 
 |-  Rel ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F )
7 relup 
 |-  Rel ( ( ( oppCat ` O ) DiagFunc ( oppCat ` P ) ) ( ( oppCat ` O ) UP ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) ) ( oppFunc ` G ) )
8 simpr 
 |-  ( ( ph /\ x ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) m ) -> x ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) m )
9 8 up1st2nd 
 |-  ( ( ph /\ x ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) m ) -> x ( <. ( 1st ` ( C DiagFunc D ) ) , ( 2nd ` ( C DiagFunc D ) ) >. ( C UP ( D FuncCat C ) ) F ) m )
10 eqid 
 |-  ( D FuncCat C ) = ( D FuncCat C )
11 10 fucbas 
 |-  ( D Func C ) = ( Base ` ( D FuncCat C ) )
12 9 11 uprcl3 
 |-  ( ( ph /\ x ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) m ) -> F e. ( D Func C ) )
13 5 adantr 
 |-  ( ( ph /\ x ( ( ( oppCat ` O ) DiagFunc ( oppCat ` P ) ) ( ( oppCat ` O ) UP ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) ) ( oppFunc ` G ) ) m ) -> D e. W )
14 4 adantr 
 |-  ( ( ph /\ x ( ( ( oppCat ` O ) DiagFunc ( oppCat ` P ) ) ( ( oppCat ` O ) UP ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) ) ( oppFunc ` G ) ) m ) -> C e. V )
15 eqid 
 |-  ( oppCat ` P ) = ( oppCat ` P )
16 eqid 
 |-  ( oppCat ` O ) = ( oppCat ` O )
17 2 fvexi 
 |-  P e. _V
18 17 a1i 
 |-  ( ( ph /\ x ( ( ( oppCat ` O ) DiagFunc ( oppCat ` P ) ) ( ( oppCat ` O ) UP ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) ) ( oppFunc ` G ) ) m ) -> P e. _V )
19 1 fvexi 
 |-  O e. _V
20 19 a1i 
 |-  ( ( ph /\ x ( ( ( oppCat ` O ) DiagFunc ( oppCat ` P ) ) ( ( oppCat ` O ) UP ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) ) ( oppFunc ` G ) ) m ) -> O e. _V )
21 simpr 
 |-  ( ( ph /\ x ( ( ( oppCat ` O ) DiagFunc ( oppCat ` P ) ) ( ( oppCat ` O ) UP ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) ) ( oppFunc ` G ) ) m ) -> x ( ( ( oppCat ` O ) DiagFunc ( oppCat ` P ) ) ( ( oppCat ` O ) UP ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) ) ( oppFunc ` G ) ) m )
22 21 up1st2nd 
 |-  ( ( ph /\ x ( ( ( oppCat ` O ) DiagFunc ( oppCat ` P ) ) ( ( oppCat ` O ) UP ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) ) ( oppFunc ` G ) ) m ) -> x ( <. ( 1st ` ( ( oppCat ` O ) DiagFunc ( oppCat ` P ) ) ) , ( 2nd ` ( ( oppCat ` O ) DiagFunc ( oppCat ` P ) ) ) >. ( ( oppCat ` O ) UP ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) ) ( oppFunc ` G ) ) m )
23 eqid 
 |-  ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) = ( ( oppCat ` P ) FuncCat ( oppCat ` O ) )
24 23 fucbas 
 |-  ( ( oppCat ` P ) Func ( oppCat ` O ) ) = ( Base ` ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) )
25 22 24 uprcl3 
 |-  ( ( ph /\ x ( ( ( oppCat ` O ) DiagFunc ( oppCat ` P ) ) ( ( oppCat ` O ) UP ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) ) ( oppFunc ` G ) ) m ) -> ( oppFunc ` G ) e. ( ( oppCat ` P ) Func ( oppCat ` O ) ) )
26 15 16 18 20 25 funcoppc5 
 |-  ( ( ph /\ x ( ( ( oppCat ` O ) DiagFunc ( oppCat ` P ) ) ( ( oppCat ` O ) UP ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) ) ( oppFunc ` G ) ) m ) -> G e. ( P Func O ) )
27 3 26 eqeltrrid 
 |-  ( ( ph /\ x ( ( ( oppCat ` O ) DiagFunc ( oppCat ` P ) ) ( ( oppCat ` O ) UP ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) ) ( oppFunc ` G ) ) m ) -> ( oppFunc ` F ) e. ( P Func O ) )
28 2 1 13 14 27 funcoppc5 
 |-  ( ( ph /\ x ( ( ( oppCat ` O ) DiagFunc ( oppCat ` P ) ) ( ( oppCat ` O ) UP ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) ) ( oppFunc ` G ) ) m ) -> F e. ( D Func C ) )
29 1 2oppchomf 
 |-  ( Homf ` C ) = ( Homf ` ( oppCat ` O ) )
30 29 a1i 
 |-  ( F e. ( D Func C ) -> ( Homf ` C ) = ( Homf ` ( oppCat ` O ) ) )
31 1 2oppccomf 
 |-  ( comf ` C ) = ( comf ` ( oppCat ` O ) )
32 31 a1i 
 |-  ( F e. ( D Func C ) -> ( comf ` C ) = ( comf ` ( oppCat ` O ) ) )
33 2 2oppchomf 
 |-  ( Homf ` D ) = ( Homf ` ( oppCat ` P ) )
34 33 a1i 
 |-  ( F e. ( D Func C ) -> ( Homf ` D ) = ( Homf ` ( oppCat ` P ) ) )
35 2 2oppccomf 
 |-  ( comf ` D ) = ( comf ` ( oppCat ` P ) )
36 35 a1i 
 |-  ( F e. ( D Func C ) -> ( comf ` D ) = ( comf ` ( oppCat ` P ) ) )
37 funcrcl 
 |-  ( F e. ( D Func C ) -> ( D e. Cat /\ C e. Cat ) )
38 37 simpld 
 |-  ( F e. ( D Func C ) -> D e. Cat )
39 2 oppccat 
 |-  ( D e. Cat -> P e. Cat )
40 15 oppccat 
 |-  ( P e. Cat -> ( oppCat ` P ) e. Cat )
41 38 39 40 3syl 
 |-  ( F e. ( D Func C ) -> ( oppCat ` P ) e. Cat )
42 37 simprd 
 |-  ( F e. ( D Func C ) -> C e. Cat )
43 1 oppccat 
 |-  ( C e. Cat -> O e. Cat )
44 16 oppccat 
 |-  ( O e. Cat -> ( oppCat ` O ) e. Cat )
45 42 43 44 3syl 
 |-  ( F e. ( D Func C ) -> ( oppCat ` O ) e. Cat )
46 34 36 30 32 38 41 42 45 fucpropd 
 |-  ( F e. ( D Func C ) -> ( D FuncCat C ) = ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) )
47 46 fveq2d 
 |-  ( F e. ( D Func C ) -> ( Homf ` ( D FuncCat C ) ) = ( Homf ` ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) ) )
48 46 fveq2d 
 |-  ( F e. ( D Func C ) -> ( comf ` ( D FuncCat C ) ) = ( comf ` ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) ) )
49 10 38 42 fuccat 
 |-  ( F e. ( D Func C ) -> ( D FuncCat C ) e. Cat )
50 46 49 eqeltrrd 
 |-  ( F e. ( D Func C ) -> ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) e. Cat )
51 30 32 47 48 42 45 49 50 uppropd 
 |-  ( F e. ( D Func C ) -> ( C UP ( D FuncCat C ) ) = ( ( oppCat ` O ) UP ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) ) )
52 30 32 34 36 42 45 38 41 diagpropd 
 |-  ( F e. ( D Func C ) -> ( C DiagFunc D ) = ( ( oppCat ` O ) DiagFunc ( oppCat ` P ) ) )
53 id 
 |-  ( F e. ( D Func C ) -> F e. ( D Func C ) )
54 2 1 53 oppfoppc2 
 |-  ( F e. ( D Func C ) -> ( oppFunc ` F ) e. ( P Func O ) )
55 3 54 eqeltrid 
 |-  ( F e. ( D Func C ) -> G e. ( P Func O ) )
56 relfunc 
 |-  Rel ( P Func O )
57 55 56 3 2oppf 
 |-  ( F e. ( D Func C ) -> ( oppFunc ` G ) = F )
58 57 eqcomd 
 |-  ( F e. ( D Func C ) -> F = ( oppFunc ` G ) )
59 51 52 58 oveq123d 
 |-  ( F e. ( D Func C ) -> ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) = ( ( ( oppCat ` O ) DiagFunc ( oppCat ` P ) ) ( ( oppCat ` O ) UP ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) ) ( oppFunc ` G ) ) )
60 59 breqd 
 |-  ( F e. ( D Func C ) -> ( x ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) m <-> x ( ( ( oppCat ` O ) DiagFunc ( oppCat ` P ) ) ( ( oppCat ` O ) UP ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) ) ( oppFunc ` G ) ) m ) )
61 12 28 60 pm5.21nd 
 |-  ( ph -> ( x ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) m <-> x ( ( ( oppCat ` O ) DiagFunc ( oppCat ` P ) ) ( ( oppCat ` O ) UP ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) ) ( oppFunc ` G ) ) m ) )
62 6 7 61 eqbrrdiv 
 |-  ( ph -> ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) = ( ( ( oppCat ` O ) DiagFunc ( oppCat ` P ) ) ( ( oppCat ` O ) UP ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) ) ( oppFunc ` G ) ) )
63 cmdfval2 
 |-  ( ( C Colimit D ) ` F ) = ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F )
64 cmdfval2 
 |-  ( ( ( oppCat ` O ) Colimit ( oppCat ` P ) ) ` ( oppFunc ` G ) ) = ( ( ( oppCat ` O ) DiagFunc ( oppCat ` P ) ) ( ( oppCat ` O ) UP ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) ) ( oppFunc ` G ) )
65 62 63 64 3eqtr4g 
 |-  ( ph -> ( ( C Colimit D ) ` F ) = ( ( ( oppCat ` O ) Colimit ( oppCat ` P ) ) ` ( oppFunc ` G ) ) )
66 eqid 
 |-  ( oppFunc ` G ) = ( oppFunc ` G )
67 19 a1i 
 |-  ( ph -> O e. _V )
68 17 a1i 
 |-  ( ph -> P e. _V )
69 16 15 66 67 68 lmddu 
 |-  ( ph -> ( ( O Limit P ) ` G ) = ( ( ( oppCat ` O ) Colimit ( oppCat ` P ) ) ` ( oppFunc ` G ) ) )
70 65 69 eqtr4d 
 |-  ( ph -> ( ( C Colimit D ) ` F ) = ( ( O Limit P ) ` G ) )