Theorem cmdpropd

Description: If the categories have the same set of objects, morphisms, and compositions, then they have the same colimits. (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	cmdpropd	⊢ ( 𝜑 → ( 𝐴 Colimit 𝐶 ) = ( 𝐵 Colimit 𝐷 ) )

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	2	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐶 Func 𝐴 ) ) → ( compf ‘ 𝐴 ) = ( compf ‘ 𝐵 ) )
12	3	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐶 Func 𝐴 ) ) → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
13	4	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐶 Func 𝐴 ) ) → ( compf ‘ 𝐶 ) = ( compf ‘ 𝐷 ) )
14		simpr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐶 Func 𝐴 ) ) → 𝑓 ∈ ( 𝐶 Func 𝐴 ) )
15	14	func1st2nd	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐶 Func 𝐴 ) ) → ( 1st ‘ 𝑓 ) ( 𝐶 Func 𝐴 ) ( 2nd ‘ 𝑓 ) )
16	15	funcrcl2	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐶 Func 𝐴 ) ) → 𝐶 ∈ Cat )
17	9	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐶 Func 𝐴 ) ) → ( 𝐶 Func 𝐴 ) = ( 𝐷 Func 𝐵 ) )
18	14 17	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐶 Func 𝐴 ) ) → 𝑓 ∈ ( 𝐷 Func 𝐵 ) )
19	18	func1st2nd	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐶 Func 𝐴 ) ) → ( 1st ‘ 𝑓 ) ( 𝐷 Func 𝐵 ) ( 2nd ‘ 𝑓 ) )
20	19	funcrcl2	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐶 Func 𝐴 ) ) → 𝐷 ∈ Cat )
21	15	funcrcl3	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐶 Func 𝐴 ) ) → 𝐴 ∈ Cat )
22	19	funcrcl3	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐶 Func 𝐴 ) ) → 𝐵 ∈ Cat )
23	12 13 10 11 16 20 21 22	fucpropd	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐶 Func 𝐴 ) ) → ( 𝐶 FuncCat 𝐴 ) = ( 𝐷 FuncCat 𝐵 ) )
24	23	fveq2d	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐶 Func 𝐴 ) ) → ( Homf ‘ ( 𝐶 FuncCat 𝐴 ) ) = ( Homf ‘ ( 𝐷 FuncCat 𝐵 ) ) )
25	23	fveq2d	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐶 Func 𝐴 ) ) → ( compf ‘ ( 𝐶 FuncCat 𝐴 ) ) = ( compf ‘ ( 𝐷 FuncCat 𝐵 ) ) )
26		eqid	⊢ ( 𝐶 FuncCat 𝐴 ) = ( 𝐶 FuncCat 𝐴 )
27	26 16 21	fuccat	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐶 Func 𝐴 ) ) → ( 𝐶 FuncCat 𝐴 ) ∈ Cat )
28	23 27	eqeltrrd	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐶 Func 𝐴 ) ) → ( 𝐷 FuncCat 𝐵 ) ∈ Cat )
29	10 11 24 25 21 22 27 28	uppropd	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐶 Func 𝐴 ) ) → ( 𝐴 UP ( 𝐶 FuncCat 𝐴 ) ) = ( 𝐵 UP ( 𝐷 FuncCat 𝐵 ) ) )
30	10 11 12 13 21 22 16 20	diagpropd	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐶 Func 𝐴 ) ) → ( 𝐴 Δfunc 𝐶 ) = ( 𝐵 Δfunc 𝐷 ) )
31		eqidd	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐶 Func 𝐴 ) ) → 𝑓 = 𝑓 )
32	29 30 31	oveq123d	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐶 Func 𝐴 ) ) → ( ( 𝐴 Δfunc 𝐶 ) ( 𝐴 UP ( 𝐶 FuncCat 𝐴 ) ) 𝑓 ) = ( ( 𝐵 Δfunc 𝐷 ) ( 𝐵 UP ( 𝐷 FuncCat 𝐵 ) ) 𝑓 ) )
33	9 32	mpteq12dva	⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝐶 Func 𝐴 ) ↦ ( ( 𝐴 Δfunc 𝐶 ) ( 𝐴 UP ( 𝐶 FuncCat 𝐴 ) ) 𝑓 ) ) = ( 𝑓 ∈ ( 𝐷 Func 𝐵 ) ↦ ( ( 𝐵 Δfunc 𝐷 ) ( 𝐵 UP ( 𝐷 FuncCat 𝐵 ) ) 𝑓 ) ) )
34		cmdfval	⊢ ( 𝐴 Colimit 𝐶 ) = ( 𝑓 ∈ ( 𝐶 Func 𝐴 ) ↦ ( ( 𝐴 Δfunc 𝐶 ) ( 𝐴 UP ( 𝐶 FuncCat 𝐴 ) ) 𝑓 ) )
35		cmdfval	⊢ ( 𝐵 Colimit 𝐷 ) = ( 𝑓 ∈ ( 𝐷 Func 𝐵 ) ↦ ( ( 𝐵 Δfunc 𝐷 ) ( 𝐵 UP ( 𝐷 FuncCat 𝐵 ) ) 𝑓 ) )
36	33 34 35	3eqtr4g	⊢ ( 𝜑 → ( 𝐴 Colimit 𝐶 ) = ( 𝐵 Colimit 𝐷 ) )