Theorem prcoftposcurfucoa

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 |-
	prcoftposcurfucoa.m	No typesetting found for |- ( ph -> M = ( ( 1st ` .o. ) ` F ) ) with typecode |-
	prcoftposcurfucoa.f	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
Assertion	prcoftposcurfucoa	Could not format assertion : No typesetting found for |- ( ph -> ( <. D , E >. -o.F F ) = 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		prcoftposcurfucoa.m	Could not format ( ph -> M = ( ( 1st ` .o. ) ` F ) ) : No typesetting found for |- ( ph -> M = ( ( 1st ` .o. ) ` F ) ) with typecode |-
6		prcoftposcurfucoa.f	$$⊢\phi \to F\in \left(C\mathrm{Func}D\right)$$
7		relfunc	$$⊢\mathrm{Rel}\left(C\mathrm{Func}D\right)$$
8		1st2nd	$$⊢\left(\mathrm{Rel}\left(C\mathrm{Func}D\right)\wedge F\in \left(C\mathrm{Func}D\right)\right)\to F=⟨1^{st}\left(F\right),2^{nd}\left(F\right)⟩$$
9	7 6 8	sylancr	$$⊢\phi \to F=⟨1^{st}\left(F\right),2^{nd}\left(F\right)⟩$$
10	9	oveq2d	Could not format ( ph -> ( <. D , E >. -o.F F ) = ( <. D , E >. -o.F <. ( 1st ` F ) , ( 2nd ` F ) >. ) ) : No typesetting found for |- ( ph -> ( <. D , E >. -o.F F ) = ( <. D , E >. -o.F <. ( 1st ` F ) , ( 2nd ` F ) >. ) ) with typecode |-
11	9	fveq2d	Could not format ( ph -> ( ( 1st ` .o. ) ` F ) = ( ( 1st ` .o. ) ` <. ( 1st ` F ) , ( 2nd ` F ) >. ) ) : No typesetting found for |- ( ph -> ( ( 1st ` .o. ) ` F ) = ( ( 1st ` .o. ) ` <. ( 1st ` F ) , ( 2nd ` F ) >. ) ) with typecode |-
12	5 11	eqtrd	Could not format ( ph -> M = ( ( 1st ` .o. ) ` <. ( 1st ` F ) , ( 2nd ` F ) >. ) ) : No typesetting found for |- ( ph -> M = ( ( 1st ` .o. ) ` <. ( 1st ` F ) , ( 2nd ` F ) >. ) ) with typecode |-
13	6	func1st2nd	$$⊢\phi \to 1^{st}\left(F\right)\left(C\mathrm{Func}D\right)2^{nd}\left(F\right)$$
14	1 2 3 4 12 13	prcoftposcurfuco	Could not format ( ph -> ( <. D , E >. -o.F <. ( 1st ` F ) , ( 2nd ` F ) >. ) = M ) : No typesetting found for |- ( ph -> ( <. D , E >. -o.F <. ( 1st ` F ) , ( 2nd ` F ) >. ) = M ) with typecode |-
15	10 14	eqtrd	Could not format ( ph -> ( <. D , E >. -o.F F ) = M ) : No typesetting found for |- ( ph -> ( <. D , E >. -o.F F ) = M ) with typecode |-