Theorem prcoffunca2

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

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

Proof

Step	Hyp	Ref	Expression
1		prcoffunc.r	⊢ 𝑅 = ( 𝐷 FuncCat 𝐸 )
2		prcoffunc.e	⊢ ( 𝜑 → 𝐸 ∈ Cat )
3		prcoffunc.s	⊢ 𝑆 = ( 𝐶 FuncCat 𝐸 )
4		prcoffunca.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
5		prcoffunca2.k	⊢ ( 𝜑 → ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) = ⟨ 𝐾 , 𝐿 ⟩ )
6	1 2 3 4	prcoffunca	⊢ ( 𝜑 → ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ∈ ( 𝑅 Func 𝑆 ) )
7	5 6	eqeltrrd	⊢ ( 𝜑 → ⟨ 𝐾 , 𝐿 ⟩ ∈ ( 𝑅 Func 𝑆 ) )
8		df-br	⊢ ( 𝐾 ( 𝑅 Func 𝑆 ) 𝐿 ↔ ⟨ 𝐾 , 𝐿 ⟩ ∈ ( 𝑅 Func 𝑆 ) )
9	7 8	sylibr	⊢ ( 𝜑 → 𝐾 ( 𝑅 Func 𝑆 ) 𝐿 )