Theorem diagpropd

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

	Ref	Expression
Hypotheses	1stfpropd.1	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(A\right)={\mathrm{Hom}}_{𝑓}\left(B\right)$$
	1stfpropd.2	$$⊢\phi \to {\mathrm{comp}}_{𝑓}\left(A\right)={\mathrm{comp}}_{𝑓}\left(B\right)$$
	1stfpropd.3	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(D\right)$$
	1stfpropd.4	$$⊢\phi \to {\mathrm{comp}}_{𝑓}\left(C\right)={\mathrm{comp}}_{𝑓}\left(D\right)$$
	1stfpropd.a	$$⊢\phi \to A\in \mathrm{Cat}$$
	1stfpropd.b	$$⊢\phi \to B\in \mathrm{Cat}$$
	1stfpropd.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	1stfpropd.d	$$⊢\phi \to D\in \mathrm{Cat}$$
Assertion	diagpropd	$$⊢\phi \to A{\Delta }_{\mathrm{func}}C=B{\Delta }_{\mathrm{func}}D$$

Proof

Step	Hyp	Ref	Expression
1		1stfpropd.1	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(A\right)={\mathrm{Hom}}_{𝑓}\left(B\right)$$
2		1stfpropd.2	$$⊢\phi \to {\mathrm{comp}}_{𝑓}\left(A\right)={\mathrm{comp}}_{𝑓}\left(B\right)$$
3		1stfpropd.3	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(D\right)$$
4		1stfpropd.4	$$⊢\phi \to {\mathrm{comp}}_{𝑓}\left(C\right)={\mathrm{comp}}_{𝑓}\left(D\right)$$
5		1stfpropd.a	$$⊢\phi \to A\in \mathrm{Cat}$$
6		1stfpropd.b	$$⊢\phi \to B\in \mathrm{Cat}$$
7		1stfpropd.c	$$⊢\phi \to C\in \mathrm{Cat}$$
8		1stfpropd.d	$$⊢\phi \to D\in \mathrm{Cat}$$
9		eqid	$$⊢A{\times }_{c}C=A{\times }_{c}C$$
10		eqid	$$⊢A{1^{st}}_{F}C=A{1^{st}}_{F}C$$
11	9 5 7 10	1stfcl	$$⊢\phi \to A{1^{st}}_{F}C\in \left(\left(A{\times }_{c}C\right)\mathrm{Func}A\right)$$
12	1 2 3 4 5 6 7 8 11	curfpropd	$$⊢\phi \to ⟨A,C⟩{curry}_F\left(A{1^{st}}_{F}C\right)=⟨B,D⟩{curry}_F\left(A{1^{st}}_{F}C\right)$$
13		eqid	$$⊢A{\Delta }_{\mathrm{func}}C=A{\Delta }_{\mathrm{func}}C$$
14	13 5 7	diagval	$$⊢\phi \to A{\Delta }_{\mathrm{func}}C=⟨A,C⟩{curry}_F\left(A{1^{st}}_{F}C\right)$$
15		eqid	$$⊢B{\Delta }_{\mathrm{func}}D=B{\Delta }_{\mathrm{func}}D$$
16	15 6 8	diagval	$$⊢\phi \to B{\Delta }_{\mathrm{func}}D=⟨B,D⟩{curry}_F\left(B{1^{st}}_{F}D\right)$$
17	1 2 3 4 5 6 7 8	1stfpropd	$$⊢\phi \to A{1^{st}}_{F}C=B{1^{st}}_{F}D$$
18	17	oveq2d	$$⊢\phi \to ⟨B,D⟩{curry}_F\left(A{1^{st}}_{F}C\right)=⟨B,D⟩{curry}_F\left(B{1^{st}}_{F}D\right)$$
19	16 18	eqtr4d	$$⊢\phi \to B{\Delta }_{\mathrm{func}}D=⟨B,D⟩{curry}_F\left(A{1^{st}}_{F}C\right)$$
20	12 14 19	3eqtr4d	$$⊢\phi \to A{\Delta }_{\mathrm{func}}C=B{\Delta }_{\mathrm{func}}D$$