Theorem prcofpropd

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

	Ref	Expression
Hypotheses	prcofpropd.1	⊢ ( 𝜑 → ( Homf ‘ 𝐴 ) = ( Homf ‘ 𝐵 ) )
	prcofpropd.2	⊢ ( 𝜑 → ( compf ‘ 𝐴 ) = ( compf ‘ 𝐵 ) )
	prcofpropd.3	⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
	prcofpropd.4	⊢ ( 𝜑 → ( compf ‘ 𝐶 ) = ( compf ‘ 𝐷 ) )
	prcofpropd.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	prcofpropd.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
	prcofpropd.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
	prcofpropd.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
	prcofpropd.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑊 )
Assertion	prcofpropd	⊢ ( 𝜑 → ( ⟨ 𝐴 , 𝐶 ⟩ −∘F 𝐹 ) = ( ⟨ 𝐵 , 𝐷 ⟩ −∘F 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		prcofpropd.1	⊢ ( 𝜑 → ( Homf ‘ 𝐴 ) = ( Homf ‘ 𝐵 ) )
2		prcofpropd.2	⊢ ( 𝜑 → ( compf ‘ 𝐴 ) = ( compf ‘ 𝐵 ) )
3		prcofpropd.3	⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
4		prcofpropd.4	⊢ ( 𝜑 → ( compf ‘ 𝐶 ) = ( compf ‘ 𝐷 ) )
5		prcofpropd.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
6		prcofpropd.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
7		prcofpropd.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
8		prcofpropd.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
9		prcofpropd.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑊 )
10	1 2 3 4 5 6 7 8	funcpropd	⊢ ( 𝜑 → ( 𝐴 Func 𝐶 ) = ( 𝐵 Func 𝐷 ) )
11	10	mpteq1d	⊢ ( 𝜑 → ( 𝑘 ∈ ( 𝐴 Func 𝐶 ) ↦ ( 𝑘 ∘func 𝐹 ) ) = ( 𝑘 ∈ ( 𝐵 Func 𝐷 ) ↦ ( 𝑘 ∘func 𝐹 ) ) )
12	10	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 Func 𝐶 ) ) → ( 𝐴 Func 𝐶 ) = ( 𝐵 Func 𝐷 ) )
13	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑙 ∈ ( 𝐴 Func 𝐶 ) ) ) → ( Homf ‘ 𝐴 ) = ( Homf ‘ 𝐵 ) )
14	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑙 ∈ ( 𝐴 Func 𝐶 ) ) ) → ( compf ‘ 𝐴 ) = ( compf ‘ 𝐵 ) )
15	3	adantr	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑙 ∈ ( 𝐴 Func 𝐶 ) ) ) → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
16	4	adantr	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑙 ∈ ( 𝐴 Func 𝐶 ) ) ) → ( compf ‘ 𝐶 ) = ( compf ‘ 𝐷 ) )
17		funcrcl	⊢ ( 𝑘 ∈ ( 𝐴 Func 𝐶 ) → ( 𝐴 ∈ Cat ∧ 𝐶 ∈ Cat ) )
18	17	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑙 ∈ ( 𝐴 Func 𝐶 ) ) ) → ( 𝐴 ∈ Cat ∧ 𝐶 ∈ Cat ) )
19	18	simpld	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑙 ∈ ( 𝐴 Func 𝐶 ) ) ) → 𝐴 ∈ Cat )
20	6	adantr	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑙 ∈ ( 𝐴 Func 𝐶 ) ) ) → 𝐵 ∈ 𝑉 )
21	13 14 19 20	catpropd	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑙 ∈ ( 𝐴 Func 𝐶 ) ) ) → ( 𝐴 ∈ Cat ↔ 𝐵 ∈ Cat ) )
22	19 21	mpbid	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑙 ∈ ( 𝐴 Func 𝐶 ) ) ) → 𝐵 ∈ Cat )
23	18	simprd	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑙 ∈ ( 𝐴 Func 𝐶 ) ) ) → 𝐶 ∈ Cat )
24	8	adantr	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑙 ∈ ( 𝐴 Func 𝐶 ) ) ) → 𝐷 ∈ 𝑉 )
25	15 16 23 24	catpropd	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑙 ∈ ( 𝐴 Func 𝐶 ) ) ) → ( 𝐶 ∈ Cat ↔ 𝐷 ∈ Cat ) )
26	23 25	mpbid	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑙 ∈ ( 𝐴 Func 𝐶 ) ) ) → 𝐷 ∈ Cat )
27	13 14 15 16 19 22 23 26	natpropd	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑙 ∈ ( 𝐴 Func 𝐶 ) ) ) → ( 𝐴 Nat 𝐶 ) = ( 𝐵 Nat 𝐷 ) )
28	27	oveqd	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑙 ∈ ( 𝐴 Func 𝐶 ) ) ) → ( 𝑘 ( 𝐴 Nat 𝐶 ) 𝑙 ) = ( 𝑘 ( 𝐵 Nat 𝐷 ) 𝑙 ) )
29	28	mpteq1d	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑙 ∈ ( 𝐴 Func 𝐶 ) ) ) → ( 𝑎 ∈ ( 𝑘 ( 𝐴 Nat 𝐶 ) 𝑙 ) ↦ ( 𝑎 ∘ ( 1st ‘ 𝐹 ) ) ) = ( 𝑎 ∈ ( 𝑘 ( 𝐵 Nat 𝐷 ) 𝑙 ) ↦ ( 𝑎 ∘ ( 1st ‘ 𝐹 ) ) ) )
30	10 12 29	mpoeq123dva	⊢ ( 𝜑 → ( 𝑘 ∈ ( 𝐴 Func 𝐶 ) , 𝑙 ∈ ( 𝐴 Func 𝐶 ) ↦ ( 𝑎 ∈ ( 𝑘 ( 𝐴 Nat 𝐶 ) 𝑙 ) ↦ ( 𝑎 ∘ ( 1st ‘ 𝐹 ) ) ) ) = ( 𝑘 ∈ ( 𝐵 Func 𝐷 ) , 𝑙 ∈ ( 𝐵 Func 𝐷 ) ↦ ( 𝑎 ∈ ( 𝑘 ( 𝐵 Nat 𝐷 ) 𝑙 ) ↦ ( 𝑎 ∘ ( 1st ‘ 𝐹 ) ) ) ) )
31	11 30	opeq12d	⊢ ( 𝜑 → ⟨ ( 𝑘 ∈ ( 𝐴 Func 𝐶 ) ↦ ( 𝑘 ∘func 𝐹 ) ) , ( 𝑘 ∈ ( 𝐴 Func 𝐶 ) , 𝑙 ∈ ( 𝐴 Func 𝐶 ) ↦ ( 𝑎 ∈ ( 𝑘 ( 𝐴 Nat 𝐶 ) 𝑙 ) ↦ ( 𝑎 ∘ ( 1st ‘ 𝐹 ) ) ) ) ⟩ = ⟨ ( 𝑘 ∈ ( 𝐵 Func 𝐷 ) ↦ ( 𝑘 ∘func 𝐹 ) ) , ( 𝑘 ∈ ( 𝐵 Func 𝐷 ) , 𝑙 ∈ ( 𝐵 Func 𝐷 ) ↦ ( 𝑎 ∈ ( 𝑘 ( 𝐵 Nat 𝐷 ) 𝑙 ) ↦ ( 𝑎 ∘ ( 1st ‘ 𝐹 ) ) ) ) ⟩ )
32		eqid	⊢ ( 𝐴 Func 𝐶 ) = ( 𝐴 Func 𝐶 )
33		eqid	⊢ ( 𝐴 Nat 𝐶 ) = ( 𝐴 Nat 𝐶 )
34	32 33 5 7 9	prcofvala	⊢ ( 𝜑 → ( ⟨ 𝐴 , 𝐶 ⟩ −∘F 𝐹 ) = ⟨ ( 𝑘 ∈ ( 𝐴 Func 𝐶 ) ↦ ( 𝑘 ∘func 𝐹 ) ) , ( 𝑘 ∈ ( 𝐴 Func 𝐶 ) , 𝑙 ∈ ( 𝐴 Func 𝐶 ) ↦ ( 𝑎 ∈ ( 𝑘 ( 𝐴 Nat 𝐶 ) 𝑙 ) ↦ ( 𝑎 ∘ ( 1st ‘ 𝐹 ) ) ) ) ⟩ )
35		eqid	⊢ ( 𝐵 Func 𝐷 ) = ( 𝐵 Func 𝐷 )
36		eqid	⊢ ( 𝐵 Nat 𝐷 ) = ( 𝐵 Nat 𝐷 )
37	35 36 6 8 9	prcofvala	⊢ ( 𝜑 → ( ⟨ 𝐵 , 𝐷 ⟩ −∘F 𝐹 ) = ⟨ ( 𝑘 ∈ ( 𝐵 Func 𝐷 ) ↦ ( 𝑘 ∘func 𝐹 ) ) , ( 𝑘 ∈ ( 𝐵 Func 𝐷 ) , 𝑙 ∈ ( 𝐵 Func 𝐷 ) ↦ ( 𝑎 ∈ ( 𝑘 ( 𝐵 Nat 𝐷 ) 𝑙 ) ↦ ( 𝑎 ∘ ( 1st ‘ 𝐹 ) ) ) ) ⟩ )
38	31 34 37	3eqtr4d	⊢ ( 𝜑 → ( ⟨ 𝐴 , 𝐶 ⟩ −∘F 𝐹 ) = ( ⟨ 𝐵 , 𝐷 ⟩ −∘F 𝐹 ) )