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 ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
lmddu.p ⊢ 𝑃 = ( oppCat ‘ 𝐷 )
lmddu.g ⊢ 𝐺 = ( oppFunc ‘ 𝐹 )
lmddu.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
lmddu.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑊 )
Assertion cmddu ( 𝜑 → ( ( 𝐶 Colimit 𝐷 ) ‘ 𝐹 ) = ( ( 𝑂 Limit 𝑃 ) ‘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 lmddu.o ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
2 lmddu.p ⊢ 𝑃 = ( oppCat ‘ 𝐷 )
3 lmddu.g ⊢ 𝐺 = ( oppFunc ‘ 𝐹 )
4 lmddu.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
5 lmddu.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑊 )
6 relup ⊢ Rel ( ( 𝐶 Δfunc 𝐷 ) ( 𝐶 UP ( 𝐷 FuncCat 𝐶 ) ) 𝐹 )
7 relup ⊢ Rel ( ( ( oppCat ‘ 𝑂 ) Δfunc ( oppCat ‘ 𝑃 ) ) ( ( oppCat ‘ 𝑂 ) UP ( ( oppCat ‘ 𝑃 ) FuncCat ( oppCat ‘ 𝑂 ) ) ) ( oppFunc ‘ 𝐺 ) )
8 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ( ( 𝐶 Δfunc 𝐷 ) ( 𝐶 UP ( 𝐷 FuncCat 𝐶 ) ) 𝐹 ) 𝑚 ) → 𝑥 ( ( 𝐶 Δfunc 𝐷 ) ( 𝐶 UP ( 𝐷 FuncCat 𝐶 ) ) 𝐹 ) 𝑚 )
9 8 up1st2nd ⊢ ( ( 𝜑 ∧ 𝑥 ( ( 𝐶 Δfunc 𝐷 ) ( 𝐶 UP ( 𝐷 FuncCat 𝐶 ) ) 𝐹 ) 𝑚 ) → 𝑥 ( ⟨ ( 1st ‘ ( 𝐶 Δfunc 𝐷 ) ) , ( 2nd ‘ ( 𝐶 Δfunc 𝐷 ) ) ⟩ ( 𝐶 UP ( 𝐷 FuncCat 𝐶 ) ) 𝐹 ) 𝑚 )
10 eqid ⊢ ( 𝐷 FuncCat 𝐶 ) = ( 𝐷 FuncCat 𝐶 )
11 10 fucbas ⊢ ( 𝐷 Func 𝐶 ) = ( Base ‘ ( 𝐷 FuncCat 𝐶 ) )
12 9 11 uprcl3 ⊢ ( ( 𝜑 ∧ 𝑥 ( ( 𝐶 Δfunc 𝐷 ) ( 𝐶 UP ( 𝐷 FuncCat 𝐶 ) ) 𝐹 ) 𝑚 ) → 𝐹 ∈ ( 𝐷 Func 𝐶 ) )
13 5 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ( ( ( oppCat ‘ 𝑂 ) Δfunc ( oppCat ‘ 𝑃 ) ) ( ( oppCat ‘ 𝑂 ) UP ( ( oppCat ‘ 𝑃 ) FuncCat ( oppCat ‘ 𝑂 ) ) ) ( oppFunc ‘ 𝐺 ) ) 𝑚 ) → 𝐷 ∈ 𝑊 )
14 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ( ( ( oppCat ‘ 𝑂 ) Δfunc ( oppCat ‘ 𝑃 ) ) ( ( oppCat ‘ 𝑂 ) UP ( ( oppCat ‘ 𝑃 ) FuncCat ( oppCat ‘ 𝑂 ) ) ) ( oppFunc ‘ 𝐺 ) ) 𝑚 ) → 𝐶 ∈ 𝑉 )
15 eqid ⊢ ( oppCat ‘ 𝑃 ) = ( oppCat ‘ 𝑃 )
16 eqid ⊢ ( oppCat ‘ 𝑂 ) = ( oppCat ‘ 𝑂 )
17 2 fvexi ⊢ 𝑃 ∈ V
18 17 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ( ( ( oppCat ‘ 𝑂 ) Δfunc ( oppCat ‘ 𝑃 ) ) ( ( oppCat ‘ 𝑂 ) UP ( ( oppCat ‘ 𝑃 ) FuncCat ( oppCat ‘ 𝑂 ) ) ) ( oppFunc ‘ 𝐺 ) ) 𝑚 ) → 𝑃 ∈ V )
19 1 fvexi ⊢ 𝑂 ∈ V
20 19 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ( ( ( oppCat ‘ 𝑂 ) Δfunc ( oppCat ‘ 𝑃 ) ) ( ( oppCat ‘ 𝑂 ) UP ( ( oppCat ‘ 𝑃 ) FuncCat ( oppCat ‘ 𝑂 ) ) ) ( oppFunc ‘ 𝐺 ) ) 𝑚 ) → 𝑂 ∈ V )
21 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ( ( ( oppCat ‘ 𝑂 ) Δfunc ( oppCat ‘ 𝑃 ) ) ( ( oppCat ‘ 𝑂 ) UP ( ( oppCat ‘ 𝑃 ) FuncCat ( oppCat ‘ 𝑂 ) ) ) ( oppFunc ‘ 𝐺 ) ) 𝑚 ) → 𝑥 ( ( ( oppCat ‘ 𝑂 ) Δfunc ( oppCat ‘ 𝑃 ) ) ( ( oppCat ‘ 𝑂 ) UP ( ( oppCat ‘ 𝑃 ) FuncCat ( oppCat ‘ 𝑂 ) ) ) ( oppFunc ‘ 𝐺 ) ) 𝑚 )
22 21 up1st2nd ⊢ ( ( 𝜑 ∧ 𝑥 ( ( ( oppCat ‘ 𝑂 ) Δfunc ( oppCat ‘ 𝑃 ) ) ( ( oppCat ‘ 𝑂 ) UP ( ( oppCat ‘ 𝑃 ) FuncCat ( oppCat ‘ 𝑂 ) ) ) ( oppFunc ‘ 𝐺 ) ) 𝑚 ) → 𝑥 ( ⟨ ( 1st ‘ ( ( oppCat ‘ 𝑂 ) Δfunc ( oppCat ‘ 𝑃 ) ) ) , ( 2nd ‘ ( ( oppCat ‘ 𝑂 ) Δfunc ( oppCat ‘ 𝑃 ) ) ) ⟩ ( ( oppCat ‘ 𝑂 ) UP ( ( oppCat ‘ 𝑃 ) FuncCat ( oppCat ‘ 𝑂 ) ) ) ( oppFunc ‘ 𝐺 ) ) 𝑚 )
23 eqid ⊢ ( ( oppCat ‘ 𝑃 ) FuncCat ( oppCat ‘ 𝑂 ) ) = ( ( oppCat ‘ 𝑃 ) FuncCat ( oppCat ‘ 𝑂 ) )
24 23 fucbas ⊢ ( ( oppCat ‘ 𝑃 ) Func ( oppCat ‘ 𝑂 ) ) = ( Base ‘ ( ( oppCat ‘ 𝑃 ) FuncCat ( oppCat ‘ 𝑂 ) ) )
25 22 24 uprcl3 ⊢ ( ( 𝜑 ∧ 𝑥 ( ( ( oppCat ‘ 𝑂 ) Δfunc ( oppCat ‘ 𝑃 ) ) ( ( oppCat ‘ 𝑂 ) UP ( ( oppCat ‘ 𝑃 ) FuncCat ( oppCat ‘ 𝑂 ) ) ) ( oppFunc ‘ 𝐺 ) ) 𝑚 ) → ( oppFunc ‘ 𝐺 ) ∈ ( ( oppCat ‘ 𝑃 ) Func ( oppCat ‘ 𝑂 ) ) )
26 15 16 18 20 25 funcoppc5 ⊢ ( ( 𝜑 ∧ 𝑥 ( ( ( oppCat ‘ 𝑂 ) Δfunc ( oppCat ‘ 𝑃 ) ) ( ( oppCat ‘ 𝑂 ) UP ( ( oppCat ‘ 𝑃 ) FuncCat ( oppCat ‘ 𝑂 ) ) ) ( oppFunc ‘ 𝐺 ) ) 𝑚 ) → 𝐺 ∈ ( 𝑃 Func 𝑂 ) )
27 3 26 eqeltrrid ⊢ ( ( 𝜑 ∧ 𝑥 ( ( ( oppCat ‘ 𝑂 ) Δfunc ( oppCat ‘ 𝑃 ) ) ( ( oppCat ‘ 𝑂 ) UP ( ( oppCat ‘ 𝑃 ) FuncCat ( oppCat ‘ 𝑂 ) ) ) ( oppFunc ‘ 𝐺 ) ) 𝑚 ) → ( oppFunc ‘ 𝐹 ) ∈ ( 𝑃 Func 𝑂 ) )
28 2 1 13 14 27 funcoppc5 ⊢ ( ( 𝜑 ∧ 𝑥 ( ( ( oppCat ‘ 𝑂 ) Δfunc ( oppCat ‘ 𝑃 ) ) ( ( oppCat ‘ 𝑂 ) UP ( ( oppCat ‘ 𝑃 ) FuncCat ( oppCat ‘ 𝑂 ) ) ) ( oppFunc ‘ 𝐺 ) ) 𝑚 ) → 𝐹 ∈ ( 𝐷 Func 𝐶 ) )
29 1 2oppchomf ⊢ ( Homf ‘ 𝐶 ) = ( Homf ‘ ( oppCat ‘ 𝑂 ) )
30 29 a1i ⊢ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) → ( Homf ‘ 𝐶 ) = ( Homf ‘ ( oppCat ‘ 𝑂 ) ) )
31 1 2oppccomf ⊢ ( compf ‘ 𝐶 ) = ( compf ‘ ( oppCat ‘ 𝑂 ) )
32 31 a1i ⊢ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) → ( compf ‘ 𝐶 ) = ( compf ‘ ( oppCat ‘ 𝑂 ) ) )
33 2 2oppchomf ⊢ ( Homf ‘ 𝐷 ) = ( Homf ‘ ( oppCat ‘ 𝑃 ) )
34 33 a1i ⊢ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) → ( Homf ‘ 𝐷 ) = ( Homf ‘ ( oppCat ‘ 𝑃 ) ) )
35 2 2oppccomf ⊢ ( compf ‘ 𝐷 ) = ( compf ‘ ( oppCat ‘ 𝑃 ) )
36 35 a1i ⊢ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) → ( compf ‘ 𝐷 ) = ( compf ‘ ( oppCat ‘ 𝑃 ) ) )
37 funcrcl ⊢ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) → ( 𝐷 ∈ Cat ∧ 𝐶 ∈ Cat ) )
38 37 simpld ⊢ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) → 𝐷 ∈ Cat )
39 2 oppccat ⊢ ( 𝐷 ∈ Cat → 𝑃 ∈ Cat )
40 15 oppccat ⊢ ( 𝑃 ∈ Cat → ( oppCat ‘ 𝑃 ) ∈ Cat )
41 38 39 40 3syl ⊢ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) → ( oppCat ‘ 𝑃 ) ∈ Cat )
42 37 simprd ⊢ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) → 𝐶 ∈ Cat )
43 1 oppccat ⊢ ( 𝐶 ∈ Cat → 𝑂 ∈ Cat )
44 16 oppccat ⊢ ( 𝑂 ∈ Cat → ( oppCat ‘ 𝑂 ) ∈ Cat )
45 42 43 44 3syl ⊢ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) → ( oppCat ‘ 𝑂 ) ∈ Cat )
46 34 36 30 32 38 41 42 45 fucpropd ⊢ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) → ( 𝐷 FuncCat 𝐶 ) = ( ( oppCat ‘ 𝑃 ) FuncCat ( oppCat ‘ 𝑂 ) ) )
47 46 fveq2d ⊢ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) → ( Homf ‘ ( 𝐷 FuncCat 𝐶 ) ) = ( Homf ‘ ( ( oppCat ‘ 𝑃 ) FuncCat ( oppCat ‘ 𝑂 ) ) ) )
48 46 fveq2d ⊢ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) → ( compf ‘ ( 𝐷 FuncCat 𝐶 ) ) = ( compf ‘ ( ( oppCat ‘ 𝑃 ) FuncCat ( oppCat ‘ 𝑂 ) ) ) )
49 10 38 42 fuccat ⊢ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) → ( 𝐷 FuncCat 𝐶 ) ∈ Cat )
50 46 49 eqeltrrd ⊢ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) → ( ( oppCat ‘ 𝑃 ) FuncCat ( oppCat ‘ 𝑂 ) ) ∈ Cat )
51 30 32 47 48 42 45 49 50 uppropd ⊢ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) → ( 𝐶 UP ( 𝐷 FuncCat 𝐶 ) ) = ( ( oppCat ‘ 𝑂 ) UP ( ( oppCat ‘ 𝑃 ) FuncCat ( oppCat ‘ 𝑂 ) ) ) )
52 30 32 34 36 42 45 38 41 diagpropd ⊢ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) → ( 𝐶 Δfunc 𝐷 ) = ( ( oppCat ‘ 𝑂 ) Δfunc ( oppCat ‘ 𝑃 ) ) )
53 id ⊢ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) → 𝐹 ∈ ( 𝐷 Func 𝐶 ) )
54 2 1 53 oppfoppc2 ⊢ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) → ( oppFunc ‘ 𝐹 ) ∈ ( 𝑃 Func 𝑂 ) )
55 3 54 eqeltrid ⊢ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) → 𝐺 ∈ ( 𝑃 Func 𝑂 ) )
56 relfunc ⊢ Rel ( 𝑃 Func 𝑂 )
57 55 56 3 2oppf ⊢ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) → ( oppFunc ‘ 𝐺 ) = 𝐹 )
58 57 eqcomd ⊢ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) → 𝐹 = ( oppFunc ‘ 𝐺 ) )
59 51 52 58 oveq123d ⊢ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) → ( ( 𝐶 Δfunc 𝐷 ) ( 𝐶 UP ( 𝐷 FuncCat 𝐶 ) ) 𝐹 ) = ( ( ( oppCat ‘ 𝑂 ) Δfunc ( oppCat ‘ 𝑃 ) ) ( ( oppCat ‘ 𝑂 ) UP ( ( oppCat ‘ 𝑃 ) FuncCat ( oppCat ‘ 𝑂 ) ) ) ( oppFunc ‘ 𝐺 ) ) )
60 59 breqd ⊢ ( 𝐹 ∈ ( 𝐷 Func 𝐶 ) → ( 𝑥 ( ( 𝐶 Δfunc 𝐷 ) ( 𝐶 UP ( 𝐷 FuncCat 𝐶 ) ) 𝐹 ) 𝑚 ↔ 𝑥 ( ( ( oppCat ‘ 𝑂 ) Δfunc ( oppCat ‘ 𝑃 ) ) ( ( oppCat ‘ 𝑂 ) UP ( ( oppCat ‘ 𝑃 ) FuncCat ( oppCat ‘ 𝑂 ) ) ) ( oppFunc ‘ 𝐺 ) ) 𝑚 ) )
61 12 28 60 pm5.21nd ⊢ ( 𝜑 → ( 𝑥 ( ( 𝐶 Δfunc 𝐷 ) ( 𝐶 UP ( 𝐷 FuncCat 𝐶 ) ) 𝐹 ) 𝑚 ↔ 𝑥 ( ( ( oppCat ‘ 𝑂 ) Δfunc ( oppCat ‘ 𝑃 ) ) ( ( oppCat ‘ 𝑂 ) UP ( ( oppCat ‘ 𝑃 ) FuncCat ( oppCat ‘ 𝑂 ) ) ) ( oppFunc ‘ 𝐺 ) ) 𝑚 ) )
62 6 7 61 eqbrrdiv ⊢ ( 𝜑 → ( ( 𝐶 Δfunc 𝐷 ) ( 𝐶 UP ( 𝐷 FuncCat 𝐶 ) ) 𝐹 ) = ( ( ( oppCat ‘ 𝑂 ) Δfunc ( oppCat ‘ 𝑃 ) ) ( ( oppCat ‘ 𝑂 ) UP ( ( oppCat ‘ 𝑃 ) FuncCat ( oppCat ‘ 𝑂 ) ) ) ( oppFunc ‘ 𝐺 ) ) )
63 cmdfval2 ⊢ ( ( 𝐶 Colimit 𝐷 ) ‘ 𝐹 ) = ( ( 𝐶 Δfunc 𝐷 ) ( 𝐶 UP ( 𝐷 FuncCat 𝐶 ) ) 𝐹 )
64 cmdfval2 ⊢ ( ( ( oppCat ‘ 𝑂 ) Colimit ( oppCat ‘ 𝑃 ) ) ‘ ( oppFunc ‘ 𝐺 ) ) = ( ( ( oppCat ‘ 𝑂 ) Δfunc ( oppCat ‘ 𝑃 ) ) ( ( oppCat ‘ 𝑂 ) UP ( ( oppCat ‘ 𝑃 ) FuncCat ( oppCat ‘ 𝑂 ) ) ) ( oppFunc ‘ 𝐺 ) )
65 62 63 64 3eqtr4g ⊢ ( 𝜑 → ( ( 𝐶 Colimit 𝐷 ) ‘ 𝐹 ) = ( ( ( oppCat ‘ 𝑂 ) Colimit ( oppCat ‘ 𝑃 ) ) ‘ ( oppFunc ‘ 𝐺 ) ) )
66 eqid ⊢ ( oppFunc ‘ 𝐺 ) = ( oppFunc ‘ 𝐺 )
67 19 a1i ⊢ ( 𝜑 → 𝑂 ∈ V )
68 17 a1i ⊢ ( 𝜑 → 𝑃 ∈ V )
69 16 15 66 67 68 lmddu ⊢ ( 𝜑 → ( ( 𝑂 Limit 𝑃 ) ‘ 𝐺 ) = ( ( ( oppCat ‘ 𝑂 ) Colimit ( oppCat ‘ 𝑃 ) ) ‘ ( oppFunc ‘ 𝐺 ) ) )
70 65 69 eqtr4d ⊢ ( 𝜑 → ( ( 𝐶 Colimit 𝐷 ) ‘ 𝐹 ) = ( ( 𝑂 Limit 𝑃 ) ‘ 𝐺 ) )