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	|- ( ph -> G = ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) )
	tposcurfcl.q	|- Q = ( D FuncCat E )
	tposcurfcl.c	|- ( ph -> C e. Cat )
	tposcurfcl.d	|- ( ph -> D e. Cat )
	tposcurfcl.f	|- ( ph -> F e. ( ( D Xc. C ) Func E ) )
Assertion	tposcurfcl	|- ( ph -> G e. ( C Func Q ) )

Proof

Step	Hyp	Ref	Expression
1		tposcurfcl.g	|- ( ph -> G = ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) )
2		tposcurfcl.q	|- Q = ( D FuncCat E )
3		tposcurfcl.c	|- ( ph -> C e. Cat )
4		tposcurfcl.d	|- ( ph -> D e. Cat )
5		tposcurfcl.f	|- ( ph -> F e. ( ( D Xc. C ) Func E ) )
6		eqid	|- ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) = ( <. C , D >. curryF ( F o.func ( C swapF D ) ) )
7		eqidd	|- ( ph -> ( F o.func ( C swapF D ) ) = ( F o.func ( C swapF D ) ) )
8	3 4 5 7	cofuswapfcl	|- ( ph -> ( F o.func ( C swapF D ) ) e. ( ( C Xc. D ) Func E ) )
9	6 2 3 4 8	curfcl	|- ( ph -> ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) e. ( C Func Q ) )
10	1 9	eqeltrd	|- ( ph -> G e. ( C Func Q ) )