Theorem precoffunc

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

	Ref	Expression
Hypotheses	precoffunc.r	$$⊢R=D\mathrm{FuncCat}E$$
	precoffunc.s	$$⊢S=C\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)$$
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.s	$$⊢S=C\mathrm{FuncCat}E$$
3		precoffunc.b	$$⊢B=D\mathrm{Func}E$$
4		precoffunc.n	$$⊢N=D\mathrm{Nat}E$$
5		precoffunc.f	$$⊢\phi \to F\left(C\mathrm{Func}D\right)G$$
6		precoffunc.e	$$⊢\phi \to E\in \mathrm{Cat}$$
7		precoffunc.k	$$⊢\phi \to K=\left(g\in B⟼g{\circ }_{\mathrm{func}}⟨F,G⟩\right)$$
8		precoffunc.l	$$⊢\phi \to L=\left(g\in B,h\in B⟼\left(a\in \left(gNh\right)⟼a\circ F\right)\right)$$
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	5 11	sylib	$$⊢\phi \to ⟨F,G⟩\in \left(C\mathrm{Func}D\right)$$
13	3	mpteq1i	$$⊢\left(g\in B⟼g{\circ }_{\mathrm{func}}⟨F,G⟩\right)=\left(g\in \left(D\mathrm{Func}E\right)⟼g{\circ }_{\mathrm{func}}⟨F,G⟩\right)$$
14	7 13	eqtrdi	$$⊢\phi \to K=\left(g\in \left(D\mathrm{Func}E\right)⟼g{\circ }_{\mathrm{func}}⟨F,G⟩\right)$$
15	3	a1i	$$⊢\phi \to B=D\mathrm{Func}E$$
16	4	a1i	$$⊢\phi \to N=D\mathrm{Nat}E$$
17	16	oveqd	$$⊢\phi \to gNh=g\left(D\mathrm{Nat}E\right)h$$
18		relfunc	$$⊢\mathrm{Rel}\left(C\mathrm{Func}D\right)$$
19		brrelex12	$$⊢\left(\mathrm{Rel}\left(C\mathrm{Func}D\right)\wedge F\left(C\mathrm{Func}D\right)G\right)\to \left(F\in \mathrm{V}\wedge G\in \mathrm{V}\right)$$
20	18 5 19	sylancr	$$⊢\phi \to \left(F\in \mathrm{V}\wedge G\in \mathrm{V}\right)$$
21		op1stg	$$⊢\left(F\in \mathrm{V}\wedge G\in \mathrm{V}\right)\to 1^{st}\left(⟨F,G⟩\right)=F$$
22	20 21	syl	$$⊢\phi \to 1^{st}\left(⟨F,G⟩\right)=F$$
23	22	eqcomd	$$⊢\phi \to F=1^{st}\left(⟨F,G⟩\right)$$
24	23	coeq2d	$$⊢\phi \to a\circ F=a\circ 1^{st}\left(⟨F,G⟩\right)$$
25	17 24	mpteq12dv	$$⊢\phi \to \left(a\in \left(gNh\right)⟼a\circ F\right)=\left(a\in \left(g\left(D\mathrm{Nat}E\right)h\right)⟼a\circ 1^{st}\left(⟨F,G⟩\right)\right)$$
26	15 15 25	mpoeq123dv	$$⊢\phi \to \left(g\in B,h\in B⟼\left(a\in \left(gNh\right)⟼a\circ F\right)\right)=\left(g\in \left(D\mathrm{Func}E\right),h\in \left(D\mathrm{Func}E\right)⟼\left(a\in \left(g\left(D\mathrm{Nat}E\right)h\right)⟼a\circ 1^{st}\left(⟨F,G⟩\right)\right)\right)$$
27	8 26	eqtrd	$$⊢\phi \to L=\left(g\in \left(D\mathrm{Func}E\right),h\in \left(D\mathrm{Func}E\right)⟼\left(a\in \left(g\left(D\mathrm{Nat}E\right)h\right)⟼a\circ 1^{st}\left(⟨F,G⟩\right)\right)\right)$$
28	14 27	opeq12d	$$⊢\phi \to ⟨K,L⟩=⟨\left(g\in \left(D\mathrm{Func}E\right)⟼g{\circ }_{\mathrm{func}}⟨F,G⟩\right),\left(g\in \left(D\mathrm{Func}E\right),h\in \left(D\mathrm{Func}E\right)⟼\left(a\in \left(g\left(D\mathrm{Nat}E\right)h\right)⟼a\circ 1^{st}\left(⟨F,G⟩\right)\right)\right)⟩$$
29		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 |-
30	9 1 10 12 6 29	precofval2	Could not format ( ph -> ( ( 1st ` ( <. ( C FuncCat D ) , R >. curryF ( ( <. C , D >. o.F E ) o.func ( ( C FuncCat D ) swapF R ) ) ) ) ` <. F , G >. ) = <. ( g e. ( D Func E ) |-> ( g o.func <. F , G >. ) ) , ( g e. ( D Func E ) , h e. ( D Func E ) |-> ( a e. ( g ( D Nat E ) h ) |-> ( a o. ( 1st ` <. 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 >. ) = <. ( g e. ( D Func E ) |-> ( g o.func <. F , G >. ) ) , ( g e. ( D Func E ) , h e. ( D Func E ) |-> ( a e. ( g ( D Nat E ) h ) |-> ( a o. ( 1st ` <. F , G >. ) ) ) ) >. ) with typecode |-
31	28 30	eqtr4d	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 |-
32	9 1 10 12 6 31 2	precofcl	$$⊢\phi \to ⟨K,L⟩\in \left(R\mathrm{Func}S\right)$$
33		df-br	$$⊢K\left(R\mathrm{Func}S\right)L\leftrightarrow ⟨K,L⟩\in \left(R\mathrm{Func}S\right)$$
34	32 33	sylibr	$$⊢\phi \to K\left(R\mathrm{Func}S\right)L$$