Theorem tposcurf1cl

Description: The partially evaluated transposed curry functor is a functor. (Contributed by Zhi Wang, 9-Oct-2025)

	Ref	Expression
Hypotheses	tposcurf1.g	|- ( ph -> G = ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) )
	tposcurf1.a	|- A = ( Base ` C )
	tposcurf1.c	|- ( ph -> C e. Cat )
	tposcurf1.d	|- ( ph -> D e. Cat )
	tposcurf1.f	|- ( ph -> F e. ( ( D Xc. C ) Func E ) )
	tposcurf1.x	|- ( ph -> X e. A )
	tposcurf1.k	|- ( ph -> K = ( ( 1st ` G ) ` X ) )
Assertion	tposcurf1cl	|- ( ph -> K e. ( D Func E ) )

Proof

Step	Hyp	Ref	Expression
1		tposcurf1.g	|- ( ph -> G = ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) )
2		tposcurf1.a	|- A = ( Base ` C )
3		tposcurf1.c	|- ( ph -> C e. Cat )
4		tposcurf1.d	|- ( ph -> D e. Cat )
5		tposcurf1.f	|- ( ph -> F e. ( ( D Xc. C ) Func E ) )
6		tposcurf1.x	|- ( ph -> X e. A )
7		tposcurf1.k	|- ( ph -> K = ( ( 1st ` G ) ` X ) )
8	1	fveq2d	|- ( ph -> ( 1st ` G ) = ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) )
9	8	fveq1d	|- ( ph -> ( ( 1st ` G ) ` X ) = ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) )
10	7 9	eqtrd	|- ( ph -> K = ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) )
11		eqid	|- ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) = ( <. C , D >. curryF ( F o.func ( C swapF D ) ) )
12		eqidd	|- ( ph -> ( F o.func ( C swapF D ) ) = ( F o.func ( C swapF D ) ) )
13	3 4 5 12	cofuswapfcl	|- ( ph -> ( F o.func ( C swapF D ) ) e. ( ( C Xc. D ) Func E ) )
14		eqid	|- ( Base ` D ) = ( Base ` D )
15		eqid	|- ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) = ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X )
16	11 2 3 4 13 14 6 15	curf1cl	|- ( ph -> ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) e. ( D Func E ) )
17	10 16	eqeltrd	|- ( ph -> K e. ( D Func E ) )