Theorem prcoffunca

Description: The pre-composition functor is a functor. (Contributed by Zhi Wang, 2-Nov-2025)

	Ref	Expression
Hypotheses	prcoffunc.r	⊢ 𝑅 = ( 𝐷 FuncCat 𝐸 )
	prcoffunc.e	⊢ ( 𝜑 → 𝐸 ∈ Cat )
	prcoffunc.s	⊢ 𝑆 = ( 𝐶 FuncCat 𝐸 )
	prcoffunca.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
Assertion	prcoffunca	⊢ ( 𝜑 → ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ∈ ( 𝑅 Func 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		prcoffunc.r	⊢ 𝑅 = ( 𝐷 FuncCat 𝐸 )
2		prcoffunc.e	⊢ ( 𝜑 → 𝐸 ∈ Cat )
3		prcoffunc.s	⊢ 𝑆 = ( 𝐶 FuncCat 𝐸 )
4		prcoffunca.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
5		eqid	⊢ ( 𝐶 FuncCat 𝐷 ) = ( 𝐶 FuncCat 𝐷 )
6		eqidd	⊢ ( 𝜑 → ( ⟨ ( 𝐶 FuncCat 𝐷 ) , 𝑅 ⟩ curryF ( ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ∘func ( ( 𝐶 FuncCat 𝐷 ) swapF 𝑅 ) ) ) = ( ⟨ ( 𝐶 FuncCat 𝐷 ) , 𝑅 ⟩ curryF ( ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ∘func ( ( 𝐶 FuncCat 𝐷 ) swapF 𝑅 ) ) ) )
7		eqidd	⊢ ( 𝜑 → ( ( 1st ‘ ( ⟨ ( 𝐶 FuncCat 𝐷 ) , 𝑅 ⟩ curryF ( ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ∘func ( ( 𝐶 FuncCat 𝐷 ) swapF 𝑅 ) ) ) ) ‘ 𝐹 ) = ( ( 1st ‘ ( ⟨ ( 𝐶 FuncCat 𝐷 ) , 𝑅 ⟩ curryF ( ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ∘func ( ( 𝐶 FuncCat 𝐷 ) swapF 𝑅 ) ) ) ) ‘ 𝐹 ) )
8	1 2 5 6 7 4	prcoftposcurfucoa	⊢ ( 𝜑 → ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) = ( ( 1st ‘ ( ⟨ ( 𝐶 FuncCat 𝐷 ) , 𝑅 ⟩ curryF ( ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ∘func ( ( 𝐶 FuncCat 𝐷 ) swapF 𝑅 ) ) ) ) ‘ 𝐹 ) )
9	5 1 6 4 2 8 3	precofcl	⊢ ( 𝜑 → ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ∈ ( 𝑅 Func 𝑆 ) )