Theorem tposcurf2val

Description: Value of a component of the transposed curry functor 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.z	$$⊢\phi \to Z\in B$$
Assertion	tposcurf2val	$$⊢\phi \to L\left(Z\right)=I\left(Z\right)\left(⟨Z,X⟩2^{nd}\left(F\right)⟨Z,Y⟩\right)K$$

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.z	$$⊢\phi \to Z\in B$$
14	1 2 3 4 5 6 7 8 9 10 11 12	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)$$
15		simpr	$$⊢\left(\phi \wedge z=Z\right)\to z=Z$$
16	15	opeq1d	$$⊢\left(\phi \wedge z=Z\right)\to ⟨z,X⟩=⟨Z,X⟩$$
17	15	opeq1d	$$⊢\left(\phi \wedge z=Z\right)\to ⟨z,Y⟩=⟨Z,Y⟩$$
18	16 17	oveq12d	$$⊢\left(\phi \wedge z=Z\right)\to ⟨z,X⟩2^{nd}\left(F\right)⟨z,Y⟩=⟨Z,X⟩2^{nd}\left(F\right)⟨Z,Y⟩$$
19	15	fveq2d	$$⊢\left(\phi \wedge z=Z\right)\to I\left(z\right)=I\left(Z\right)$$
20		eqidd	$$⊢\left(\phi \wedge z=Z\right)\to K=K$$
21	18 19 20	oveq123d	$$⊢\left(\phi \wedge z=Z\right)\to I\left(z\right)\left(⟨z,X⟩2^{nd}\left(F\right)⟨z,Y⟩\right)K=I\left(Z\right)\left(⟨Z,X⟩2^{nd}\left(F\right)⟨Z,Y⟩\right)K$$
22		ovexd	$$⊢\phi \to I\left(Z\right)\left(⟨Z,X⟩2^{nd}\left(F\right)⟨Z,Y⟩\right)K\in \mathrm{V}$$
23	14 21 13 22	fvmptd	$$⊢\phi \to L\left(Z\right)=I\left(Z\right)\left(⟨Z,X⟩2^{nd}\left(F\right)⟨Z,Y⟩\right)K$$