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	$$⊢R=D\mathrm{FuncCat}E$$
	precoffunc.b	$$⊢B=D\mathrm{Func}E$$
	precoffunc.n	$$⊢N=D\mathrm{Nat}E$$
	precoffunc.f	$$⊢\phi \to F\left(C\mathrm{Func}D\right)G$$
	precoffunc.e	$$⊢\phi \to E\in \mathrm{Cat}$$
	precoffunc.k	$$⊢\phi \to K=\left(g\in B⟼g{\circ }_{\mathrm{func}}⟨F,G⟩\right)$$
	precoffunc.l	$$⊢\phi \to L=\left(g\in B,h\in B⟼\left(a\in \left(gNh\right)⟼a\circ F\right)\right)$$
	precoffunc.s	$$⊢S=C\mathrm{FuncCat}E$$
Assertion	precoffunc	$$⊢\phi \to K\left(R\mathrm{Func}S\right)L$$

Proof

Step	Hyp	Ref	Expression
1		precoffunc.r	$$⊢R=D\mathrm{FuncCat}E$$
2		precoffunc.b	$$⊢B=D\mathrm{Func}E$$
3		precoffunc.n	$$⊢N=D\mathrm{Nat}E$$
4		precoffunc.f	$$⊢\phi \to F\left(C\mathrm{Func}D\right)G$$
5		precoffunc.e	$$⊢\phi \to E\in \mathrm{Cat}$$
6		precoffunc.k	$$⊢\phi \to K=\left(g\in B⟼g{\circ }_{\mathrm{func}}⟨F,G⟩\right)$$
7		precoffunc.l	$$⊢\phi \to L=\left(g\in B,h\in B⟼\left(a\in \left(gNh\right)⟼a\circ F\right)\right)$$
8		precoffunc.s	$$⊢S=C\mathrm{FuncCat}E$$
9		eqid	$$⊢C\mathrm{FuncCat}D=C\mathrm{FuncCat}D$$
10		eqidd	Could not format ( ph -> ( <. ( C FuncCat D ) , R >. curryF ( ( <. C , D >. o.F E ) o.func ( ( C FuncCat D ) swapF R ) ) ) = ( <. ( C FuncCat D ) , R >. curryF ( ( <. C , D >. o.F E ) o.func ( ( C FuncCat D ) swapF R ) ) ) ) : No typesetting found for |- ( ph -> ( <. ( C FuncCat D ) , R >. curryF ( ( <. C , D >. o.F E ) o.func ( ( C FuncCat D ) swapF R ) ) ) = ( <. ( C FuncCat D ) , R >. curryF ( ( <. C , D >. o.F E ) o.func ( ( C FuncCat D ) swapF R ) ) ) ) with typecode |-
11		df-br	$$⊢F\left(C\mathrm{Func}D\right)G\leftrightarrow ⟨F,G⟩\in \left(C\mathrm{Func}D\right)$$
12	4 11	sylib	$$⊢\phi \to ⟨F,G⟩\in \left(C\mathrm{Func}D\right)$$
13		eqidd	Could not format ( ph -> ( ( 1st ` ( <. ( C FuncCat D ) , R >. curryF ( ( <. C , D >. o.F E ) o.func ( ( C FuncCat D ) swapF R ) ) ) ) ` <. F , G >. ) = ( ( 1st ` ( <. ( C FuncCat D ) , R >. curryF ( ( <. C , D >. o.F E ) o.func ( ( C FuncCat D ) swapF R ) ) ) ) ` <. F , G >. ) ) : No typesetting found for |- ( ph -> ( ( 1st ` ( <. ( C FuncCat D ) , R >. curryF ( ( <. C , D >. o.F E ) o.func ( ( C FuncCat D ) swapF R ) ) ) ) ` <. F , G >. ) = ( ( 1st ` ( <. ( C FuncCat D ) , R >. curryF ( ( <. C , D >. o.F E ) o.func ( ( C FuncCat D ) swapF R ) ) ) ) ` <. F , G >. ) ) with typecode |-
14	1 2 3 4 5 6 7 9 10 13	precofval3	Could not format ( ph -> <. K , L >. = ( ( 1st ` ( <. ( C FuncCat D ) , R >. curryF ( ( <. C , D >. o.F E ) o.func ( ( C FuncCat D ) swapF R ) ) ) ) ` <. F , G >. ) ) : No typesetting found for |- ( ph -> <. K , L >. = ( ( 1st ` ( <. ( C FuncCat D ) , R >. curryF ( ( <. C , D >. o.F E ) o.func ( ( C FuncCat D ) swapF R ) ) ) ) ` <. F , G >. ) ) with typecode |-
15	9 1 10 12 5 14 8	precofcl	$$⊢\phi \to ⟨K,L⟩\in \left(R\mathrm{Func}S\right)$$
16		df-br	$$⊢K\left(R\mathrm{Func}S\right)L\leftrightarrow ⟨K,L⟩\in \left(R\mathrm{Func}S\right)$$
17	15 16	sylibr	$$⊢\phi \to K\left(R\mathrm{Func}S\right)L$$