Theorem prcoftposcurfucoa

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 𝑅 ) ) ) )
	prcoftposcurfucoa.m	⊢ ( 𝜑 → 𝑀 = ( ( 1st ‘ ⚬ ) ‘ 𝐹 ) )
	prcoftposcurfucoa.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
Assertion	prcoftposcurfucoa	⊢ ( 𝜑 → ( ⟨ 𝐷 , 𝐸 ⟩ −∘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		prcoftposcurfucoa.m	⊢ ( 𝜑 → 𝑀 = ( ( 1st ‘ ⚬ ) ‘ 𝐹 ) )
6		prcoftposcurfucoa.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
7		relfunc	⊢ Rel ( 𝐶 Func 𝐷 )
8		1st2nd	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐹 ∈ ( 𝐶 Func 𝐷 ) ) → 𝐹 = ⟨ ( 1st ‘ 𝐹 ) , ( 2nd ‘ 𝐹 ) ⟩ )
9	7 6 8	sylancr	⊢ ( 𝜑 → 𝐹 = ⟨ ( 1st ‘ 𝐹 ) , ( 2nd ‘ 𝐹 ) ⟩ )
10	9	oveq2d	⊢ ( 𝜑 → ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) = ( ⟨ 𝐷 , 𝐸 ⟩ −∘F ⟨ ( 1st ‘ 𝐹 ) , ( 2nd ‘ 𝐹 ) ⟩ ) )
11	9	fveq2d	⊢ ( 𝜑 → ( ( 1st ‘ ⚬ ) ‘ 𝐹 ) = ( ( 1st ‘ ⚬ ) ‘ ⟨ ( 1st ‘ 𝐹 ) , ( 2nd ‘ 𝐹 ) ⟩ ) )
12	5 11	eqtrd	⊢ ( 𝜑 → 𝑀 = ( ( 1st ‘ ⚬ ) ‘ ⟨ ( 1st ‘ 𝐹 ) , ( 2nd ‘ 𝐹 ) ⟩ ) )
13	6	func1st2nd	⊢ ( 𝜑 → ( 1st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2nd ‘ 𝐹 ) )
14	1 2 3 4 12 13	prcoftposcurfuco	⊢ ( 𝜑 → ( ⟨ 𝐷 , 𝐸 ⟩ −∘F ⟨ ( 1st ‘ 𝐹 ) , ( 2nd ‘ 𝐹 ) ⟩ ) = 𝑀 )
15	10 14	eqtrd	⊢ ( 𝜑 → ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) = 𝑀 )