Theorem tposcurf2cl

Description: The transposed curry functor at a morphism is a natural transformation. (Contributed by Zhi Wang, 10-Oct-2025)

	Ref	Expression
Hypotheses	tposcurf2.g	No typesetting found for |- ( ph -> G = ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) with typecode |-
	tposcurf2.a	$$⊢A={\mathrm{Base}}_C$$
	tposcurf2.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	tposcurf2.d	$$⊢\phi \to D\in \mathrm{Cat}$$
	tposcurf2.f	$$⊢\phi \to F\in \left(\left(D{\times }_{c}C\right)\mathrm{Func}E\right)$$
	tposcurf2.b	$$⊢B={\mathrm{Base}}_D$$
	tposcurf2.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
	tposcurf2.i	$$⊢I=\mathrm{Id}\left(D\right)$$
	tposcurf2.x	$$⊢\phi \to X\in A$$
	tposcurf2.y	$$⊢\phi \to Y\in A$$
	tposcurf2.k	$$⊢\phi \to K\in \left(XHY\right)$$
	tposcurf2.l	$$⊢\phi \to L=\left(X{2}^{nd}\left(G\right)Y\right)\left(K\right)$$
	tposcurf2.n	$$⊢N=D\mathrm{Nat}E$$
Assertion	tposcurf2cl	$$⊢\phi \to L\in \left(1^{st}\left(G\right)\left(X\right)N{1}^{st}\left(G\right)\left(Y\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		tposcurf2.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		tposcurf2.a	$$⊢A={\mathrm{Base}}_C$$
3		tposcurf2.c	$$⊢\phi \to C\in \mathrm{Cat}$$
4		tposcurf2.d	$$⊢\phi \to D\in \mathrm{Cat}$$
5		tposcurf2.f	$$⊢\phi \to F\in \left(\left(D{\times }_{c}C\right)\mathrm{Func}E\right)$$
6		tposcurf2.b	$$⊢B={\mathrm{Base}}_D$$
7		tposcurf2.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
8		tposcurf2.i	$$⊢I=\mathrm{Id}\left(D\right)$$
9		tposcurf2.x	$$⊢\phi \to X\in A$$
10		tposcurf2.y	$$⊢\phi \to Y\in A$$
11		tposcurf2.k	$$⊢\phi \to K\in \left(XHY\right)$$
12		tposcurf2.l	$$⊢\phi \to L=\left(X{2}^{nd}\left(G\right)Y\right)\left(K\right)$$
13		tposcurf2.n	$$⊢N=D\mathrm{Nat}E$$
14		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 |-
15		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 |-
16	3 4 5 15	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 |-
17		eqid	Could not format ( ( X ( 2nd ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) Y ) ` K ) = ( ( X ( 2nd ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) Y ) ` K ) : No typesetting found for |- ( ( X ( 2nd ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) Y ) ` K ) = ( ( X ( 2nd ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) Y ) ` K ) with typecode |-
18	14 2 3 4 16 6 7 8 9 10 11 17 13	curf2cl	Could not format ( ph -> ( ( X ( 2nd ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) Y ) ` K ) e. ( ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) N ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` Y ) ) ) : No typesetting found for |- ( ph -> ( ( X ( 2nd ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) Y ) ` K ) e. ( ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) N ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` Y ) ) ) with typecode |-
19	1	fveq2d	Could not format ( ph -> ( 2nd ` G ) = ( 2nd ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ) : No typesetting found for |- ( ph -> ( 2nd ` G ) = ( 2nd ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ) with typecode |-
20	19	oveqd	Could not format ( ph -> ( X ( 2nd ` G ) Y ) = ( X ( 2nd ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) Y ) ) : No typesetting found for |- ( ph -> ( X ( 2nd ` G ) Y ) = ( X ( 2nd ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) Y ) ) with typecode |-
21	20	fveq1d	Could not format ( ph -> ( ( X ( 2nd ` G ) Y ) ` K ) = ( ( X ( 2nd ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) Y ) ` K ) ) : No typesetting found for |- ( ph -> ( ( X ( 2nd ` G ) Y ) ` K ) = ( ( X ( 2nd ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) Y ) ` K ) ) with typecode |-
22	12 21	eqtrd	Could not format ( ph -> L = ( ( X ( 2nd ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) Y ) ` K ) ) : No typesetting found for |- ( ph -> L = ( ( X ( 2nd ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) Y ) ` K ) ) with typecode |-
23	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 |-
24	23	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 |-
25	23	fveq1d	Could not format ( ph -> ( ( 1st ` G ) ` Y ) = ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` Y ) ) : No typesetting found for |- ( ph -> ( ( 1st ` G ) ` Y ) = ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` Y ) ) with typecode |-
26	24 25	oveq12d	Could not format ( ph -> ( ( ( 1st ` G ) ` X ) N ( ( 1st ` G ) ` Y ) ) = ( ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) N ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` Y ) ) ) : No typesetting found for |- ( ph -> ( ( ( 1st ` G ) ` X ) N ( ( 1st ` G ) ` Y ) ) = ( ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) N ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` Y ) ) ) with typecode |-
27	18 22 26	3eltr4d	$$⊢\phi \to L\in \left(1^{st}\left(G\right)\left(X\right)N{1}^{st}\left(G\right)\left(Y\right)\right)$$