Theorem prcoftposcurfuco

Description: The pre-composition functor is the transposed curry of the functor composition bifunctor. (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}$$
	prcoftposcurfuco.q	$$⊢Q=C\mathrm{FuncCat}D$$
	prcoftposcurfuco.o	No typesetting found for |- ( ph -> .o. = ( <. Q , R >. curryF ( ( <. C , D >. o.F E ) o.func ( Q swapF R ) ) ) ) with typecode |-
	prcoftposcurfuco.m	No typesetting found for |- ( ph -> M = ( ( 1st ` .o. ) ` <. F , G >. ) ) with typecode |-
	prcoftposcurfuco.f	$$⊢\phi \to F\left(C\mathrm{Func}D\right)G$$
Assertion	prcoftposcurfuco	Could not format assertion : No typesetting found for |- ( ph -> ( <. D , E >. -o.F <. F , G >. ) = M ) 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		prcoftposcurfuco.q	$$⊢Q=C\mathrm{FuncCat}D$$
4		prcoftposcurfuco.o	Could not format ( ph -> .o. = ( <. Q , R >. curryF ( ( <. C , D >. o.F E ) o.func ( Q swapF R ) ) ) ) : No typesetting found for |- ( ph -> .o. = ( <. Q , R >. curryF ( ( <. C , D >. o.F E ) o.func ( Q swapF R ) ) ) ) with typecode |-
5		prcoftposcurfuco.m	Could not format ( ph -> M = ( ( 1st ` .o. ) ` <. F , G >. ) ) : No typesetting found for |- ( ph -> M = ( ( 1st ` .o. ) ` <. F , G >. ) ) with typecode |-
6		prcoftposcurfuco.f	$$⊢\phi \to F\left(C\mathrm{Func}D\right)G$$
7		eqid	$$⊢D\mathrm{Func}E=D\mathrm{Func}E$$
8		eqid	$$⊢D\mathrm{Nat}E=D\mathrm{Nat}E$$
9	6	funcrcl3	$$⊢\phi \to D\in \mathrm{Cat}$$
10		relfunc	$$⊢\mathrm{Rel}\left(C\mathrm{Func}D\right)$$
11	7 8 9 2 10 6	prcofval	Could not format ( ph -> ( <. D , E >. -o.F <. F , G >. ) = <. ( k e. ( D Func E ) |-> ( k o.func <. F , G >. ) ) , ( k e. ( D Func E ) , l e. ( D Func E ) |-> ( a e. ( k ( D Nat E ) l ) |-> ( a o. F ) ) ) >. ) : No typesetting found for |- ( ph -> ( <. D , E >. -o.F <. F , G >. ) = <. ( k e. ( D Func E ) |-> ( k o.func <. F , G >. ) ) , ( k e. ( D Func E ) , l e. ( D Func E ) |-> ( a e. ( k ( D Nat E ) l ) |-> ( a o. F ) ) ) >. ) with typecode |-
12		eqidd	$$⊢\phi \to \left(k\in \left(D\mathrm{Func}E\right)⟼k{\circ }_{\mathrm{func}}⟨F,G⟩\right)=\left(k\in \left(D\mathrm{Func}E\right)⟼k{\circ }_{\mathrm{func}}⟨F,G⟩\right)$$
13		eqidd	$$⊢\phi \to \left(k\in \left(D\mathrm{Func}E\right),l\in \left(D\mathrm{Func}E\right)⟼\left(a\in \left(k\left(D\mathrm{Nat}E\right)l\right)⟼a\circ F\right)\right)=\left(k\in \left(D\mathrm{Func}E\right),l\in \left(D\mathrm{Func}E\right)⟼\left(a\in \left(k\left(D\mathrm{Nat}E\right)l\right)⟼a\circ F\right)\right)$$
14	1 7 8 6 2 12 13 3 4 5	precofval3	$$⊢\phi \to ⟨\left(k\in \left(D\mathrm{Func}E\right)⟼k{\circ }_{\mathrm{func}}⟨F,G⟩\right),\left(k\in \left(D\mathrm{Func}E\right),l\in \left(D\mathrm{Func}E\right)⟼\left(a\in \left(k\left(D\mathrm{Nat}E\right)l\right)⟼a\circ F\right)\right)⟩=M$$
15	11 14	eqtrd	Could not format ( ph -> ( <. D , E >. -o.F <. F , G >. ) = M ) : No typesetting found for |- ( ph -> ( <. D , E >. -o.F <. F , G >. ) = M ) with typecode |-