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	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(A\right)={\mathrm{Hom}}_{𝑓}\left(B\right)$$
	lmdpropd.2	$$⊢\phi \to {\mathrm{comp}}_{𝑓}\left(A\right)={\mathrm{comp}}_{𝑓}\left(B\right)$$
	lmdpropd.3	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(D\right)$$
	lmdpropd.4	$$⊢\phi \to {\mathrm{comp}}_{𝑓}\left(C\right)={\mathrm{comp}}_{𝑓}\left(D\right)$$
	lmdpropd.a	$$⊢\phi \to A\in V$$
	lmdpropd.b	$$⊢\phi \to B\in V$$
	lmdpropd.c	$$⊢\phi \to C\in V$$
	lmdpropd.d	$$⊢\phi \to D\in V$$
Assertion	cmdpropd	Could not format assertion : No typesetting found for |- ( ph -> ( A Colimit C ) = ( B Colimit D ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		lmdpropd.1	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(A\right)={\mathrm{Hom}}_{𝑓}\left(B\right)$$
2		lmdpropd.2	$$⊢\phi \to {\mathrm{comp}}_{𝑓}\left(A\right)={\mathrm{comp}}_{𝑓}\left(B\right)$$
3		lmdpropd.3	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(D\right)$$
4		lmdpropd.4	$$⊢\phi \to {\mathrm{comp}}_{𝑓}\left(C\right)={\mathrm{comp}}_{𝑓}\left(D\right)$$
5		lmdpropd.a	$$⊢\phi \to A\in V$$
6		lmdpropd.b	$$⊢\phi \to B\in V$$
7		lmdpropd.c	$$⊢\phi \to C\in V$$
8		lmdpropd.d	$$⊢\phi \to D\in V$$
9	3 4 1 2 7 8 5 6	funcpropd	$$⊢\phi \to C\mathrm{Func}A=D\mathrm{Func}B$$
10	1	adantr	$$⊢\left(\phi \wedge f\in \left(C\mathrm{Func}A\right)\right)\to {\mathrm{Hom}}_{𝑓}\left(A\right)={\mathrm{Hom}}_{𝑓}\left(B\right)$$
11	2	adantr	$$⊢\left(\phi \wedge f\in \left(C\mathrm{Func}A\right)\right)\to {\mathrm{comp}}_{𝑓}\left(A\right)={\mathrm{comp}}_{𝑓}\left(B\right)$$
12	3	adantr	$$⊢\left(\phi \wedge f\in \left(C\mathrm{Func}A\right)\right)\to {\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(D\right)$$
13	4	adantr	$$⊢\left(\phi \wedge f\in \left(C\mathrm{Func}A\right)\right)\to {\mathrm{comp}}_{𝑓}\left(C\right)={\mathrm{comp}}_{𝑓}\left(D\right)$$
14		simpr	$$⊢\left(\phi \wedge f\in \left(C\mathrm{Func}A\right)\right)\to f\in \left(C\mathrm{Func}A\right)$$
15	14	func1st2nd	$$⊢\left(\phi \wedge f\in \left(C\mathrm{Func}A\right)\right)\to 1^{st}\left(f\right)\left(C\mathrm{Func}A\right)2^{nd}\left(f\right)$$
16	15	funcrcl2	$$⊢\left(\phi \wedge f\in \left(C\mathrm{Func}A\right)\right)\to C\in \mathrm{Cat}$$
17	9	adantr	$$⊢\left(\phi \wedge f\in \left(C\mathrm{Func}A\right)\right)\to C\mathrm{Func}A=D\mathrm{Func}B$$
18	14 17	eleqtrd	$$⊢\left(\phi \wedge f\in \left(C\mathrm{Func}A\right)\right)\to f\in \left(D\mathrm{Func}B\right)$$
19	18	func1st2nd	$$⊢\left(\phi \wedge f\in \left(C\mathrm{Func}A\right)\right)\to 1^{st}\left(f\right)\left(D\mathrm{Func}B\right)2^{nd}\left(f\right)$$
20	19	funcrcl2	$$⊢\left(\phi \wedge f\in \left(C\mathrm{Func}A\right)\right)\to D\in \mathrm{Cat}$$
21	15	funcrcl3	$$⊢\left(\phi \wedge f\in \left(C\mathrm{Func}A\right)\right)\to A\in \mathrm{Cat}$$
22	19	funcrcl3	$$⊢\left(\phi \wedge f\in \left(C\mathrm{Func}A\right)\right)\to B\in \mathrm{Cat}$$
23	12 13 10 11 16 20 21 22	fucpropd	$$⊢\left(\phi \wedge f\in \left(C\mathrm{Func}A\right)\right)\to C\mathrm{FuncCat}A=D\mathrm{FuncCat}B$$
24	23	fveq2d	$$⊢\left(\phi \wedge f\in \left(C\mathrm{Func}A\right)\right)\to {\mathrm{Hom}}_{𝑓}\left(C\mathrm{FuncCat}A\right)={\mathrm{Hom}}_{𝑓}\left(D\mathrm{FuncCat}B\right)$$
25	23	fveq2d	$$⊢\left(\phi \wedge f\in \left(C\mathrm{Func}A\right)\right)\to {\mathrm{comp}}_{𝑓}\left(C\mathrm{FuncCat}A\right)={\mathrm{comp}}_{𝑓}\left(D\mathrm{FuncCat}B\right)$$
26		eqid	$$⊢C\mathrm{FuncCat}A=C\mathrm{FuncCat}A$$
27	26 16 21	fuccat	$$⊢\left(\phi \wedge f\in \left(C\mathrm{Func}A\right)\right)\to C\mathrm{FuncCat}A\in \mathrm{Cat}$$
28	23 27	eqeltrrd	$$⊢\left(\phi \wedge f\in \left(C\mathrm{Func}A\right)\right)\to D\mathrm{FuncCat}B\in \mathrm{Cat}$$
29	10 11 24 25 21 22 27 28	uppropd	Could not format ( ( ph /\ f e. ( C Func A ) ) -> ( A UP ( C FuncCat A ) ) = ( B UP ( D FuncCat B ) ) ) : No typesetting found for |- ( ( ph /\ f e. ( C Func A ) ) -> ( A UP ( C FuncCat A ) ) = ( B UP ( D FuncCat B ) ) ) with typecode |-
30	10 11 12 13 21 22 16 20	diagpropd	$$⊢\left(\phi \wedge f\in \left(C\mathrm{Func}A\right)\right)\to A{\Delta }_{\mathrm{func}}C=B{\Delta }_{\mathrm{func}}D$$
31		eqidd	$$⊢\left(\phi \wedge f\in \left(C\mathrm{Func}A\right)\right)\to f=f$$
32	29 30 31	oveq123d	Could not format ( ( ph /\ f e. ( C Func A ) ) -> ( ( A DiagFunc C ) ( A UP ( C FuncCat A ) ) f ) = ( ( B DiagFunc D ) ( B UP ( D FuncCat B ) ) f ) ) : No typesetting found for |- ( ( ph /\ f e. ( C Func A ) ) -> ( ( A DiagFunc C ) ( A UP ( C FuncCat A ) ) f ) = ( ( B DiagFunc D ) ( B UP ( D FuncCat B ) ) f ) ) with typecode |-
33	9 32	mpteq12dva	Could not format ( ph -> ( f e. ( C Func A ) |-> ( ( A DiagFunc C ) ( A UP ( C FuncCat A ) ) f ) ) = ( f e. ( D Func B ) |-> ( ( B DiagFunc D ) ( B UP ( D FuncCat B ) ) f ) ) ) : No typesetting found for |- ( ph -> ( f e. ( C Func A ) |-> ( ( A DiagFunc C ) ( A UP ( C FuncCat A ) ) f ) ) = ( f e. ( D Func B ) |-> ( ( B DiagFunc D ) ( B UP ( D FuncCat B ) ) f ) ) ) with typecode |-
34		cmdfval	Could not format ( A Colimit C ) = ( f e. ( C Func A ) |-> ( ( A DiagFunc C ) ( A UP ( C FuncCat A ) ) f ) ) : No typesetting found for |- ( A Colimit C ) = ( f e. ( C Func A ) |-> ( ( A DiagFunc C ) ( A UP ( C FuncCat A ) ) f ) ) with typecode |-
35		cmdfval	Could not format ( B Colimit D ) = ( f e. ( D Func B ) |-> ( ( B DiagFunc D ) ( B UP ( D FuncCat B ) ) f ) ) : No typesetting found for |- ( B Colimit D ) = ( f e. ( D Func B ) |-> ( ( B DiagFunc D ) ( B UP ( D FuncCat B ) ) f ) ) with typecode |-
36	33 34 35	3eqtr4g	Could not format ( ph -> ( A Colimit C ) = ( B Colimit D ) ) : No typesetting found for |- ( ph -> ( A Colimit C ) = ( B Colimit D ) ) with typecode |-