Theorem precoffunc

Description: The pre-composition functor, expressed explicitly, is a functor. (Contributed by Zhi Wang, 11-Oct-2025) (Proof shortened by Zhi Wang, 20-Oct-2025)

	Ref	Expression
Hypotheses	precoffunc.r	⊢ 𝑅 = ( 𝐷 FuncCat 𝐸 )
	precoffunc.b	⊢ 𝐵 = ( 𝐷 Func 𝐸 )
	precoffunc.n	⊢ 𝑁 = ( 𝐷 Nat 𝐸 )
	precoffunc.f	⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
	precoffunc.e	⊢ ( 𝜑 → 𝐸 ∈ Cat )
	precoffunc.k	⊢ ( 𝜑 → 𝐾 = ( 𝑔 ∈ 𝐵 ↦ ( 𝑔 ∘func ⟨ 𝐹 , 𝐺 ⟩ ) ) )
	precoffunc.l	⊢ ( 𝜑 → 𝐿 = ( 𝑔 ∈ 𝐵 , ℎ ∈ 𝐵 ↦ ( 𝑎 ∈ ( 𝑔 𝑁 ℎ ) ↦ ( 𝑎 ∘ 𝐹 ) ) ) )
	precoffunc.s	⊢ 𝑆 = ( 𝐶 FuncCat 𝐸 )
Assertion	precoffunc	⊢ ( 𝜑 → 𝐾 ( 𝑅 Func 𝑆 ) 𝐿 )

Proof

Step	Hyp	Ref	Expression
1		precoffunc.r	⊢ 𝑅 = ( 𝐷 FuncCat 𝐸 )
2		precoffunc.b	⊢ 𝐵 = ( 𝐷 Func 𝐸 )
3		precoffunc.n	⊢ 𝑁 = ( 𝐷 Nat 𝐸 )
4		precoffunc.f	⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
5		precoffunc.e	⊢ ( 𝜑 → 𝐸 ∈ Cat )
6		precoffunc.k	⊢ ( 𝜑 → 𝐾 = ( 𝑔 ∈ 𝐵 ↦ ( 𝑔 ∘func ⟨ 𝐹 , 𝐺 ⟩ ) ) )
7		precoffunc.l	⊢ ( 𝜑 → 𝐿 = ( 𝑔 ∈ 𝐵 , ℎ ∈ 𝐵 ↦ ( 𝑎 ∈ ( 𝑔 𝑁 ℎ ) ↦ ( 𝑎 ∘ 𝐹 ) ) ) )
8		precoffunc.s	⊢ 𝑆 = ( 𝐶 FuncCat 𝐸 )
9		eqid	⊢ ( 𝐶 FuncCat 𝐷 ) = ( 𝐶 FuncCat 𝐷 )
10		eqidd	⊢ ( 𝜑 → ( ⟨ ( 𝐶 FuncCat 𝐷 ) , 𝑅 ⟩ curryF ( ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ∘func ( ( 𝐶 FuncCat 𝐷 ) swapF 𝑅 ) ) ) = ( ⟨ ( 𝐶 FuncCat 𝐷 ) , 𝑅 ⟩ curryF ( ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ∘func ( ( 𝐶 FuncCat 𝐷 ) swapF 𝑅 ) ) ) )
11		df-br	⊢ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐶 Func 𝐷 ) )
12	4 11	sylib	⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐶 Func 𝐷 ) )
13		eqidd	⊢ ( 𝜑 → ( ( 1st ‘ ( ⟨ ( 𝐶 FuncCat 𝐷 ) , 𝑅 ⟩ curryF ( ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ∘func ( ( 𝐶 FuncCat 𝐷 ) swapF 𝑅 ) ) ) ) ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = ( ( 1st ‘ ( ⟨ ( 𝐶 FuncCat 𝐷 ) , 𝑅 ⟩ curryF ( ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ∘func ( ( 𝐶 FuncCat 𝐷 ) swapF 𝑅 ) ) ) ) ‘ ⟨ 𝐹 , 𝐺 ⟩ ) )
14	1 2 3 4 5 6 7 9 10 13	precofval3	⊢ ( 𝜑 → ⟨ 𝐾 , 𝐿 ⟩ = ( ( 1st ‘ ( ⟨ ( 𝐶 FuncCat 𝐷 ) , 𝑅 ⟩ curryF ( ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) ∘func ( ( 𝐶 FuncCat 𝐷 ) swapF 𝑅 ) ) ) ) ‘ ⟨ 𝐹 , 𝐺 ⟩ ) )
15	9 1 10 12 5 14 8	precofcl	⊢ ( 𝜑 → ⟨ 𝐾 , 𝐿 ⟩ ∈ ( 𝑅 Func 𝑆 ) )
16		df-br	⊢ ( 𝐾 ( 𝑅 Func 𝑆 ) 𝐿 ↔ ⟨ 𝐾 , 𝐿 ⟩ ∈ ( 𝑅 Func 𝑆 ) )
17	15 16	sylibr	⊢ ( 𝜑 → 𝐾 ( 𝑅 Func 𝑆 ) 𝐿 )