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	⊢ 𝐹 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐶 )
	mpocurryd.c	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 𝐶 ∈ 𝑉 )
	mpocurryd.n	⊢ ( 𝜑 → 𝑌 ≠ ∅ )
	mpocurryvald.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑊 )
	mpocurryvald.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
Assertion	mpocurryvald	⊢ ( 𝜑 → ( curry 𝐹 ‘ 𝐴 ) = ( 𝑦 ∈ 𝑌 ↦ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		mpocurryd.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝐶 )
2		mpocurryd.c	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 𝐶 ∈ 𝑉 )
3		mpocurryd.n	⊢ ( 𝜑 → 𝑌 ≠ ∅ )
4		mpocurryvald.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑊 )
5		mpocurryvald.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
6	1 2 3	mpocurryd	⊢ ( 𝜑 → curry 𝐹 = ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐶 ) ) )
7		nfcv	⊢ Ⅎ 𝑎 ( 𝑦 ∈ 𝑌 ↦ 𝐶 )
8		nfcv	⊢ Ⅎ 𝑥 𝑌
9		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑎 / 𝑥 ⦌ 𝐶
10	8 9	nfmpt	⊢ Ⅎ 𝑥 ( 𝑦 ∈ 𝑌 ↦ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 )
11		csbeq1a	⊢ ( 𝑥 = 𝑎 → 𝐶 = ⦋ 𝑎 / 𝑥 ⦌ 𝐶 )
12	11	mpteq2dv	⊢ ( 𝑥 = 𝑎 → ( 𝑦 ∈ 𝑌 ↦ 𝐶 ) = ( 𝑦 ∈ 𝑌 ↦ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 ) )
13	7 10 12	cbvmpt	⊢ ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ 𝐶 ) ) = ( 𝑎 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 ) )
14	6 13	eqtrdi	⊢ ( 𝜑 → curry 𝐹 = ( 𝑎 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 ) ) )
15		csbeq1	⊢ ( 𝑎 = 𝐴 → ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝐴 / 𝑥 ⦌ 𝐶 )
16	15	adantl	⊢ ( ( 𝜑 ∧ 𝑎 = 𝐴 ) → ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝐴 / 𝑥 ⦌ 𝐶 )
17	16	mpteq2dv	⊢ ( ( 𝜑 ∧ 𝑎 = 𝐴 ) → ( 𝑦 ∈ 𝑌 ↦ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 ) = ( 𝑦 ∈ 𝑌 ↦ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) )
18	4	mptexd	⊢ ( 𝜑 → ( 𝑦 ∈ 𝑌 ↦ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ∈ V )
19	14 17 5 18	fvmptd	⊢ ( 𝜑 → ( curry 𝐹 ‘ 𝐴 ) = ( 𝑦 ∈ 𝑌 ↦ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) )