Theorem postcofcl

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

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

Proof

Step	Hyp	Ref	Expression
1		postcofval.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
2		postcofval.r	⊢ 𝑅 = ( 𝐷 FuncCat 𝐸 )
3		postcofval.o	⊢ ⚬ = ( ⟨ 𝑅 , 𝑄 ⟩ curryF ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) )
4		postcofval.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐷 Func 𝐸 ) )
5		postcofval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
6		postcofval.k	⊢ 𝐾 = ( ( 1st ‘ ⚬ ) ‘ 𝐹 )
7		postcofcl.s	⊢ 𝑆 = ( 𝐶 FuncCat 𝐸 )
8	2	fucbas	⊢ ( 𝐷 Func 𝐸 ) = ( Base ‘ 𝑅 )
9	4	func1st2nd	⊢ ( 𝜑 → ( 1st ‘ 𝐹 ) ( 𝐷 Func 𝐸 ) ( 2nd ‘ 𝐹 ) )
10	9	funcrcl2	⊢ ( 𝜑 → 𝐷 ∈ Cat )
11	9	funcrcl3	⊢ ( 𝜑 → 𝐸 ∈ Cat )
12	2 10 11	fuccat	⊢ ( 𝜑 → 𝑅 ∈ Cat )
13	1 5 10	fuccat	⊢ ( 𝜑 → 𝑄 ∈ Cat )
14	2 1	oveq12i	⊢ ( 𝑅 ×c 𝑄 ) = ( ( 𝐷 FuncCat 𝐸 ) ×c ( 𝐶 FuncCat 𝐷 ) )
15	14 7 5 10 11	fucofunca	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ∈ ( ( 𝑅 ×c 𝑄 ) Func 𝑆 ) )
16		eqid	⊢ ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
17	3 8 12 13 15 16 4 6	curf1cl	⊢ ( 𝜑 → 𝐾 ∈ ( 𝑄 Func 𝑆 ) )