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 ⊢ F = x ∈ X , y ∈ Y ⟼ C
mpocurryd.c ⊢ φ → ∀ x ∈ X ∀ y ∈ Y C ∈ V
mpocurryd.n ⊢ φ → Y ≠ ∅
mpocurryvald.y ⊢ φ → Y ∈ W
mpocurryvald.a ⊢ φ → A ∈ X
Assertion mpocurryvald ⊢ φ → curry F ⁡ A = y ∈ Y ⟼ ⦋ A / x⦌ C

Proof

Step Hyp Ref Expression
1 mpocurryd.f ⊢ F = x ∈ X , y ∈ Y ⟼ C
2 mpocurryd.c ⊢ φ → ∀ x ∈ X ∀ y ∈ Y C ∈ V
3 mpocurryd.n ⊢ φ → Y ≠ ∅
4 mpocurryvald.y ⊢ φ → Y ∈ W
5 mpocurryvald.a ⊢ φ → A ∈ X
6 1 2 3 mpocurryd ⊢ φ → curry F = x ∈ X ⟼ y ∈ Y ⟼ C
7 nfcv ⊢ Ⅎ _ a y ∈ Y ⟼ C
8 nfcv ⊢ Ⅎ _ x Y
9 nfcsb1v ⊢ Ⅎ _ x ⦋ a / x⦌ C
10 8 9 nfmpt ⊢ Ⅎ _ x y ∈ Y ⟼ ⦋ a / x⦌ C
11 csbeq1a ⊢ x = a → C = ⦋ a / x⦌ C
12 11 mpteq2dv ⊢ x = a → y ∈ Y ⟼ C = y ∈ Y ⟼ ⦋ a / x⦌ C
13 7 10 12 cbvmpt ⊢ x ∈ X ⟼ y ∈ Y ⟼ C = a ∈ X ⟼ y ∈ Y ⟼ ⦋ a / x⦌ C
14 6 13 eqtrdi ⊢ φ → curry F = a ∈ X ⟼ y ∈ Y ⟼ ⦋ a / x⦌ C
15 csbeq1 ⊢ a = A → ⦋ a / x⦌ C = ⦋ A / x⦌ C
16 15 adantl ⊢ φ ∧ a = A → ⦋ a / x⦌ C = ⦋ A / x⦌ C
17 16 mpteq2dv ⊢ φ ∧ a = A → y ∈ Y ⟼ ⦋ a / x⦌ C = y ∈ Y ⟼ ⦋ A / x⦌ C
18 4 mptexd ⊢ φ → y ∈ Y ⟼ ⦋ A / x⦌ C ∈ V
19 14 17 5 18 fvmptd ⊢ φ → curry F ⁡ A = y ∈ Y ⟼ ⦋ A / x⦌ C