Theorem fvmpocurryd

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

	Ref	Expression
Hypotheses	fvmpocurryd.f	$$⊢F=\left(x\in X,y\in Y⟼C\right)$$
	fvmpocurryd.c	$$⊢\phi \to \forall x\in X\forall y\in YC\in V$$
	fvmpocurryd.y	$$⊢\phi \to Y\in W$$
	fvmpocurryd.a	$$⊢\phi \to A\in X$$
	fvmpocurryd.b	$$⊢\phi \to B\in Y$$
Assertion	fvmpocurryd	$$⊢\phi \to curryF\left(A\right)\left(B\right)=AFB$$

Proof

Step	Hyp	Ref	Expression
1		fvmpocurryd.f	$$⊢F=\left(x\in X,y\in Y⟼C\right)$$
2		fvmpocurryd.c	$$⊢\phi \to \forall x\in X\forall y\in YC\in V$$
3		fvmpocurryd.y	$$⊢\phi \to Y\in W$$
4		fvmpocurryd.a	$$⊢\phi \to A\in X$$
5		fvmpocurryd.b	$$⊢\phi \to B\in Y$$
6		csbcom	$$⊢⦋B/b⦌⦋A/a⦌⦋b/y⦌⦋a/x⦌C=⦋A/a⦌⦋B/b⦌⦋b/y⦌⦋a/x⦌C$$
7		csbcow	$$⊢⦋B/b⦌⦋b/y⦌⦋a/x⦌C=⦋B/y⦌⦋a/x⦌C$$
8	7	csbeq2i	$$⊢⦋A/a⦌⦋B/b⦌⦋b/y⦌⦋a/x⦌C=⦋A/a⦌⦋B/y⦌⦋a/x⦌C$$
9		csbcom	$$⊢⦋A/a⦌⦋B/y⦌⦋a/x⦌C=⦋B/y⦌⦋A/a⦌⦋a/x⦌C$$
10		csbcow	$$⊢⦋A/a⦌⦋a/x⦌C=⦋A/x⦌C$$
11	10	csbeq2i	$$⊢⦋B/y⦌⦋A/a⦌⦋a/x⦌C=⦋B/y⦌⦋A/x⦌C$$
12	9 11	eqtri	$$⊢⦋A/a⦌⦋B/y⦌⦋a/x⦌C=⦋B/y⦌⦋A/x⦌C$$
13	6 8 12	3eqtri	$$⊢⦋B/b⦌⦋A/a⦌⦋b/y⦌⦋a/x⦌C=⦋B/y⦌⦋A/x⦌C$$
14		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋A/x⦌C$$
15	14	nfel1	$$⊢Ⅎx⦋A/x⦌C\in V$$
16		nfcsb1v	$$⊢\underset{\_}{Ⅎ}y⦋B/y⦌⦋A/x⦌C$$
17	16	nfel1	$$⊢Ⅎy⦋B/y⦌⦋A/x⦌C\in V$$
18		csbeq1a	$$⊢x=A\to C=⦋A/x⦌C$$
19	18	eleq1d	$$⊢x=A\to \left(C\in V\leftrightarrow ⦋A/x⦌C\in V\right)$$
20		csbeq1a	$$⊢y=B\to ⦋A/x⦌C=⦋B/y⦌⦋A/x⦌C$$
21	20	eleq1d	$$⊢y=B\to \left(⦋A/x⦌C\in V\leftrightarrow ⦋B/y⦌⦋A/x⦌C\in V\right)$$
22	15 17 19 21	rspc2	$$⊢\left(A\in X\wedge B\in Y\right)\to \left(\forall x\in X\forall y\in YC\in V\to ⦋B/y⦌⦋A/x⦌C\in V\right)$$
23	22	imp	$$⊢\left(\left(A\in X\wedge B\in Y\right)\wedge \forall x\in X\forall y\in YC\in V\right)\to ⦋B/y⦌⦋A/x⦌C\in V$$
24	4 5 2 23	syl21anc	$$⊢\phi \to ⦋B/y⦌⦋A/x⦌C\in V$$
25	13 24	eqeltrid	$$⊢\phi \to ⦋B/b⦌⦋A/a⦌⦋b/y⦌⦋a/x⦌C\in V$$
26		eqid	$$⊢\left(b\in Y⟼⦋A/a⦌⦋b/y⦌⦋a/x⦌C\right)=\left(b\in Y⟼⦋A/a⦌⦋b/y⦌⦋a/x⦌C\right)$$
27	26	fvmpts	$$⊢\left(B\in Y\wedge ⦋B/b⦌⦋A/a⦌⦋b/y⦌⦋a/x⦌C\in V\right)\to \left(b\in Y⟼⦋A/a⦌⦋b/y⦌⦋a/x⦌C\right)\left(B\right)=⦋B/b⦌⦋A/a⦌⦋b/y⦌⦋a/x⦌C$$
28	5 25 27	syl2anc	$$⊢\phi \to \left(b\in Y⟼⦋A/a⦌⦋b/y⦌⦋a/x⦌C\right)\left(B\right)=⦋B/b⦌⦋A/a⦌⦋b/y⦌⦋a/x⦌C$$
29		nfcv	$$⊢\underset{\_}{Ⅎ}aC$$
30		nfcv	$$⊢\underset{\_}{Ⅎ}bC$$
31		nfcv	$$⊢\underset{\_}{Ⅎ}xb$$
32		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋a/x⦌C$$
33	31 32	nfcsbw	$$⊢\underset{\_}{Ⅎ}x⦋b/y⦌⦋a/x⦌C$$
34		nfcsb1v	$$⊢\underset{\_}{Ⅎ}y⦋b/y⦌⦋a/x⦌C$$
35		csbeq1a	$$⊢x=a\to C=⦋a/x⦌C$$
36		csbeq1a	$$⊢y=b\to ⦋a/x⦌C=⦋b/y⦌⦋a/x⦌C$$
37	35 36	sylan9eq	$$⊢\left(x=a\wedge y=b\right)\to C=⦋b/y⦌⦋a/x⦌C$$
38	29 30 33 34 37	cbvmpo	$$⊢\left(x\in X,y\in Y⟼C\right)=\left(a\in X,b\in Y⟼⦋b/y⦌⦋a/x⦌C\right)$$
39	1 38	eqtri	$$⊢F=\left(a\in X,b\in Y⟼⦋b/y⦌⦋a/x⦌C\right)$$
40	32	nfel1	$$⊢Ⅎx⦋a/x⦌C\in V$$
41	34	nfel1	$$⊢Ⅎy⦋b/y⦌⦋a/x⦌C\in V$$
42	35	eleq1d	$$⊢x=a\to \left(C\in V\leftrightarrow ⦋a/x⦌C\in V\right)$$
43	36	eleq1d	$$⊢y=b\to \left(⦋a/x⦌C\in V\leftrightarrow ⦋b/y⦌⦋a/x⦌C\in V\right)$$
44	40 41 42 43	rspc2	$$⊢\left(a\in X\wedge b\in Y\right)\to \left(\forall x\in X\forall y\in YC\in V\to ⦋b/y⦌⦋a/x⦌C\in V\right)$$
45	2 44	mpan9	$$⊢\left(\phi \wedge \left(a\in X\wedge b\in Y\right)\right)\to ⦋b/y⦌⦋a/x⦌C\in V$$
46	45	ralrimivva	$$⊢\phi \to \forall a\in X\forall b\in Y⦋b/y⦌⦋a/x⦌C\in V$$
47	5	ne0d	$$⊢\phi \to Y\ne \varnothing$$
48	39 46 47 3 4	mpocurryvald	$$⊢\phi \to curryF\left(A\right)=\left(b\in Y⟼⦋A/a⦌⦋b/y⦌⦋a/x⦌C\right)$$
49	48	fveq1d	$$⊢\phi \to curryF\left(A\right)\left(B\right)=\left(b\in Y⟼⦋A/a⦌⦋b/y⦌⦋a/x⦌C\right)\left(B\right)$$
50	1	a1i	$$⊢\phi \to F=\left(x\in X,y\in Y⟼C\right)$$
51		csbcow	$$⊢⦋y/b⦌⦋b/y⦌⦋a/x⦌C=⦋y/y⦌⦋a/x⦌C$$
52		csbid	$$⊢⦋y/y⦌⦋a/x⦌C=⦋a/x⦌C$$
53	51 52	eqtr2i	$$⊢⦋a/x⦌C=⦋y/b⦌⦋b/y⦌⦋a/x⦌C$$
54	53	a1i	$$⊢\phi \to ⦋a/x⦌C=⦋y/b⦌⦋b/y⦌⦋a/x⦌C$$
55	54	csbeq2dv	$$⊢\phi \to ⦋x/a⦌⦋a/x⦌C=⦋x/a⦌⦋y/b⦌⦋b/y⦌⦋a/x⦌C$$
56		csbcow	$$⊢⦋x/a⦌⦋a/x⦌C=⦋x/x⦌C$$
57		csbid	$$⊢⦋x/x⦌C=C$$
58	56 57	eqtri	$$⊢⦋x/a⦌⦋a/x⦌C=C$$
59		csbcom	$$⊢⦋x/a⦌⦋y/b⦌⦋b/y⦌⦋a/x⦌C=⦋y/b⦌⦋x/a⦌⦋b/y⦌⦋a/x⦌C$$
60	55 58 59	3eqtr3g	$$⊢\phi \to C=⦋y/b⦌⦋x/a⦌⦋b/y⦌⦋a/x⦌C$$
61		csbeq1	$$⊢x=A\to ⦋x/a⦌⦋b/y⦌⦋a/x⦌C=⦋A/a⦌⦋b/y⦌⦋a/x⦌C$$
62	61	adantr	$$⊢\left(x=A\wedge y=B\right)\to ⦋x/a⦌⦋b/y⦌⦋a/x⦌C=⦋A/a⦌⦋b/y⦌⦋a/x⦌C$$
63	62	csbeq2dv	$$⊢\left(x=A\wedge y=B\right)\to ⦋y/b⦌⦋x/a⦌⦋b/y⦌⦋a/x⦌C=⦋y/b⦌⦋A/a⦌⦋b/y⦌⦋a/x⦌C$$
64		csbeq1	$$⊢y=B\to ⦋y/b⦌⦋A/a⦌⦋b/y⦌⦋a/x⦌C=⦋B/b⦌⦋A/a⦌⦋b/y⦌⦋a/x⦌C$$
65	64	adantl	$$⊢\left(x=A\wedge y=B\right)\to ⦋y/b⦌⦋A/a⦌⦋b/y⦌⦋a/x⦌C=⦋B/b⦌⦋A/a⦌⦋b/y⦌⦋a/x⦌C$$
66	63 65	eqtrd	$$⊢\left(x=A\wedge y=B\right)\to ⦋y/b⦌⦋x/a⦌⦋b/y⦌⦋a/x⦌C=⦋B/b⦌⦋A/a⦌⦋b/y⦌⦋a/x⦌C$$
67	60 66	sylan9eq	$$⊢\left(\phi \wedge \left(x=A\wedge y=B\right)\right)\to C=⦋B/b⦌⦋A/a⦌⦋b/y⦌⦋a/x⦌C$$
68		eqidd	$$⊢\left(\phi \wedge x=A\right)\to Y=Y$$
69		nfv	$$⊢Ⅎx\phi$$
70		nfv	$$⊢Ⅎy\phi$$
71		nfcv	$$⊢\underset{\_}{Ⅎ}yA$$
72		nfcv	$$⊢\underset{\_}{Ⅎ}xB$$
73		nfcv	$$⊢\underset{\_}{Ⅎ}xA$$
74	73 33	nfcsbw	$$⊢\underset{\_}{Ⅎ}x⦋A/a⦌⦋b/y⦌⦋a/x⦌C$$
75	72 74	nfcsbw	$$⊢\underset{\_}{Ⅎ}x⦋B/b⦌⦋A/a⦌⦋b/y⦌⦋a/x⦌C$$
76	13 16	nfcxfr	$$⊢\underset{\_}{Ⅎ}y⦋B/b⦌⦋A/a⦌⦋b/y⦌⦋a/x⦌C$$
77	50 67 68 4 5 25 69 70 71 72 75 76	ovmpodxf	$$⊢\phi \to AFB=⦋B/b⦌⦋A/a⦌⦋b/y⦌⦋a/x⦌C$$
78	28 49 77	3eqtr4d	$$⊢\phi \to curryF\left(A\right)\left(B\right)=AFB$$