Metamath Proof Explorer


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 F = x X , y Y C
fvmpocurryd.c φ x X y Y C V
fvmpocurryd.y φ Y W
fvmpocurryd.a φ A X
fvmpocurryd.b φ B Y
Assertion fvmpocurryd φ curry F A B = A F B

Proof

Step Hyp Ref Expression
1 fvmpocurryd.f F = x X , y Y C
2 fvmpocurryd.c φ x X y Y C V
3 fvmpocurryd.y φ Y W
4 fvmpocurryd.a φ A X
5 fvmpocurryd.b φ B Y
6 csbcom B / b A / a b / y a / x C = A / a B / b b / y a / x C
7 csbcow B / b b / y a / x C = B / y a / x C
8 7 csbeq2i A / a B / b b / y a / x C = A / a B / y a / x C
9 csbcom A / a B / y a / x C = B / y A / a a / x C
10 csbcow A / a a / x C = A / x C
11 10 csbeq2i B / y A / a a / x C = B / y A / x C
12 9 11 eqtri A / a B / y a / x C = B / y A / x C
13 6 8 12 3eqtri B / b A / a b / y a / x C = B / y A / x C
14 nfcsb1v _ x A / x C
15 14 nfel1 x A / x C V
16 nfcsb1v _ y B / y A / x C
17 16 nfel1 y B / y A / x C V
18 csbeq1a x = A C = A / x C
19 18 eleq1d x = A C V A / x C V
20 csbeq1a y = B A / x C = B / y A / x C
21 20 eleq1d y = B A / x C V B / y A / x C V
22 15 17 19 21 rspc2 A X B Y x X y Y C V B / y A / x C V
23 22 imp A X B Y x X y Y C V B / y A / x C V
24 4 5 2 23 syl21anc φ B / y A / x C V
25 13 24 eqeltrid φ B / b A / a b / y a / x C V
26 eqid b Y A / a b / y a / x C = b Y A / a b / y a / x C
27 26 fvmpts B Y B / b A / a b / y a / x C V b Y A / a b / y a / x C B = B / b A / a b / y a / x C
28 5 25 27 syl2anc φ b Y A / a b / y a / x C B = B / b A / a b / y a / x C
29 nfcv _ a C
30 nfcv _ b C
31 nfcv _ x b
32 nfcsb1v _ x a / x C
33 31 32 nfcsbw _ x b / y a / x C
34 nfcsb1v _ y b / y a / x C
35 csbeq1a x = a C = a / x C
36 csbeq1a y = b a / x C = b / y a / x C
37 35 36 sylan9eq x = a y = b C = b / y a / x C
38 29 30 33 34 37 cbvmpo x X , y Y C = a X , b Y b / y a / x C
39 1 38 eqtri F = a X , b Y b / y a / x C
40 32 nfel1 x a / x C V
41 34 nfel1 y b / y a / x C V
42 35 eleq1d x = a C V a / x C V
43 36 eleq1d y = b a / x C V b / y a / x C V
44 40 41 42 43 rspc2 a X b Y x X y Y C V b / y a / x C V
45 2 44 mpan9 φ a X b Y b / y a / x C V
46 45 ralrimivva φ a X b Y b / y a / x C V
47 5 ne0d φ Y
48 39 46 47 3 4 mpocurryvald φ curry F A = b Y A / a b / y a / x C
49 48 fveq1d φ curry F A B = b Y A / a b / y a / x C B
50 1 a1i φ F = x X , y Y C
51 csbcow y / b b / y a / x C = y / y a / x C
52 csbid y / y a / x C = a / x C
53 51 52 eqtr2i a / x C = y / b b / y a / x C
54 53 a1i φ a / x C = y / b b / y a / x C
55 54 csbeq2dv φ x / a a / x C = x / a y / b b / y a / x C
56 csbcow x / a a / x C = x / x C
57 csbid x / x C = C
58 56 57 eqtri x / a a / x C = C
59 csbcom x / a y / b b / y a / x C = y / b x / a b / y a / x C
60 55 58 59 3eqtr3g φ C = y / b x / a b / y a / x C
61 csbeq1 x = A x / a b / y a / x C = A / a b / y a / x C
62 61 adantr x = A y = B x / a b / y a / x C = A / a b / y a / x C
63 62 csbeq2dv x = A y = B y / b x / a b / y a / x C = y / b A / a b / y a / x C
64 csbeq1 y = B y / b A / a b / y a / x C = B / b A / a b / y a / x C
65 64 adantl x = A y = B y / b A / a b / y a / x C = B / b A / a b / y a / x C
66 63 65 eqtrd x = A y = B y / b x / a b / y a / x C = B / b A / a b / y a / x C
67 60 66 sylan9eq φ x = A y = B C = B / b A / a b / y a / x C
68 eqidd φ x = A Y = Y
69 nfv x φ
70 nfv y φ
71 nfcv _ y A
72 nfcv _ x B
73 nfcv _ x A
74 73 33 nfcsbw _ x A / a b / y a / x C
75 72 74 nfcsbw _ x B / b A / a b / y a / x C
76 13 16 nfcxfr _ y B / b A / a b / y a / x C
77 50 67 68 4 5 25 69 70 71 72 75 76 ovmpodxf φ A F B = B / b A / a b / y a / x C
78 28 49 77 3eqtr4d φ curry F A B = A F B