Metamath Proof Explorer

Theorem lmdpropd

Description: If the categories have the same set of objects, morphisms, and compositions, then they have the same limits. (Contributed by Zhi Wang, 20-Nov-2025)

Ref Expression
Hypotheses lmdpropd.1 ⊢ ( 𝜑 → ( Homf ‘ 𝐴 ) = ( Homf ‘ 𝐵 ) )
lmdpropd.2 ⊢ ( 𝜑 → ( compf ‘ 𝐴 ) = ( compf ‘ 𝐵 ) )
lmdpropd.3 ⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
lmdpropd.4 ⊢ ( 𝜑 → ( compf ‘ 𝐶 ) = ( compf ‘ 𝐷 ) )
lmdpropd.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
lmdpropd.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
lmdpropd.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
lmdpropd.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
Assertion lmdpropd ( 𝜑 → ( 𝐴 Limit 𝐶 ) = ( 𝐵 Limit 𝐷 ) )

Proof

Step Hyp Ref Expression
1 lmdpropd.1 ⊢ ( 𝜑 → ( Homf ‘ 𝐴 ) = ( Homf ‘ 𝐵 ) )
2 lmdpropd.2 ⊢ ( 𝜑 → ( compf ‘ 𝐴 ) = ( compf ‘ 𝐵 ) )
3 lmdpropd.3 ⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
4 lmdpropd.4 ⊢ ( 𝜑 → ( compf ‘ 𝐶 ) = ( compf ‘ 𝐷 ) )
5 lmdpropd.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
6 lmdpropd.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
7 lmdpropd.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
8 lmdpropd.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
9 3 4 1 2 7 8 5 6 funcpropd ⊢ ( 𝜑 → ( 𝐶 Func 𝐴 ) = ( 𝐷 Func 𝐵 ) )
10 1 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐶 Func 𝐴 ) ) → ( Homf ‘ 𝐴 ) = ( Homf ‘ 𝐵 ) )
11 10 oppchomfpropd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐶 Func 𝐴 ) ) → ( Homf ‘ ( oppCat ‘ 𝐴 ) ) = ( Homf ‘ ( oppCat ‘ 𝐵 ) ) )
12 2 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐶 Func 𝐴 ) ) → ( compf ‘ 𝐴 ) = ( compf ‘ 𝐵 ) )
13 10 12 oppccomfpropd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐶 Func 𝐴 ) ) → ( compf ‘ ( oppCat ‘ 𝐴 ) ) = ( compf ‘ ( oppCat ‘ 𝐵 ) ) )
14 3 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐶 Func 𝐴 ) ) → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
15 4 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐶 Func 𝐴 ) ) → ( compf ‘ 𝐶 ) = ( compf ‘ 𝐷 ) )
16 simpr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐶 Func 𝐴 ) ) → 𝑓 ∈ ( 𝐶 Func 𝐴 ) )
17 16 func1st2nd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐶 Func 𝐴 ) ) → ( 1st ‘ 𝑓 ) ( 𝐶 Func 𝐴 ) ( 2nd ‘ 𝑓 ) )
18 17 funcrcl2 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐶 Func 𝐴 ) ) → 𝐶 ∈ Cat )
19 9 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐶 Func 𝐴 ) ) → ( 𝐶 Func 𝐴 ) = ( 𝐷 Func 𝐵 ) )
20 16 19 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐶 Func 𝐴 ) ) → 𝑓 ∈ ( 𝐷 Func 𝐵 ) )
21 20 func1st2nd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐶 Func 𝐴 ) ) → ( 1st ‘ 𝑓 ) ( 𝐷 Func 𝐵 ) ( 2nd ‘ 𝑓 ) )
22 21 funcrcl2 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐶 Func 𝐴 ) ) → 𝐷 ∈ Cat )
23 17 funcrcl3 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐶 Func 𝐴 ) ) → 𝐴 ∈ Cat )
24 21 funcrcl3 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐶 Func 𝐴 ) ) → 𝐵 ∈ Cat )
25 14 15 10 12 18 22 23 24 fucpropd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐶 Func 𝐴 ) ) → ( 𝐶 FuncCat 𝐴 ) = ( 𝐷 FuncCat 𝐵 ) )
26 25 fveq2d ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐶 Func 𝐴 ) ) → ( Homf ‘ ( 𝐶 FuncCat 𝐴 ) ) = ( Homf ‘ ( 𝐷 FuncCat 𝐵 ) ) )
27 26 oppchomfpropd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐶 Func 𝐴 ) ) → ( Homf ‘ ( oppCat ‘ ( 𝐶 FuncCat 𝐴 ) ) ) = ( Homf ‘ ( oppCat ‘ ( 𝐷 FuncCat 𝐵 ) ) ) )
28 25 fveq2d ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐶 Func 𝐴 ) ) → ( compf ‘ ( 𝐶 FuncCat 𝐴 ) ) = ( compf ‘ ( 𝐷 FuncCat 𝐵 ) ) )
29 26 28 oppccomfpropd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐶 Func 𝐴 ) ) → ( compf ‘ ( oppCat ‘ ( 𝐶 FuncCat 𝐴 ) ) ) = ( compf ‘ ( oppCat ‘ ( 𝐷 FuncCat 𝐵 ) ) ) )
30 fvexd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐶 Func 𝐴 ) ) → ( oppCat ‘ 𝐴 ) ∈ V )
31 fvexd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐶 Func 𝐴 ) ) → ( oppCat ‘ 𝐵 ) ∈ V )
32 fvexd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐶 Func 𝐴 ) ) → ( oppCat ‘ ( 𝐶 FuncCat 𝐴 ) ) ∈ V )
33 fvexd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐶 Func 𝐴 ) ) → ( oppCat ‘ ( 𝐷 FuncCat 𝐵 ) ) ∈ V )
34 11 13 27 29 30 31 32 33 uppropd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐶 Func 𝐴 ) ) → ( ( oppCat ‘ 𝐴 ) UP ( oppCat ‘ ( 𝐶 FuncCat 𝐴 ) ) ) = ( ( oppCat ‘ 𝐵 ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐵 ) ) ) )
35 10 12 14 15 23 24 18 22 diagpropd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐶 Func 𝐴 ) ) → ( 𝐴 Δfunc 𝐶 ) = ( 𝐵 Δfunc 𝐷 ) )
36 35 fveq2d ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐶 Func 𝐴 ) ) → ( oppFunc ‘ ( 𝐴 Δfunc 𝐶 ) ) = ( oppFunc ‘ ( 𝐵 Δfunc 𝐷 ) ) )
37 eqidd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐶 Func 𝐴 ) ) → 𝑓 = 𝑓 )
38 34 36 37 oveq123d ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐶 Func 𝐴 ) ) → ( ( oppFunc ‘ ( 𝐴 Δfunc 𝐶 ) ) ( ( oppCat ‘ 𝐴 ) UP ( oppCat ‘ ( 𝐶 FuncCat 𝐴 ) ) ) 𝑓 ) = ( ( oppFunc ‘ ( 𝐵 Δfunc 𝐷 ) ) ( ( oppCat ‘ 𝐵 ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐵 ) ) ) 𝑓 ) )
39 9 38 mpteq12dva ⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝐶 Func 𝐴 ) ↦ ( ( oppFunc ‘ ( 𝐴 Δfunc 𝐶 ) ) ( ( oppCat ‘ 𝐴 ) UP ( oppCat ‘ ( 𝐶 FuncCat 𝐴 ) ) ) 𝑓 ) ) = ( 𝑓 ∈ ( 𝐷 Func 𝐵 ) ↦ ( ( oppFunc ‘ ( 𝐵 Δfunc 𝐷 ) ) ( ( oppCat ‘ 𝐵 ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐵 ) ) ) 𝑓 ) ) )
40 lmdfval ⊢ ( 𝐴 Limit 𝐶 ) = ( 𝑓 ∈ ( 𝐶 Func 𝐴 ) ↦ ( ( oppFunc ‘ ( 𝐴 Δfunc 𝐶 ) ) ( ( oppCat ‘ 𝐴 ) UP ( oppCat ‘ ( 𝐶 FuncCat 𝐴 ) ) ) 𝑓 ) )
41 lmdfval ⊢ ( 𝐵 Limit 𝐷 ) = ( 𝑓 ∈ ( 𝐷 Func 𝐵 ) ↦ ( ( oppFunc ‘ ( 𝐵 Δfunc 𝐷 ) ) ( ( oppCat ‘ 𝐵 ) UP ( oppCat ‘ ( 𝐷 FuncCat 𝐵 ) ) ) 𝑓 ) )
42 39 40 41 3eqtr4g ⊢ ( 𝜑 → ( 𝐴 Limit 𝐶 ) = ( 𝐵 Limit 𝐷 ) )