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		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	2 12 13	fuccat	⊢ ( 𝜑 → 𝑅 ∈ Cat )
15	1 5 12	fuccat	⊢ ( 𝜑 → 𝑄 ∈ Cat )
16	2 1	oveq12i	⊢ ( 𝑅 ×c 𝑄 ) = ( ( 𝐷 FuncCat 𝐸 ) ×c ( 𝐶 FuncCat 𝐷 ) )
17	16 7 5 12 13	fucofunca	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ∈ ( ( 𝑅 ×c 𝑄 ) Func 𝑆 ) )
18		eqid	⊢ ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
19	3 8 14 15 17 18 4 6	curf1cl	⊢ ( 𝜑 → 𝐾 ∈ ( 𝑄 Func 𝑆 ) )