Theorem tposcurfcl

Description: The transposed curry functor of a functor F : D X. C --> E is a functor tposcurry ( F ) : C --> ( D --> E ) . (Contributed by Zhi Wang, 9-Oct-2025)

	Ref	Expression
Hypotheses	tposcurfcl.g	No typesetting found for |- ( ph -> G = ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) with typecode |-
	tposcurfcl.q	$$⊢Q=D\mathrm{FuncCat}E$$
	tposcurfcl.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	tposcurfcl.d	$$⊢\phi \to D\in \mathrm{Cat}$$
	tposcurfcl.f	$$⊢\phi \to F\in \left(\left(D{\times }_{c}C\right)\mathrm{Func}E\right)$$
Assertion	tposcurfcl	$$⊢\phi \to G\in \left(C\mathrm{Func}Q\right)$$

Proof

Step	Hyp	Ref	Expression
1		tposcurfcl.g	Could not format ( ph -> G = ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) : No typesetting found for |- ( ph -> G = ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) with typecode |-
2		tposcurfcl.q	$$⊢Q=D\mathrm{FuncCat}E$$
3		tposcurfcl.c	$$⊢\phi \to C\in \mathrm{Cat}$$
4		tposcurfcl.d	$$⊢\phi \to D\in \mathrm{Cat}$$
5		tposcurfcl.f	$$⊢\phi \to F\in \left(\left(D{\times }_{c}C\right)\mathrm{Func}E\right)$$
6		eqid	Could not format ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) = ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) : No typesetting found for |- ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) = ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) with typecode |-
7		eqidd	Could not format ( ph -> ( F o.func ( C swapF D ) ) = ( F o.func ( C swapF D ) ) ) : No typesetting found for |- ( ph -> ( F o.func ( C swapF D ) ) = ( F o.func ( C swapF D ) ) ) with typecode |-
8	3 4 5 7	cofuswapfcl	Could not format ( ph -> ( F o.func ( C swapF D ) ) e. ( ( C Xc. D ) Func E ) ) : No typesetting found for |- ( ph -> ( F o.func ( C swapF D ) ) e. ( ( C Xc. D ) Func E ) ) with typecode |-
9	6 2 3 4 8	curfcl	Could not format ( ph -> ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) e. ( C Func Q ) ) : No typesetting found for |- ( ph -> ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) e. ( C Func Q ) ) with typecode |-
10	1 9	eqeltrd	$$⊢\phi \to G\in \left(C\mathrm{Func}Q\right)$$