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	|- ( ph -> ( Homf ` A ) = ( Homf ` B ) )
	1stfpropd.2	|- ( ph -> ( comf ` A ) = ( comf ` B ) )
	1stfpropd.3	|- ( ph -> ( Homf ` C ) = ( Homf ` D ) )
	1stfpropd.4	|- ( ph -> ( comf ` C ) = ( comf ` D ) )
	1stfpropd.a	|- ( ph -> A e. Cat )
	1stfpropd.b	|- ( ph -> B e. Cat )
	1stfpropd.c	|- ( ph -> C e. Cat )
	1stfpropd.d	|- ( ph -> D e. Cat )
Assertion	diagpropd	|- ( ph -> ( A DiagFunc C ) = ( B DiagFunc D ) )

Proof

Step	Hyp	Ref	Expression
1		1stfpropd.1	|- ( ph -> ( Homf ` A ) = ( Homf ` B ) )
2		1stfpropd.2	|- ( ph -> ( comf ` A ) = ( comf ` B ) )
3		1stfpropd.3	|- ( ph -> ( Homf ` C ) = ( Homf ` D ) )
4		1stfpropd.4	|- ( ph -> ( comf ` C ) = ( comf ` D ) )
5		1stfpropd.a	|- ( ph -> A e. Cat )
6		1stfpropd.b	|- ( ph -> B e. Cat )
7		1stfpropd.c	|- ( ph -> C e. Cat )
8		1stfpropd.d	|- ( ph -> D e. Cat )
9		eqid	|- ( A Xc. C ) = ( A Xc. C )
10		eqid	|- ( A 1stF C ) = ( A 1stF C )
11	9 5 7 10	1stfcl	|- ( ph -> ( A 1stF C ) e. ( ( A Xc. C ) Func A ) )
12	1 2 3 4 5 6 7 8 11	curfpropd	|- ( ph -> ( <. A , C >. curryF ( A 1stF C ) ) = ( <. B , D >. curryF ( A 1stF C ) ) )
13		eqid	|- ( A DiagFunc C ) = ( A DiagFunc C )
14	13 5 7	diagval	|- ( ph -> ( A DiagFunc C ) = ( <. A , C >. curryF ( A 1stF C ) ) )
15		eqid	|- ( B DiagFunc D ) = ( B DiagFunc D )
16	15 6 8	diagval	|- ( ph -> ( B DiagFunc D ) = ( <. B , D >. curryF ( B 1stF D ) ) )
17	1 2 3 4 5 6 7 8	1stfpropd	|- ( ph -> ( A 1stF C ) = ( B 1stF D ) )
18	17	oveq2d	|- ( ph -> ( <. B , D >. curryF ( A 1stF C ) ) = ( <. B , D >. curryF ( B 1stF D ) ) )
19	16 18	eqtr4d	|- ( ph -> ( B DiagFunc D ) = ( <. B , D >. curryF ( A 1stF C ) ) )
20	12 14 19	3eqtr4d	|- ( ph -> ( A DiagFunc C ) = ( B DiagFunc D ) )