Theorem prcoftposcurfuco

Description: The pre-composition functor is the transposed curry of the functor composition bifunctor. (Contributed by Zhi Wang, 2-Nov-2025)

	Ref	Expression
Hypotheses	prcoffunc.r	⊢ 𝑅 = ( 𝐷 FuncCat 𝐸 )
	prcoffunc.e	⊢ ( 𝜑 → 𝐸 ∈ Cat )
	prcoftposcurfuco.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
	prcoftposcurfuco.o	⊢ ( 𝜑 → ⚬ = ( ⟨ 𝑄 , 𝑅 ⟩ curryF ( ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ∘func ( 𝑄 swapF 𝑅 ) ) ) )
	prcoftposcurfuco.m	⊢ ( 𝜑 → 𝑀 = ( ( 1st ‘ ⚬ ) ‘ ⟨ 𝐹 , 𝐺 ⟩ ) )
	prcoftposcurfuco.f	⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
Assertion	prcoftposcurfuco	⊢ ( 𝜑 → ( ⟨ 𝐷 , 𝐸 ⟩ −∘F ⟨ 𝐹 , 𝐺 ⟩ ) = 𝑀 )

Proof

Step	Hyp	Ref	Expression
1		prcoffunc.r	⊢ 𝑅 = ( 𝐷 FuncCat 𝐸 )
2		prcoffunc.e	⊢ ( 𝜑 → 𝐸 ∈ Cat )
3		prcoftposcurfuco.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
4		prcoftposcurfuco.o	⊢ ( 𝜑 → ⚬ = ( ⟨ 𝑄 , 𝑅 ⟩ curryF ( ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ∘func ( 𝑄 swapF 𝑅 ) ) ) )
5		prcoftposcurfuco.m	⊢ ( 𝜑 → 𝑀 = ( ( 1st ‘ ⚬ ) ‘ ⟨ 𝐹 , 𝐺 ⟩ ) )
6		prcoftposcurfuco.f	⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
7		eqid	⊢ ( 𝐷 Func 𝐸 ) = ( 𝐷 Func 𝐸 )
8		eqid	⊢ ( 𝐷 Nat 𝐸 ) = ( 𝐷 Nat 𝐸 )
9	6	funcrcl3	⊢ ( 𝜑 → 𝐷 ∈ Cat )
10		relfunc	⊢ Rel ( 𝐶 Func 𝐷 )
11	7 8 9 2 10 6	prcofval	⊢ ( 𝜑 → ( ⟨ 𝐷 , 𝐸 ⟩ −∘F ⟨ 𝐹 , 𝐺 ⟩ ) = ⟨ ( 𝑘 ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑘 ∘func ⟨ 𝐹 , 𝐺 ⟩ ) ) , ( 𝑘 ∈ ( 𝐷 Func 𝐸 ) , 𝑙 ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑎 ∈ ( 𝑘 ( 𝐷 Nat 𝐸 ) 𝑙 ) ↦ ( 𝑎 ∘ 𝐹 ) ) ) ⟩ )
12		eqidd	⊢ ( 𝜑 → ( 𝑘 ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑘 ∘func ⟨ 𝐹 , 𝐺 ⟩ ) ) = ( 𝑘 ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑘 ∘func ⟨ 𝐹 , 𝐺 ⟩ ) ) )
13		eqidd	⊢ ( 𝜑 → ( 𝑘 ∈ ( 𝐷 Func 𝐸 ) , 𝑙 ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑎 ∈ ( 𝑘 ( 𝐷 Nat 𝐸 ) 𝑙 ) ↦ ( 𝑎 ∘ 𝐹 ) ) ) = ( 𝑘 ∈ ( 𝐷 Func 𝐸 ) , 𝑙 ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑎 ∈ ( 𝑘 ( 𝐷 Nat 𝐸 ) 𝑙 ) ↦ ( 𝑎 ∘ 𝐹 ) ) ) )
14	1 7 8 6 2 12 13 3 4 5	precofval3	⊢ ( 𝜑 → ⟨ ( 𝑘 ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑘 ∘func ⟨ 𝐹 , 𝐺 ⟩ ) ) , ( 𝑘 ∈ ( 𝐷 Func 𝐸 ) , 𝑙 ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑎 ∈ ( 𝑘 ( 𝐷 Nat 𝐸 ) 𝑙 ) ↦ ( 𝑎 ∘ 𝐹 ) ) ) ⟩ = 𝑀 )
15	11 14	eqtrd	⊢ ( 𝜑 → ( ⟨ 𝐷 , 𝐸 ⟩ −∘F ⟨ 𝐹 , 𝐺 ⟩ ) = 𝑀 )