Theorem precofcl

Description: The pre-composition functor as a transposed curry of the functor composition bifunctor is a functor. (Contributed by Zhi Wang, 11-Oct-2025)

	Ref	Expression
Hypotheses	precofval.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
	precofval.r	⊢ 𝑅 = ( 𝐷 FuncCat 𝐸 )
	precofval.o	⊢ ( 𝜑 → ⚬ = ( ⟨ 𝑄 , 𝑅 ⟩ curryF ( ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ∘func ( 𝑄 swapF 𝑅 ) ) ) )
	precofval.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
	precofval.e	⊢ ( 𝜑 → 𝐸 ∈ Cat )
	precofval.k	⊢ ( 𝜑 → 𝐾 = ( ( 1st ‘ ⚬ ) ‘ 𝐹 ) )
	precofcl.s	⊢ 𝑆 = ( 𝐶 FuncCat 𝐸 )
Assertion	precofcl	⊢ ( 𝜑 → 𝐾 ∈ ( 𝑅 Func 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		precofval.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
2		precofval.r	⊢ 𝑅 = ( 𝐷 FuncCat 𝐸 )
3		precofval.o	⊢ ( 𝜑 → ⚬ = ( ⟨ 𝑄 , 𝑅 ⟩ curryF ( ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ∘func ( 𝑄 swapF 𝑅 ) ) ) )
4		precofval.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
5		precofval.e	⊢ ( 𝜑 → 𝐸 ∈ Cat )
6		precofval.k	⊢ ( 𝜑 → 𝐾 = ( ( 1st ‘ ⚬ ) ‘ 𝐹 ) )
7		precofcl.s	⊢ 𝑆 = ( 𝐶 FuncCat 𝐸 )
8	1	fucbas	⊢ ( 𝐶 Func 𝐷 ) = ( Base ‘ 𝑄 )
9		relfunc	⊢ Rel ( 𝐶 Func 𝐷 )
10		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐹 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2nd ‘ 𝐹 ) )
11	9 4 10	sylancr	⊢ ( 𝜑 → ( 1st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2nd ‘ 𝐹 ) )
12	11	funcrcl2	⊢ ( 𝜑 → 𝐶 ∈ Cat )
13	11	funcrcl3	⊢ ( 𝜑 → 𝐷 ∈ Cat )
14	1 12 13	fuccat	⊢ ( 𝜑 → 𝑄 ∈ Cat )
15	2 13 5	fuccat	⊢ ( 𝜑 → 𝑅 ∈ Cat )
16	2 1	oveq12i	⊢ ( 𝑅 ×c 𝑄 ) = ( ( 𝐷 FuncCat 𝐸 ) ×c ( 𝐶 FuncCat 𝐷 ) )
17	16 7 12 13 5	fucofunca	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ∈ ( ( 𝑅 ×c 𝑄 ) Func 𝑆 ) )
18	3 8 14 15 17 4 6	tposcurf1cl	⊢ ( 𝜑 → 𝐾 ∈ ( 𝑅 Func 𝑆 ) )