Theorem tposcurf1cl

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

	Ref	Expression
Hypotheses	tposcurf1.g	No typesetting found for |- ( ph -> G = ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) with typecode |-
	tposcurf1.a	$$⊢A={\mathrm{Base}}_C$$
	tposcurf1.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	tposcurf1.d	$$⊢\phi \to D\in \mathrm{Cat}$$
	tposcurf1.f	$$⊢\phi \to F\in \left(\left(D{\times }_{c}C\right)\mathrm{Func}E\right)$$
	tposcurf1.x	$$⊢\phi \to X\in A$$
	tposcurf1.k	$$⊢\phi \to K=1^{st}\left(G\right)\left(X\right)$$
Assertion	tposcurf1cl	$$⊢\phi \to K\in \left(D\mathrm{Func}E\right)$$

Proof

Step	Hyp	Ref	Expression
1		tposcurf1.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		tposcurf1.a	$$⊢A={\mathrm{Base}}_C$$
3		tposcurf1.c	$$⊢\phi \to C\in \mathrm{Cat}$$
4		tposcurf1.d	$$⊢\phi \to D\in \mathrm{Cat}$$
5		tposcurf1.f	$$⊢\phi \to F\in \left(\left(D{\times }_{c}C\right)\mathrm{Func}E\right)$$
6		tposcurf1.x	$$⊢\phi \to X\in A$$
7		tposcurf1.k	$$⊢\phi \to K=1^{st}\left(G\right)\left(X\right)$$
8	1	fveq2d	Could not format ( ph -> ( 1st ` G ) = ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ) : No typesetting found for |- ( ph -> ( 1st ` G ) = ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ) with typecode |-
9	8	fveq1d	Could not format ( ph -> ( ( 1st ` G ) ` X ) = ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) ) : No typesetting found for |- ( ph -> ( ( 1st ` G ) ` X ) = ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) ) with typecode |-
10	7 9	eqtrd	Could not format ( ph -> K = ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) ) : No typesetting found for |- ( ph -> K = ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) ) with typecode |-
11		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 |-
12		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 |-
13	3 4 5 12	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 |-
14		eqid	$$⊢{\mathrm{Base}}_D={\mathrm{Base}}_D$$
15		eqid	Could not format ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) = ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) : No typesetting found for |- ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) = ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) with typecode |-
16	11 2 3 4 13 14 6 15	curf1cl	Could not format ( ph -> ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) e. ( D Func E ) ) : No typesetting found for |- ( ph -> ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) e. ( D Func E ) ) with typecode |-
17	10 16	eqeltrd	$$⊢\phi \to K\in \left(D\mathrm{Func}E\right)$$