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