Theorem prcoffunc

Description: The pre-composition functor is a functor. (Contributed by Zhi Wang, 2-Nov-2025)

	Ref	Expression
Hypotheses	prcoffunc.r	$$⊢R=D\mathrm{FuncCat}E$$
	prcoffunc.e	$$⊢\phi \to E\in \mathrm{Cat}$$
	prcoffunc.s	$$⊢S=C\mathrm{FuncCat}E$$
	prcoffunc.f	$$⊢\phi \to F\left(C\mathrm{Func}D\right)G$$
Assertion	prcoffunc	Could not format assertion : No typesetting found for |- ( ph -> ( <. D , E >. -o.F <. F , G >. ) e. ( R Func S ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		prcoffunc.r	$$⊢R=D\mathrm{FuncCat}E$$
2		prcoffunc.e	$$⊢\phi \to E\in \mathrm{Cat}$$
3		prcoffunc.s	$$⊢S=C\mathrm{FuncCat}E$$
4		prcoffunc.f	$$⊢\phi \to F\left(C\mathrm{Func}D\right)G$$
5		eqid	$$⊢C\mathrm{FuncCat}D=C\mathrm{FuncCat}D$$
6		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 |-
7		df-br	$$⊢F\left(C\mathrm{Func}D\right)G\leftrightarrow ⟨F,G⟩\in \left(C\mathrm{Func}D\right)$$
8	4 7	sylib	$$⊢\phi \to ⟨F,G⟩\in \left(C\mathrm{Func}D\right)$$
9		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 |-
10	1 2 5 6 9 4	prcoftposcurfuco	Could not format ( ph -> ( <. D , E >. -o.F <. 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 -> ( <. D , E >. -o.F <. F , G >. ) = ( ( 1st ` ( <. ( C FuncCat D ) , R >. curryF ( ( <. C , D >. o.F E ) o.func ( ( C FuncCat D ) swapF R ) ) ) ) ` <. F , G >. ) ) with typecode |-
11	5 1 6 8 2 10 3	precofcl	Could not format ( ph -> ( <. D , E >. -o.F <. F , G >. ) e. ( R Func S ) ) : No typesetting found for |- ( ph -> ( <. D , E >. -o.F <. F , G >. ) e. ( R Func S ) ) with typecode |-