MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fvmpt2curryd Structured version   Visualization version   GIF version

Theorem fvmpt2curryd 7261
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.)
Hypotheses
Ref Expression
fvmpt2curryd.f 𝐹 = (𝑥𝑋, 𝑦𝑌𝐶)
fvmpt2curryd.c (𝜑 → ∀𝑥𝑋𝑦𝑌 𝐶𝑉)
fvmpt2curryd.y (𝜑𝑌𝑊)
fvmpt2curryd.a (𝜑𝐴𝑋)
fvmpt2curryd.b (𝜑𝐵𝑌)
Assertion
Ref Expression
fvmpt2curryd (𝜑 → ((curry 𝐹𝐴)‘𝐵) = (𝐴𝐹𝐵))
Distinct variable groups:   𝑥,𝐴,𝑦   𝑥,𝐵,𝑦   𝑥,𝑉,𝑦   𝑥,𝑋,𝑦   𝑥,𝑌,𝑦   𝜑,𝑥,𝑦
Allowed substitution hints:   𝐶(𝑥,𝑦)   𝐹(𝑥,𝑦)   𝑊(𝑥,𝑦)

Proof of Theorem fvmpt2curryd
Dummy variables 𝑎 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fvmpt2curryd.b . . 3 (𝜑𝐵𝑌)
2 csbcom 3945 . . . . 5 𝐵 / 𝑏𝐴 / 𝑎𝑏 / 𝑦𝑎 / 𝑥𝐶 = 𝐴 / 𝑎𝐵 / 𝑏𝑏 / 𝑦𝑎 / 𝑥𝐶
3 csbco 3508 . . . . . 6 𝐵 / 𝑏𝑏 / 𝑦𝑎 / 𝑥𝐶 = 𝐵 / 𝑦𝑎 / 𝑥𝐶
43csbeq2i 3944 . . . . 5 𝐴 / 𝑎𝐵 / 𝑏𝑏 / 𝑦𝑎 / 𝑥𝐶 = 𝐴 / 𝑎𝐵 / 𝑦𝑎 / 𝑥𝐶
5 csbcom 3945 . . . . . 6 𝐴 / 𝑎𝐵 / 𝑦𝑎 / 𝑥𝐶 = 𝐵 / 𝑦𝐴 / 𝑎𝑎 / 𝑥𝐶
6 csbco 3508 . . . . . . 7 𝐴 / 𝑎𝑎 / 𝑥𝐶 = 𝐴 / 𝑥𝐶
76csbeq2i 3944 . . . . . 6 𝐵 / 𝑦𝐴 / 𝑎𝑎 / 𝑥𝐶 = 𝐵 / 𝑦𝐴 / 𝑥𝐶
85, 7eqtri 2631 . . . . 5 𝐴 / 𝑎𝐵 / 𝑦𝑎 / 𝑥𝐶 = 𝐵 / 𝑦𝐴 / 𝑥𝐶
92, 4, 83eqtri 2635 . . . 4 𝐵 / 𝑏𝐴 / 𝑎𝑏 / 𝑦𝑎 / 𝑥𝐶 = 𝐵 / 𝑦𝐴 / 𝑥𝐶
10 fvmpt2curryd.a . . . . 5 (𝜑𝐴𝑋)
11 fvmpt2curryd.c . . . . 5 (𝜑 → ∀𝑥𝑋𝑦𝑌 𝐶𝑉)
12 nfcsb1v 3514 . . . . . . . 8 𝑥𝐴 / 𝑥𝐶
1312nfel1 2764 . . . . . . 7 𝑥𝐴 / 𝑥𝐶𝑉
14 nfcsb1v 3514 . . . . . . . 8 𝑦𝐵 / 𝑦𝐴 / 𝑥𝐶
1514nfel1 2764 . . . . . . 7 𝑦𝐵 / 𝑦𝐴 / 𝑥𝐶𝑉
16 csbeq1a 3507 . . . . . . . 8 (𝑥 = 𝐴𝐶 = 𝐴 / 𝑥𝐶)
1716eleq1d 2671 . . . . . . 7 (𝑥 = 𝐴 → (𝐶𝑉𝐴 / 𝑥𝐶𝑉))
18 csbeq1a 3507 . . . . . . . 8 (𝑦 = 𝐵𝐴 / 𝑥𝐶 = 𝐵 / 𝑦𝐴 / 𝑥𝐶)
1918eleq1d 2671 . . . . . . 7 (𝑦 = 𝐵 → (𝐴 / 𝑥𝐶𝑉𝐵 / 𝑦𝐴 / 𝑥𝐶𝑉))
2013, 15, 17, 19rspc2 3291 . . . . . 6 ((𝐴𝑋𝐵𝑌) → (∀𝑥𝑋𝑦𝑌 𝐶𝑉𝐵 / 𝑦𝐴 / 𝑥𝐶𝑉))
2120imp 443 . . . . 5 (((𝐴𝑋𝐵𝑌) ∧ ∀𝑥𝑋𝑦𝑌 𝐶𝑉) → 𝐵 / 𝑦𝐴 / 𝑥𝐶𝑉)
2210, 1, 11, 21syl21anc 1316 . . . 4 (𝜑𝐵 / 𝑦𝐴 / 𝑥𝐶𝑉)
239, 22syl5eqel 2691 . . 3 (𝜑𝐵 / 𝑏𝐴 / 𝑎𝑏 / 𝑦𝑎 / 𝑥𝐶𝑉)
24 eqid 2609 . . . 4 (𝑏𝑌𝐴 / 𝑎𝑏 / 𝑦𝑎 / 𝑥𝐶) = (𝑏𝑌𝐴 / 𝑎𝑏 / 𝑦𝑎 / 𝑥𝐶)
2524fvmpts 6179 . . 3 ((𝐵𝑌𝐵 / 𝑏𝐴 / 𝑎𝑏 / 𝑦𝑎 / 𝑥𝐶𝑉) → ((𝑏𝑌𝐴 / 𝑎𝑏 / 𝑦𝑎 / 𝑥𝐶)‘𝐵) = 𝐵 / 𝑏𝐴 / 𝑎𝑏 / 𝑦𝑎 / 𝑥𝐶)
261, 23, 25syl2anc 690 . 2 (𝜑 → ((𝑏𝑌𝐴 / 𝑎𝑏 / 𝑦𝑎 / 𝑥𝐶)‘𝐵) = 𝐵 / 𝑏𝐴 / 𝑎𝑏 / 𝑦𝑎 / 𝑥𝐶)
27 fvmpt2curryd.f . . . . 5 𝐹 = (𝑥𝑋, 𝑦𝑌𝐶)
28 nfcv 2750 . . . . . 6 𝑎𝐶
29 nfcv 2750 . . . . . 6 𝑏𝐶
30 nfcv 2750 . . . . . . 7 𝑥𝑏
31 nfcsb1v 3514 . . . . . . 7 𝑥𝑎 / 𝑥𝐶
3230, 31nfcsb 3516 . . . . . 6 𝑥𝑏 / 𝑦𝑎 / 𝑥𝐶
33 nfcsb1v 3514 . . . . . 6 𝑦𝑏 / 𝑦𝑎 / 𝑥𝐶
34 csbeq1a 3507 . . . . . . 7 (𝑥 = 𝑎𝐶 = 𝑎 / 𝑥𝐶)
35 csbeq1a 3507 . . . . . . 7 (𝑦 = 𝑏𝑎 / 𝑥𝐶 = 𝑏 / 𝑦𝑎 / 𝑥𝐶)
3634, 35sylan9eq 2663 . . . . . 6 ((𝑥 = 𝑎𝑦 = 𝑏) → 𝐶 = 𝑏 / 𝑦𝑎 / 𝑥𝐶)
3728, 29, 32, 33, 36cbvmpt2 6610 . . . . 5 (𝑥𝑋, 𝑦𝑌𝐶) = (𝑎𝑋, 𝑏𝑌𝑏 / 𝑦𝑎 / 𝑥𝐶)
3827, 37eqtri 2631 . . . 4 𝐹 = (𝑎𝑋, 𝑏𝑌𝑏 / 𝑦𝑎 / 𝑥𝐶)
3931nfel1 2764 . . . . . . 7 𝑥𝑎 / 𝑥𝐶𝑉
4033nfel1 2764 . . . . . . 7 𝑦𝑏 / 𝑦𝑎 / 𝑥𝐶𝑉
4134eleq1d 2671 . . . . . . 7 (𝑥 = 𝑎 → (𝐶𝑉𝑎 / 𝑥𝐶𝑉))
4235eleq1d 2671 . . . . . . 7 (𝑦 = 𝑏 → (𝑎 / 𝑥𝐶𝑉𝑏 / 𝑦𝑎 / 𝑥𝐶𝑉))
4339, 40, 41, 42rspc2 3291 . . . . . 6 ((𝑎𝑋𝑏𝑌) → (∀𝑥𝑋𝑦𝑌 𝐶𝑉𝑏 / 𝑦𝑎 / 𝑥𝐶𝑉))
4411, 43mpan9 484 . . . . 5 ((𝜑 ∧ (𝑎𝑋𝑏𝑌)) → 𝑏 / 𝑦𝑎 / 𝑥𝐶𝑉)
4544ralrimivva 2953 . . . 4 (𝜑 → ∀𝑎𝑋𝑏𝑌 𝑏 / 𝑦𝑎 / 𝑥𝐶𝑉)
46 ne0i 3879 . . . . 5 (𝐵𝑌𝑌 ≠ ∅)
471, 46syl 17 . . . 4 (𝜑𝑌 ≠ ∅)
48 fvmpt2curryd.y . . . 4 (𝜑𝑌𝑊)
4938, 45, 47, 48, 10mpt2curryvald 7260 . . 3 (𝜑 → (curry 𝐹𝐴) = (𝑏𝑌𝐴 / 𝑎𝑏 / 𝑦𝑎 / 𝑥𝐶))
5049fveq1d 6090 . 2 (𝜑 → ((curry 𝐹𝐴)‘𝐵) = ((𝑏𝑌𝐴 / 𝑎𝑏 / 𝑦𝑎 / 𝑥𝐶)‘𝐵))
5127a1i 11 . . 3 (𝜑𝐹 = (𝑥𝑋, 𝑦𝑌𝐶))
52 csbco 3508 . . . . . . . 8 𝑦 / 𝑏𝑏 / 𝑦𝑎 / 𝑥𝐶 = 𝑦 / 𝑦𝑎 / 𝑥𝐶
53 csbid 3506 . . . . . . . 8 𝑦 / 𝑦𝑎 / 𝑥𝐶 = 𝑎 / 𝑥𝐶
5452, 53eqtr2i 2632 . . . . . . 7 𝑎 / 𝑥𝐶 = 𝑦 / 𝑏𝑏 / 𝑦𝑎 / 𝑥𝐶
5554a1i 11 . . . . . 6 (𝜑𝑎 / 𝑥𝐶 = 𝑦 / 𝑏𝑏 / 𝑦𝑎 / 𝑥𝐶)
5655csbeq2dv 3943 . . . . 5 (𝜑𝑥 / 𝑎𝑎 / 𝑥𝐶 = 𝑥 / 𝑎𝑦 / 𝑏𝑏 / 𝑦𝑎 / 𝑥𝐶)
57 csbco 3508 . . . . . 6 𝑥 / 𝑎𝑎 / 𝑥𝐶 = 𝑥 / 𝑥𝐶
58 csbid 3506 . . . . . 6 𝑥 / 𝑥𝐶 = 𝐶
5957, 58eqtri 2631 . . . . 5 𝑥 / 𝑎𝑎 / 𝑥𝐶 = 𝐶
60 csbcom 3945 . . . . 5 𝑥 / 𝑎𝑦 / 𝑏𝑏 / 𝑦𝑎 / 𝑥𝐶 = 𝑦 / 𝑏𝑥 / 𝑎𝑏 / 𝑦𝑎 / 𝑥𝐶
6156, 59, 603eqtr3g 2666 . . . 4 (𝜑𝐶 = 𝑦 / 𝑏𝑥 / 𝑎𝑏 / 𝑦𝑎 / 𝑥𝐶)
62 csbeq1 3501 . . . . . . 7 (𝑥 = 𝐴𝑥 / 𝑎𝑏 / 𝑦𝑎 / 𝑥𝐶 = 𝐴 / 𝑎𝑏 / 𝑦𝑎 / 𝑥𝐶)
6362adantr 479 . . . . . 6 ((𝑥 = 𝐴𝑦 = 𝐵) → 𝑥 / 𝑎𝑏 / 𝑦𝑎 / 𝑥𝐶 = 𝐴 / 𝑎𝑏 / 𝑦𝑎 / 𝑥𝐶)
6463csbeq2dv 3943 . . . . 5 ((𝑥 = 𝐴𝑦 = 𝐵) → 𝑦 / 𝑏𝑥 / 𝑎𝑏 / 𝑦𝑎 / 𝑥𝐶 = 𝑦 / 𝑏𝐴 / 𝑎𝑏 / 𝑦𝑎 / 𝑥𝐶)
65 csbeq1 3501 . . . . . 6 (𝑦 = 𝐵𝑦 / 𝑏𝐴 / 𝑎𝑏 / 𝑦𝑎 / 𝑥𝐶 = 𝐵 / 𝑏𝐴 / 𝑎𝑏 / 𝑦𝑎 / 𝑥𝐶)
6665adantl 480 . . . . 5 ((𝑥 = 𝐴𝑦 = 𝐵) → 𝑦 / 𝑏𝐴 / 𝑎𝑏 / 𝑦𝑎 / 𝑥𝐶 = 𝐵 / 𝑏𝐴 / 𝑎𝑏 / 𝑦𝑎 / 𝑥𝐶)
6764, 66eqtrd 2643 . . . 4 ((𝑥 = 𝐴𝑦 = 𝐵) → 𝑦 / 𝑏𝑥 / 𝑎𝑏 / 𝑦𝑎 / 𝑥𝐶 = 𝐵 / 𝑏𝐴 / 𝑎𝑏 / 𝑦𝑎 / 𝑥𝐶)
6861, 67sylan9eq 2663 . . 3 ((𝜑 ∧ (𝑥 = 𝐴𝑦 = 𝐵)) → 𝐶 = 𝐵 / 𝑏𝐴 / 𝑎𝑏 / 𝑦𝑎 / 𝑥𝐶)
69 eqidd 2610 . . 3 ((𝜑𝑥 = 𝐴) → 𝑌 = 𝑌)
70 nfv 1829 . . 3 𝑥𝜑
71 nfv 1829 . . 3 𝑦𝜑
72 nfcv 2750 . . 3 𝑦𝐴
73 nfcv 2750 . . 3 𝑥𝐵
74 nfcv 2750 . . . . 5 𝑥𝐴
7574, 32nfcsb 3516 . . . 4 𝑥𝐴 / 𝑎𝑏 / 𝑦𝑎 / 𝑥𝐶
7673, 75nfcsb 3516 . . 3 𝑥𝐵 / 𝑏𝐴 / 𝑎𝑏 / 𝑦𝑎 / 𝑥𝐶
779, 14nfcxfr 2748 . . 3 𝑦𝐵 / 𝑏𝐴 / 𝑎𝑏 / 𝑦𝑎 / 𝑥𝐶
7851, 68, 69, 10, 1, 23, 70, 71, 72, 73, 76, 77ovmpt2dxf 6662 . 2 (𝜑 → (𝐴𝐹𝐵) = 𝐵 / 𝑏𝐴 / 𝑎𝑏 / 𝑦𝑎 / 𝑥𝐶)
7926, 50, 783eqtr4d 2653 1 (𝜑 → ((curry 𝐹𝐴)‘𝐵) = (𝐴𝐹𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = wceq 1474  wcel 1976  wne 2779  wral 2895  csb 3498  c0 3873  cmpt 4637  cfv 5790  (class class class)co 6527  cmpt2 6529  curry ccur 7255
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6824
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-fal 1480  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-ral 2900  df-rex 2901  df-reu 2902  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-id 4943  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-1st 7036  df-2nd 7037  df-cur 7257
This theorem is referenced by:  pmatcollpw3lem  20349  logbfval  24245
  Copyright terms: Public domain W3C validator