Theorem mpocurryvald

Description: The value of a curried operation given in maps-to notation is a function over the second argument of the original operation. (Contributed by AV, 27-Oct-2019)

	Ref	Expression
Hypotheses	mpocurryd.f	|- F = ( x e. X , y e. Y |-> C )
	mpocurryd.c	|- ( ph -> A. x e. X A. y e. Y C e. V )
	mpocurryd.n	|- ( ph -> Y =/= (/) )
	mpocurryvald.y	|- ( ph -> Y e. W )
	mpocurryvald.a	|- ( ph -> A e. X )
Assertion	mpocurryvald	|- ( ph -> ( curry F ` A ) = ( y e. Y |-> [_ A / x ]_ C ) )

Proof

Step	Hyp	Ref	Expression
1		mpocurryd.f	|- F = ( x e. X , y e. Y |-> C )
2		mpocurryd.c	|- ( ph -> A. x e. X A. y e. Y C e. V )
3		mpocurryd.n	|- ( ph -> Y =/= (/) )
4		mpocurryvald.y	|- ( ph -> Y e. W )
5		mpocurryvald.a	|- ( ph -> A e. X )
6	1 2 3	mpocurryd	|- ( ph -> curry F = ( x e. X |-> ( y e. Y |-> C ) ) )
7		nfcv	|- F/_ a ( y e. Y |-> C )
8		nfcv	|- F/_ x Y
9		nfcsb1v	|- F/_ x [_ a / x ]_ C
10	8 9	nfmpt	|- F/_ x ( y e. Y |-> [_ a / x ]_ C )
11		csbeq1a	|- ( x = a -> C = [_ a / x ]_ C )
12	11	mpteq2dv	|- ( x = a -> ( y e. Y |-> C ) = ( y e. Y |-> [_ a / x ]_ C ) )
13	7 10 12	cbvmpt	|- ( x e. X |-> ( y e. Y |-> C ) ) = ( a e. X |-> ( y e. Y |-> [_ a / x ]_ C ) )
14	6 13	eqtrdi	|- ( ph -> curry F = ( a e. X |-> ( y e. Y |-> [_ a / x ]_ C ) ) )
15		csbeq1	|- ( a = A -> [_ a / x ]_ C = [_ A / x ]_ C )
16	15	adantl	|- ( ( ph /\ a = A ) -> [_ a / x ]_ C = [_ A / x ]_ C )
17	16	mpteq2dv	|- ( ( ph /\ a = A ) -> ( y e. Y |-> [_ a / x ]_ C ) = ( y e. Y |-> [_ A / x ]_ C ) )
18	4	mptexd	|- ( ph -> ( y e. Y |-> [_ A / x ]_ C ) e. _V )
19	14 17 5 18	fvmptd	|- ( ph -> ( curry F ` A ) = ( y e. Y |-> [_ A / x ]_ C ) )