Theorem tposcurf2

Description: Value of the transposed curry functor at a morphism. (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)$$
Assertion	tposcurf2	$$⊢\phi \to L=\left(z\in B⟼I\left(z\right)\left(⟨z,X⟩2^{nd}\left(F\right)⟨z,Y⟩\right)K\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	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 |-
14	13	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 |-
15	14	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 |-
16	12 15	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 |-
17		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 |-
18		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 |-
19	3 4 5 18	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 |-
20		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 |-
21	17 2 3 4 19 6 7 8 9 10 11 20	curf2	Could not format ( ph -> ( ( X ( 2nd ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) Y ) ` K ) = ( z e. B |-> ( K ( <. X , z >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. Y , z >. ) ( I ` z ) ) ) ) : No typesetting found for |- ( ph -> ( ( X ( 2nd ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) Y ) ` K ) = ( z e. B |-> ( K ( <. X , z >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. Y , z >. ) ( I ` z ) ) ) ) with typecode |-
22	3	adantr	$$⊢\left(\phi \wedge z\in B\right)\to C\in \mathrm{Cat}$$
23	4	adantr	$$⊢\left(\phi \wedge z\in B\right)\to D\in \mathrm{Cat}$$
24	5	adantr	$$⊢\left(\phi \wedge z\in B\right)\to F\in \left(\left(D{\times }_{c}C\right)\mathrm{Func}E\right)$$
25		eqidd	Could not format ( ( ph /\ z e. B ) -> ( F o.func ( C swapF D ) ) = ( F o.func ( C swapF D ) ) ) : No typesetting found for |- ( ( ph /\ z e. B ) -> ( F o.func ( C swapF D ) ) = ( F o.func ( C swapF D ) ) ) with typecode |-
26	9	adantr	$$⊢\left(\phi \wedge z\in B\right)\to X\in A$$
27		simpr	$$⊢\left(\phi \wedge z\in B\right)\to z\in B$$
28	10	adantr	$$⊢\left(\phi \wedge z\in B\right)\to Y\in A$$
29		eqid	$$⊢\mathrm{Hom}\left(D\right)=\mathrm{Hom}\left(D\right)$$
30	11	adantr	$$⊢\left(\phi \wedge z\in B\right)\to K\in \left(XHY\right)$$
31	6 29 8 23 27	catidcl	$$⊢\left(\phi \wedge z\in B\right)\to I\left(z\right)\in \left(z\mathrm{Hom}\left(D\right)z\right)$$
32	22 23 24 25 2 6 26 27 28 27 7 29 30 31	cofuswapf2	Could not format ( ( ph /\ z e. B ) -> ( K ( <. X , z >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. Y , z >. ) ( I ` z ) ) = ( ( I ` z ) ( <. z , X >. ( 2nd ` F ) <. z , Y >. ) K ) ) : No typesetting found for |- ( ( ph /\ z e. B ) -> ( K ( <. X , z >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. Y , z >. ) ( I ` z ) ) = ( ( I ` z ) ( <. z , X >. ( 2nd ` F ) <. z , Y >. ) K ) ) with typecode |-
33	32	mpteq2dva	Could not format ( ph -> ( z e. B |-> ( K ( <. X , z >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. Y , z >. ) ( I ` z ) ) ) = ( z e. B |-> ( ( I ` z ) ( <. z , X >. ( 2nd ` F ) <. z , Y >. ) K ) ) ) : No typesetting found for |- ( ph -> ( z e. B |-> ( K ( <. X , z >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. Y , z >. ) ( I ` z ) ) ) = ( z e. B |-> ( ( I ` z ) ( <. z , X >. ( 2nd ` F ) <. z , Y >. ) K ) ) ) with typecode |-
34	16 21 33	3eqtrd	$$⊢\phi \to L=\left(z\in B⟼I\left(z\right)\left(⟨z,X⟩2^{nd}\left(F\right)⟨z,Y⟩\right)K\right)$$