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	|- ( ph -> G = ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) )
	tposcurf2.a	|- A = ( Base ` C )
	tposcurf2.c	|- ( ph -> C e. Cat )
	tposcurf2.d	|- ( ph -> D e. Cat )
	tposcurf2.f	|- ( ph -> F e. ( ( D Xc. C ) Func E ) )
	tposcurf2.b	|- B = ( Base ` D )
	tposcurf2.h	|- H = ( Hom ` C )
	tposcurf2.i	|- I = ( Id ` D )
	tposcurf2.x	|- ( ph -> X e. A )
	tposcurf2.y	|- ( ph -> Y e. A )
	tposcurf2.k	|- ( ph -> K e. ( X H Y ) )
	tposcurf2.l	|- ( ph -> L = ( ( X ( 2nd ` G ) Y ) ` K ) )
	tposcurf2.z	|- ( ph -> Z e. B )
Assertion	tposcurf2val	|- ( ph -> ( L ` Z ) = ( ( I ` Z ) ( <. Z , X >. ( 2nd ` F ) <. Z , Y >. ) K ) )

Proof

Step	Hyp	Ref	Expression
1		tposcurf2.g	|- ( ph -> G = ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) )
2		tposcurf2.a	|- A = ( Base ` C )
3		tposcurf2.c	|- ( ph -> C e. Cat )
4		tposcurf2.d	|- ( ph -> D e. Cat )
5		tposcurf2.f	|- ( ph -> F e. ( ( D Xc. C ) Func E ) )
6		tposcurf2.b	|- B = ( Base ` D )
7		tposcurf2.h	|- H = ( Hom ` C )
8		tposcurf2.i	|- I = ( Id ` D )
9		tposcurf2.x	|- ( ph -> X e. A )
10		tposcurf2.y	|- ( ph -> Y e. A )
11		tposcurf2.k	|- ( ph -> K e. ( X H Y ) )
12		tposcurf2.l	|- ( ph -> L = ( ( X ( 2nd ` G ) Y ) ` K ) )
13		tposcurf2.z	|- ( ph -> Z e. B )
14	1 2 3 4 5 6 7 8 9 10 11 12	tposcurf2	|- ( ph -> L = ( z e. B |-> ( ( I ` z ) ( <. z , X >. ( 2nd ` F ) <. z , Y >. ) K ) ) )
15		simpr	|- ( ( ph /\ z = Z ) -> z = Z )
16	15	opeq1d	|- ( ( ph /\ z = Z ) -> <. z , X >. = <. Z , X >. )
17	15	opeq1d	|- ( ( ph /\ z = Z ) -> <. z , Y >. = <. Z , Y >. )
18	16 17	oveq12d	|- ( ( ph /\ z = Z ) -> ( <. z , X >. ( 2nd ` F ) <. z , Y >. ) = ( <. Z , X >. ( 2nd ` F ) <. Z , Y >. ) )
19	15	fveq2d	|- ( ( ph /\ z = Z ) -> ( I ` z ) = ( I ` Z ) )
20		eqidd	|- ( ( ph /\ z = Z ) -> K = K )
21	18 19 20	oveq123d	|- ( ( ph /\ z = Z ) -> ( ( I ` z ) ( <. z , X >. ( 2nd ` F ) <. z , Y >. ) K ) = ( ( I ` Z ) ( <. Z , X >. ( 2nd ` F ) <. Z , Y >. ) K ) )
22		ovexd	|- ( ph -> ( ( I ` Z ) ( <. Z , X >. ( 2nd ` F ) <. Z , Y >. ) K ) e. _V )
23	14 21 13 22	fvmptd	|- ( ph -> ( L ` Z ) = ( ( I ` Z ) ( <. Z , X >. ( 2nd ` F ) <. Z , Y >. ) K ) )