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=\left(x\in X,y\in Y⟼C\right)$$
	mpocurryd.c	$$⊢\phi \to \forall x\in X\forall y\in YC\in V$$
	mpocurryd.n	$$⊢\phi \to Y\ne \varnothing$$
	mpocurryvald.y	$$⊢\phi \to Y\in W$$
	mpocurryvald.a	$$⊢\phi \to A\in X$$
Assertion	mpocurryvald	$$⊢\phi \to curryF\left(A\right)=\left(y\in Y⟼⦋A/x⦌C\right)$$

Proof

Step	Hyp	Ref	Expression
1		mpocurryd.f	$$⊢F=\left(x\in X,y\in Y⟼C\right)$$
2		mpocurryd.c	$$⊢\phi \to \forall x\in X\forall y\in YC\in V$$
3		mpocurryd.n	$$⊢\phi \to Y\ne \varnothing$$
4		mpocurryvald.y	$$⊢\phi \to Y\in W$$
5		mpocurryvald.a	$$⊢\phi \to A\in X$$
6	1 2 3	mpocurryd	$$⊢\phi \to curryF=\left(x\in X⟼\left(y\in Y⟼C\right)\right)$$
7		nfcv	$$⊢\underset{\_}{Ⅎ}a\left(y\in Y⟼C\right)$$
8		nfcv	$$⊢\underset{\_}{Ⅎ}xY$$
9		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋a/x⦌C$$
10	8 9	nfmpt	$$⊢\underset{\_}{Ⅎ}x\left(y\in Y⟼⦋a/x⦌C\right)$$
11		csbeq1a	$$⊢x=a\to C=⦋a/x⦌C$$
12	11	mpteq2dv	$$⊢x=a\to \left(y\in Y⟼C\right)=\left(y\in Y⟼⦋a/x⦌C\right)$$
13	7 10 12	cbvmpt	$$⊢\left(x\in X⟼\left(y\in Y⟼C\right)\right)=\left(a\in X⟼\left(y\in Y⟼⦋a/x⦌C\right)\right)$$
14	6 13	eqtrdi	$$⊢\phi \to curryF=\left(a\in X⟼\left(y\in Y⟼⦋a/x⦌C\right)\right)$$
15		csbeq1	$$⊢a=A\to ⦋a/x⦌C=⦋A/x⦌C$$
16	15	adantl	$$⊢\left(\phi \wedge a=A\right)\to ⦋a/x⦌C=⦋A/x⦌C$$
17	16	mpteq2dv	$$⊢\left(\phi \wedge a=A\right)\to \left(y\in Y⟼⦋a/x⦌C\right)=\left(y\in Y⟼⦋A/x⦌C\right)$$
18	4	mptexd	$$⊢\phi \to \left(y\in Y⟼⦋A/x⦌C\right)\in \mathrm{V}$$
19	14 17 5 18	fvmptd	$$⊢\phi \to curryF\left(A\right)=\left(y\in Y⟼⦋A/x⦌C\right)$$