Theorem tposcurf11

Description: Value of the double evaluated transposed curry 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)$$
	tposcurf1.b	$$⊢B={\mathrm{Base}}_D$$
	tposcurf11.y	$$⊢\phi \to Y\in B$$
Assertion	tposcurf11	$$⊢\phi \to 1^{st}\left(K\right)\left(Y\right)=Y{1}^{st}\left(F\right)X$$

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		tposcurf1.b	$$⊢B={\mathrm{Base}}_D$$
9		tposcurf11.y	$$⊢\phi \to Y\in B$$
10	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 |-
11	10	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 |-
12	7 11	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 |-
13	12	fveq2d	Could not format ( ph -> ( 1st ` K ) = ( 1st ` ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) ) ) : No typesetting found for |- ( ph -> ( 1st ` K ) = ( 1st ` ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) ) ) with typecode |-
14	13	fveq1d	Could not format ( ph -> ( ( 1st ` K ) ` Y ) = ( ( 1st ` ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) ) ` Y ) ) : No typesetting found for |- ( ph -> ( ( 1st ` K ) ` Y ) = ( ( 1st ` ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) ) ` Y ) ) with typecode |-
15		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 |-
16		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 |-
17	3 4 5 16	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 |-
18		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 |-
19	15 2 3 4 17 8 6 18 9	curf11	Could not format ( ph -> ( ( 1st ` ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) ) ` Y ) = ( X ( 1st ` ( F o.func ( C swapF D ) ) ) Y ) ) : No typesetting found for |- ( ph -> ( ( 1st ` ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) ) ` Y ) = ( X ( 1st ` ( F o.func ( C swapF D ) ) ) Y ) ) with typecode |-
20	3 4 5 16 2 8 6 9	cofuswapf1	Could not format ( ph -> ( X ( 1st ` ( F o.func ( C swapF D ) ) ) Y ) = ( Y ( 1st ` F ) X ) ) : No typesetting found for |- ( ph -> ( X ( 1st ` ( F o.func ( C swapF D ) ) ) Y ) = ( Y ( 1st ` F ) X ) ) with typecode |-
21	14 19 20	3eqtrd	$$⊢\phi \to 1^{st}\left(K\right)\left(Y\right)=Y{1}^{st}\left(F\right)X$$