This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐹 ‘ 𝐴 ) = ( 𝑦 ∈ 𝑌 ↦ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) )