Theorem prcoffunc

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 𝐸 )
	prcoffunc.f	⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
Assertion	prcoffunc	⊢ ( 𝜑 → ( ⟨ 𝐷 , 𝐸 ⟩ −∘F ⟨ 𝐹 , 𝐺 ⟩ ) ∈ ( 𝑅 Func 𝑆 ) )

Proof

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