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	⊢ ( 𝜑 → ( Homf ‘ 𝐴 ) = ( Homf ‘ 𝐵 ) )
	1stfpropd.2	⊢ ( 𝜑 → ( compf ‘ 𝐴 ) = ( compf ‘ 𝐵 ) )
	1stfpropd.3	⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
	1stfpropd.4	⊢ ( 𝜑 → ( compf ‘ 𝐶 ) = ( compf ‘ 𝐷 ) )
	1stfpropd.a	⊢ ( 𝜑 → 𝐴 ∈ Cat )
	1stfpropd.b	⊢ ( 𝜑 → 𝐵 ∈ Cat )
	1stfpropd.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	1stfpropd.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
Assertion	diagpropd	⊢ ( 𝜑 → ( 𝐴 Δfunc 𝐶 ) = ( 𝐵 Δfunc 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		1stfpropd.1	⊢ ( 𝜑 → ( Homf ‘ 𝐴 ) = ( Homf ‘ 𝐵 ) )
2		1stfpropd.2	⊢ ( 𝜑 → ( compf ‘ 𝐴 ) = ( compf ‘ 𝐵 ) )
3		1stfpropd.3	⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
4		1stfpropd.4	⊢ ( 𝜑 → ( compf ‘ 𝐶 ) = ( compf ‘ 𝐷 ) )
5		1stfpropd.a	⊢ ( 𝜑 → 𝐴 ∈ Cat )
6		1stfpropd.b	⊢ ( 𝜑 → 𝐵 ∈ Cat )
7		1stfpropd.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
8		1stfpropd.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
9		eqid	⊢ ( 𝐴 ×c 𝐶 ) = ( 𝐴 ×c 𝐶 )
10		eqid	⊢ ( 𝐴 1stF 𝐶 ) = ( 𝐴 1stF 𝐶 )
11	9 5 7 10	1stfcl	⊢ ( 𝜑 → ( 𝐴 1stF 𝐶 ) ∈ ( ( 𝐴 ×c 𝐶 ) Func 𝐴 ) )
12	1 2 3 4 5 6 7 8 11	curfpropd	⊢ ( 𝜑 → ( ⟨ 𝐴 , 𝐶 ⟩ curryF ( 𝐴 1stF 𝐶 ) ) = ( ⟨ 𝐵 , 𝐷 ⟩ curryF ( 𝐴 1stF 𝐶 ) ) )
13		eqid	⊢ ( 𝐴 Δfunc 𝐶 ) = ( 𝐴 Δfunc 𝐶 )
14	13 5 7	diagval	⊢ ( 𝜑 → ( 𝐴 Δfunc 𝐶 ) = ( ⟨ 𝐴 , 𝐶 ⟩ curryF ( 𝐴 1stF 𝐶 ) ) )
15		eqid	⊢ ( 𝐵 Δfunc 𝐷 ) = ( 𝐵 Δfunc 𝐷 )
16	15 6 8	diagval	⊢ ( 𝜑 → ( 𝐵 Δfunc 𝐷 ) = ( ⟨ 𝐵 , 𝐷 ⟩ curryF ( 𝐵 1stF 𝐷 ) ) )
17	1 2 3 4 5 6 7 8	1stfpropd	⊢ ( 𝜑 → ( 𝐴 1stF 𝐶 ) = ( 𝐵 1stF 𝐷 ) )
18	17	oveq2d	⊢ ( 𝜑 → ( ⟨ 𝐵 , 𝐷 ⟩ curryF ( 𝐴 1stF 𝐶 ) ) = ( ⟨ 𝐵 , 𝐷 ⟩ curryF ( 𝐵 1stF 𝐷 ) ) )
19	16 18	eqtr4d	⊢ ( 𝜑 → ( 𝐵 Δfunc 𝐷 ) = ( ⟨ 𝐵 , 𝐷 ⟩ curryF ( 𝐴 1stF 𝐶 ) ) )
20	12 14 19	3eqtr4d	⊢ ( 𝜑 → ( 𝐴 Δfunc 𝐶 ) = ( 𝐵 Δfunc 𝐷 ) )