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	⊢ 𝐹 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐶 )
	fvmpocurryd.c	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 𝐶 ∈ 𝑉 )
	fvmpocurryd.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑊 )
	fvmpocurryd.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
	fvmpocurryd.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑌 )
Assertion	fvmpocurryd	⊢ ( 𝜑 → ( ( curry 𝐹 ‘ 𝐴 ) ‘ 𝐵 ) = ( 𝐴 𝐹 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		fvmpocurryd.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐶 )
2		fvmpocurryd.c	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 𝐶 ∈ 𝑉 )
3		fvmpocurryd.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑊 )
4		fvmpocurryd.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
5		fvmpocurryd.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑌 )
6		csbcom	⊢ ⦋ 𝐵 / 𝑏 ⦌ ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝐵 / 𝑏 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶
7		csbcow	⊢ ⦋ 𝐵 / 𝑏 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝐵 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶
8	7	csbeq2i	⊢ ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝐵 / 𝑏 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝐵 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶
9		csbcom	⊢ ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝐵 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝐵 / 𝑦 ⦌ ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶
10		csbcow	⊢ ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝐴 / 𝑥 ⦌ 𝐶
11	10	csbeq2i	⊢ ⦋ 𝐵 / 𝑦 ⦌ ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝐵 / 𝑦 ⦌ ⦋ 𝐴 / 𝑥 ⦌ 𝐶
12	9 11	eqtri	⊢ ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝐵 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝐵 / 𝑦 ⦌ ⦋ 𝐴 / 𝑥 ⦌ 𝐶
13	6 8 12	3eqtri	⊢ ⦋ 𝐵 / 𝑏 ⦌ ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝐵 / 𝑦 ⦌ ⦋ 𝐴 / 𝑥 ⦌ 𝐶
14		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝐴 / 𝑥 ⦌ 𝐶
15	14	nfel1	⊢ Ⅎ 𝑥 ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ∈ 𝑉
16		nfcsb1v	⊢ Ⅎ 𝑦 ⦋ 𝐵 / 𝑦 ⦌ ⦋ 𝐴 / 𝑥 ⦌ 𝐶
17	16	nfel1	⊢ Ⅎ 𝑦 ⦋ 𝐵 / 𝑦 ⦌ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ∈ 𝑉
18		csbeq1a	⊢ ( 𝑥 = 𝐴 → 𝐶 = ⦋ 𝐴 / 𝑥 ⦌ 𝐶 )
19	18	eleq1d	⊢ ( 𝑥 = 𝐴 → ( 𝐶 ∈ 𝑉 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ∈ 𝑉 ) )
20		csbeq1a	⊢ ( 𝑦 = 𝐵 → ⦋ 𝐴 / 𝑥 ⦌ 𝐶 = ⦋ 𝐵 / 𝑦 ⦌ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 )
21	20	eleq1d	⊢ ( 𝑦 = 𝐵 → ( ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ∈ 𝑉 ↔ ⦋ 𝐵 / 𝑦 ⦌ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ∈ 𝑉 ) )
22	15 17 19 21	rspc2	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 𝐶 ∈ 𝑉 → ⦋ 𝐵 / 𝑦 ⦌ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ∈ 𝑉 ) )
23	22	imp	⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 𝐶 ∈ 𝑉 ) → ⦋ 𝐵 / 𝑦 ⦌ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ∈ 𝑉 )
24	4 5 2 23	syl21anc	⊢ ( 𝜑 → ⦋ 𝐵 / 𝑦 ⦌ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ∈ 𝑉 )
25	13 24	eqeltrid	⊢ ( 𝜑 → ⦋ 𝐵 / 𝑏 ⦌ ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 ∈ 𝑉 )
26		eqid	⊢ ( 𝑏 ∈ 𝑌 ↦ ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 ) = ( 𝑏 ∈ 𝑌 ↦ ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 )
27	26	fvmpts	⊢ ( ( 𝐵 ∈ 𝑌 ∧ ⦋ 𝐵 / 𝑏 ⦌ ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 ∈ 𝑉 ) → ( ( 𝑏 ∈ 𝑌 ↦ ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 ) ‘ 𝐵 ) = ⦋ 𝐵 / 𝑏 ⦌ ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 )
28	5 25 27	syl2anc	⊢ ( 𝜑 → ( ( 𝑏 ∈ 𝑌 ↦ ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 ) ‘ 𝐵 ) = ⦋ 𝐵 / 𝑏 ⦌ ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 )
29		nfcv	⊢ Ⅎ 𝑎 𝐶
30		nfcv	⊢ Ⅎ 𝑏 𝐶
31		nfcv	⊢ Ⅎ 𝑥 𝑏
32		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑎 / 𝑥 ⦌ 𝐶
33	31 32	nfcsbw	⊢ Ⅎ 𝑥 ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶
34		nfcsb1v	⊢ Ⅎ 𝑦 ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶
35		csbeq1a	⊢ ( 𝑥 = 𝑎 → 𝐶 = ⦋ 𝑎 / 𝑥 ⦌ 𝐶 )
36		csbeq1a	⊢ ( 𝑦 = 𝑏 → ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 )
37	35 36	sylan9eq	⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → 𝐶 = ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 )
38	29 30 33 34 37	cbvmpo	⊢ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐶 ) = ( 𝑎 ∈ 𝑋 , 𝑏 ∈ 𝑌 ↦ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 )
39	1 38	eqtri	⊢ 𝐹 = ( 𝑎 ∈ 𝑋 , 𝑏 ∈ 𝑌 ↦ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 )
40	32	nfel1	⊢ Ⅎ 𝑥 ⦋ 𝑎 / 𝑥 ⦌ 𝐶 ∈ 𝑉
41	34	nfel1	⊢ Ⅎ 𝑦 ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 ∈ 𝑉
42	35	eleq1d	⊢ ( 𝑥 = 𝑎 → ( 𝐶 ∈ 𝑉 ↔ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 ∈ 𝑉 ) )
43	36	eleq1d	⊢ ( 𝑦 = 𝑏 → ( ⦋ 𝑎 / 𝑥 ⦌ 𝐶 ∈ 𝑉 ↔ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 ∈ 𝑉 ) )
44	40 41 42 43	rspc2	⊢ ( ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌 ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 𝐶 ∈ 𝑉 → ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 ∈ 𝑉 ) )
45	2 44	mpan9	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑌 ) ) → ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 ∈ 𝑉 )
46	45	ralrimivva	⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝑋 ∀ 𝑏 ∈ 𝑌 ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 ∈ 𝑉 )
47	5	ne0d	⊢ ( 𝜑 → 𝑌 ≠ ∅ )
48	39 46 47 3 4	mpocurryvald	⊢ ( 𝜑 → ( curry 𝐹 ‘ 𝐴 ) = ( 𝑏 ∈ 𝑌 ↦ ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 ) )
49	48	fveq1d	⊢ ( 𝜑 → ( ( curry 𝐹 ‘ 𝐴 ) ‘ 𝐵 ) = ( ( 𝑏 ∈ 𝑌 ↦ ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 ) ‘ 𝐵 ) )
50	1	a1i	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐶 ) )
51		csbcow	⊢ ⦋ 𝑦 / 𝑏 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝑦 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶
52		csbid	⊢ ⦋ 𝑦 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝑎 / 𝑥 ⦌ 𝐶
53	51 52	eqtr2i	⊢ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝑦 / 𝑏 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶
54	53	a1i	⊢ ( 𝜑 → ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝑦 / 𝑏 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 )
55	54	csbeq2dv	⊢ ( 𝜑 → ⦋ 𝑥 / 𝑎 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝑥 / 𝑎 ⦌ ⦋ 𝑦 / 𝑏 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 )
56		csbcow	⊢ ⦋ 𝑥 / 𝑎 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝑥 / 𝑥 ⦌ 𝐶
57		csbid	⊢ ⦋ 𝑥 / 𝑥 ⦌ 𝐶 = 𝐶
58	56 57	eqtri	⊢ ⦋ 𝑥 / 𝑎 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = 𝐶
59		csbcom	⊢ ⦋ 𝑥 / 𝑎 ⦌ ⦋ 𝑦 / 𝑏 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝑦 / 𝑏 ⦌ ⦋ 𝑥 / 𝑎 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶
60	55 58 59	3eqtr3g	⊢ ( 𝜑 → 𝐶 = ⦋ 𝑦 / 𝑏 ⦌ ⦋ 𝑥 / 𝑎 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 )
61		csbeq1	⊢ ( 𝑥 = 𝐴 → ⦋ 𝑥 / 𝑎 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 )
62	61	adantr	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ⦋ 𝑥 / 𝑎 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 )
63	62	csbeq2dv	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ⦋ 𝑦 / 𝑏 ⦌ ⦋ 𝑥 / 𝑎 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝑦 / 𝑏 ⦌ ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 )
64		csbeq1	⊢ ( 𝑦 = 𝐵 → ⦋ 𝑦 / 𝑏 ⦌ ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝐵 / 𝑏 ⦌ ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 )
65	64	adantl	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ⦋ 𝑦 / 𝑏 ⦌ ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝐵 / 𝑏 ⦌ ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 )
66	63 65	eqtrd	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ⦋ 𝑦 / 𝑏 ⦌ ⦋ 𝑥 / 𝑎 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝐵 / 𝑏 ⦌ ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 )
67	60 66	sylan9eq	⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ) → 𝐶 = ⦋ 𝐵 / 𝑏 ⦌ ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 )
68		eqidd	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → 𝑌 = 𝑌 )
69		nfv	⊢ Ⅎ 𝑥 𝜑
70		nfv	⊢ Ⅎ 𝑦 𝜑
71		nfcv	⊢ Ⅎ 𝑦 𝐴
72		nfcv	⊢ Ⅎ 𝑥 𝐵
73		nfcv	⊢ Ⅎ 𝑥 𝐴
74	73 33	nfcsbw	⊢ Ⅎ 𝑥 ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶
75	72 74	nfcsbw	⊢ Ⅎ 𝑥 ⦋ 𝐵 / 𝑏 ⦌ ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶
76	13 16	nfcxfr	⊢ Ⅎ 𝑦 ⦋ 𝐵 / 𝑏 ⦌ ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶
77	50 67 68 4 5 25 69 70 71 72 75 76	ovmpodxf	⊢ ( 𝜑 → ( 𝐴 𝐹 𝐵 ) = ⦋ 𝐵 / 𝑏 ⦌ ⦋ 𝐴 / 𝑎 ⦌ ⦋ 𝑏 / 𝑦 ⦌ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 )
78	28 49 77	3eqtr4d	⊢ ( 𝜑 → ( ( curry 𝐹 ‘ 𝐴 ) ‘ 𝐵 ) = ( 𝐴 𝐹 𝐵 ) )