Users' Mathboxes Mathbox for Brendan Leahy < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  unccur Structured version   Visualization version   GIF version

Theorem unccur 36090
Description: Uncurrying of currying. (Contributed by Brendan Leahy, 5-Jun-2021.)
Assertion
Ref Expression
unccur ((𝐹:(𝐴 × 𝐵)⟶𝐶𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶𝑊) → uncurry curry 𝐹 = 𝐹)

Proof of Theorem unccur
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ffn 6673 . . . . . . . . 9 (𝐹:(𝐴 × 𝐵)⟶𝐶𝐹 Fn (𝐴 × 𝐵))
21anim1i 616 . . . . . . . 8 ((𝐹:(𝐴 × 𝐵)⟶𝐶𝐵 ∈ (𝑉 ∖ {∅})) → (𝐹 Fn (𝐴 × 𝐵) ∧ 𝐵 ∈ (𝑉 ∖ {∅})))
323adant3 1133 . . . . . . 7 ((𝐹:(𝐴 × 𝐵)⟶𝐶𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶𝑊) → (𝐹 Fn (𝐴 × 𝐵) ∧ 𝐵 ∈ (𝑉 ∖ {∅})))
4 3anass 1096 . . . . . . . . . . 11 ((𝐹 Fn (𝐴 × 𝐵) ∧ 𝑥𝐴𝑦𝐵) ↔ (𝐹 Fn (𝐴 × 𝐵) ∧ (𝑥𝐴𝑦𝐵)))
5 curfv 36087 . . . . . . . . . . 11 (((𝐹 Fn (𝐴 × 𝐵) ∧ 𝑥𝐴𝑦𝐵) ∧ 𝐵 ∈ (𝑉 ∖ {∅})) → ((curry 𝐹𝑥)‘𝑦) = (𝑥𝐹𝑦))
64, 5sylanbr 583 . . . . . . . . . 10 (((𝐹 Fn (𝐴 × 𝐵) ∧ (𝑥𝐴𝑦𝐵)) ∧ 𝐵 ∈ (𝑉 ∖ {∅})) → ((curry 𝐹𝑥)‘𝑦) = (𝑥𝐹𝑦))
76an32s 651 . . . . . . . . 9 (((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐵 ∈ (𝑉 ∖ {∅})) ∧ (𝑥𝐴𝑦𝐵)) → ((curry 𝐹𝑥)‘𝑦) = (𝑥𝐹𝑦))
87eqeq1d 2739 . . . . . . . 8 (((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐵 ∈ (𝑉 ∖ {∅})) ∧ (𝑥𝐴𝑦𝐵)) → (((curry 𝐹𝑥)‘𝑦) = 𝑧 ↔ (𝑥𝐹𝑦) = 𝑧))
9 eqcom 2744 . . . . . . . 8 ((𝑥𝐹𝑦) = 𝑧𝑧 = (𝑥𝐹𝑦))
108, 9bitrdi 287 . . . . . . 7 (((𝐹 Fn (𝐴 × 𝐵) ∧ 𝐵 ∈ (𝑉 ∖ {∅})) ∧ (𝑥𝐴𝑦𝐵)) → (((curry 𝐹𝑥)‘𝑦) = 𝑧𝑧 = (𝑥𝐹𝑦)))
113, 10sylan 581 . . . . . 6 (((𝐹:(𝐴 × 𝐵)⟶𝐶𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶𝑊) ∧ (𝑥𝐴𝑦𝐵)) → (((curry 𝐹𝑥)‘𝑦) = 𝑧𝑧 = (𝑥𝐹𝑦)))
12 curf 36085 . . . . . . . . . 10 ((𝐹:(𝐴 × 𝐵)⟶𝐶𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶𝑊) → curry 𝐹:𝐴⟶(𝐶m 𝐵))
1312ffvelcdmda 7040 . . . . . . . . 9 (((𝐹:(𝐴 × 𝐵)⟶𝐶𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶𝑊) ∧ 𝑥𝐴) → (curry 𝐹𝑥) ∈ (𝐶m 𝐵))
14 elmapfn 8810 . . . . . . . . 9 ((curry 𝐹𝑥) ∈ (𝐶m 𝐵) → (curry 𝐹𝑥) Fn 𝐵)
1513, 14syl 17 . . . . . . . 8 (((𝐹:(𝐴 × 𝐵)⟶𝐶𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶𝑊) ∧ 𝑥𝐴) → (curry 𝐹𝑥) Fn 𝐵)
16 fnbrfvb 6900 . . . . . . . 8 (((curry 𝐹𝑥) Fn 𝐵𝑦𝐵) → (((curry 𝐹𝑥)‘𝑦) = 𝑧𝑦(curry 𝐹𝑥)𝑧))
1715, 16sylan 581 . . . . . . 7 ((((𝐹:(𝐴 × 𝐵)⟶𝐶𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶𝑊) ∧ 𝑥𝐴) ∧ 𝑦𝐵) → (((curry 𝐹𝑥)‘𝑦) = 𝑧𝑦(curry 𝐹𝑥)𝑧))
1817anasss 468 . . . . . 6 (((𝐹:(𝐴 × 𝐵)⟶𝐶𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶𝑊) ∧ (𝑥𝐴𝑦𝐵)) → (((curry 𝐹𝑥)‘𝑦) = 𝑧𝑦(curry 𝐹𝑥)𝑧))
19 ibar 530 . . . . . . 7 ((𝑥𝐴𝑦𝐵) → (𝑧 = (𝑥𝐹𝑦) ↔ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = (𝑥𝐹𝑦))))
2019adantl 483 . . . . . 6 (((𝐹:(𝐴 × 𝐵)⟶𝐶𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶𝑊) ∧ (𝑥𝐴𝑦𝐵)) → (𝑧 = (𝑥𝐹𝑦) ↔ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = (𝑥𝐹𝑦))))
2111, 18, 203bitr3d 309 . . . . 5 (((𝐹:(𝐴 × 𝐵)⟶𝐶𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶𝑊) ∧ (𝑥𝐴𝑦𝐵)) → (𝑦(curry 𝐹𝑥)𝑧 ↔ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = (𝑥𝐹𝑦))))
22 df-br 5111 . . . . . . . . . . 11 (𝑦(curry 𝐹𝑥)𝑧 ↔ ⟨𝑦, 𝑧⟩ ∈ (curry 𝐹𝑥))
23 elfvdm 6884 . . . . . . . . . . 11 (⟨𝑦, 𝑧⟩ ∈ (curry 𝐹𝑥) → 𝑥 ∈ dom curry 𝐹)
2422, 23sylbi 216 . . . . . . . . . 10 (𝑦(curry 𝐹𝑥)𝑧𝑥 ∈ dom curry 𝐹)
25 fdm 6682 . . . . . . . . . . . 12 (curry 𝐹:𝐴⟶(𝐶m 𝐵) → dom curry 𝐹 = 𝐴)
2625eleq2d 2824 . . . . . . . . . . 11 (curry 𝐹:𝐴⟶(𝐶m 𝐵) → (𝑥 ∈ dom curry 𝐹𝑥𝐴))
2726biimpa 478 . . . . . . . . . 10 ((curry 𝐹:𝐴⟶(𝐶m 𝐵) ∧ 𝑥 ∈ dom curry 𝐹) → 𝑥𝐴)
2824, 27sylan2 594 . . . . . . . . 9 ((curry 𝐹:𝐴⟶(𝐶m 𝐵) ∧ 𝑦(curry 𝐹𝑥)𝑧) → 𝑥𝐴)
29 ffvelcdm 7037 . . . . . . . . . . . . 13 ((curry 𝐹:𝐴⟶(𝐶m 𝐵) ∧ 𝑥𝐴) → (curry 𝐹𝑥) ∈ (𝐶m 𝐵))
30 elmapi 8794 . . . . . . . . . . . . 13 ((curry 𝐹𝑥) ∈ (𝐶m 𝐵) → (curry 𝐹𝑥):𝐵𝐶)
31 fdm 6682 . . . . . . . . . . . . 13 ((curry 𝐹𝑥):𝐵𝐶 → dom (curry 𝐹𝑥) = 𝐵)
3229, 30, 313syl 18 . . . . . . . . . . . 12 ((curry 𝐹:𝐴⟶(𝐶m 𝐵) ∧ 𝑥𝐴) → dom (curry 𝐹𝑥) = 𝐵)
33 vex 3452 . . . . . . . . . . . . 13 𝑦 ∈ V
34 vex 3452 . . . . . . . . . . . . 13 𝑧 ∈ V
3533, 34breldm 5869 . . . . . . . . . . . 12 (𝑦(curry 𝐹𝑥)𝑧𝑦 ∈ dom (curry 𝐹𝑥))
36 eleq2 2827 . . . . . . . . . . . . 13 (dom (curry 𝐹𝑥) = 𝐵 → (𝑦 ∈ dom (curry 𝐹𝑥) ↔ 𝑦𝐵))
3736biimpa 478 . . . . . . . . . . . 12 ((dom (curry 𝐹𝑥) = 𝐵𝑦 ∈ dom (curry 𝐹𝑥)) → 𝑦𝐵)
3832, 35, 37syl2an 597 . . . . . . . . . . 11 (((curry 𝐹:𝐴⟶(𝐶m 𝐵) ∧ 𝑥𝐴) ∧ 𝑦(curry 𝐹𝑥)𝑧) → 𝑦𝐵)
3938an32s 651 . . . . . . . . . 10 (((curry 𝐹:𝐴⟶(𝐶m 𝐵) ∧ 𝑦(curry 𝐹𝑥)𝑧) ∧ 𝑥𝐴) → 𝑦𝐵)
4028, 39mpdan 686 . . . . . . . . 9 ((curry 𝐹:𝐴⟶(𝐶m 𝐵) ∧ 𝑦(curry 𝐹𝑥)𝑧) → 𝑦𝐵)
4128, 40jca 513 . . . . . . . 8 ((curry 𝐹:𝐴⟶(𝐶m 𝐵) ∧ 𝑦(curry 𝐹𝑥)𝑧) → (𝑥𝐴𝑦𝐵))
4212, 41sylan 581 . . . . . . 7 (((𝐹:(𝐴 × 𝐵)⟶𝐶𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶𝑊) ∧ 𝑦(curry 𝐹𝑥)𝑧) → (𝑥𝐴𝑦𝐵))
4342stoic1a 1775 . . . . . 6 (((𝐹:(𝐴 × 𝐵)⟶𝐶𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶𝑊) ∧ ¬ (𝑥𝐴𝑦𝐵)) → ¬ 𝑦(curry 𝐹𝑥)𝑧)
44 simpl 484 . . . . . . . 8 (((𝑥𝐴𝑦𝐵) ∧ 𝑧 = (𝑥𝐹𝑦)) → (𝑥𝐴𝑦𝐵))
4544con3i 154 . . . . . . 7 (¬ (𝑥𝐴𝑦𝐵) → ¬ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = (𝑥𝐹𝑦)))
4645adantl 483 . . . . . 6 (((𝐹:(𝐴 × 𝐵)⟶𝐶𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶𝑊) ∧ ¬ (𝑥𝐴𝑦𝐵)) → ¬ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = (𝑥𝐹𝑦)))
4743, 462falsed 377 . . . . 5 (((𝐹:(𝐴 × 𝐵)⟶𝐶𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶𝑊) ∧ ¬ (𝑥𝐴𝑦𝐵)) → (𝑦(curry 𝐹𝑥)𝑧 ↔ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = (𝑥𝐹𝑦))))
4821, 47pm2.61dan 812 . . . 4 ((𝐹:(𝐴 × 𝐵)⟶𝐶𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶𝑊) → (𝑦(curry 𝐹𝑥)𝑧 ↔ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = (𝑥𝐹𝑦))))
4948oprabbidv 7428 . . 3 ((𝐹:(𝐴 × 𝐵)⟶𝐶𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶𝑊) → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝑦(curry 𝐹𝑥)𝑧} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = (𝑥𝐹𝑦))})
50 df-unc 8204 . . 3 uncurry curry 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝑦(curry 𝐹𝑥)𝑧}
51 df-mpo 7367 . . 3 (𝑥𝐴, 𝑦𝐵 ↦ (𝑥𝐹𝑦)) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = (𝑥𝐹𝑦))}
5249, 50, 513eqtr4g 2802 . 2 ((𝐹:(𝐴 × 𝐵)⟶𝐶𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶𝑊) → uncurry curry 𝐹 = (𝑥𝐴, 𝑦𝐵 ↦ (𝑥𝐹𝑦)))
53 fnov 7492 . . . 4 (𝐹 Fn (𝐴 × 𝐵) ↔ 𝐹 = (𝑥𝐴, 𝑦𝐵 ↦ (𝑥𝐹𝑦)))
541, 53sylib 217 . . 3 (𝐹:(𝐴 × 𝐵)⟶𝐶𝐹 = (𝑥𝐴, 𝑦𝐵 ↦ (𝑥𝐹𝑦)))
55543ad2ant1 1134 . 2 ((𝐹:(𝐴 × 𝐵)⟶𝐶𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶𝑊) → 𝐹 = (𝑥𝐴, 𝑦𝐵 ↦ (𝑥𝐹𝑦)))
5652, 55eqtr4d 2780 1 ((𝐹:(𝐴 × 𝐵)⟶𝐶𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶𝑊) → uncurry curry 𝐹 = 𝐹)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397  w3a 1088   = wceq 1542  wcel 2107  cdif 3912  c0 4287  {csn 4591  cop 4597   class class class wbr 5110   × cxp 5636  dom cdm 5638   Fn wfn 6496  wf 6497  cfv 6501  (class class class)co 7362  {coprab 7363  cmpo 7364  curry ccur 8201  uncurry cunc 8202  m cmap 8772
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-id 5536  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-ov 7365  df-oprab 7366  df-mpo 7367  df-1st 7926  df-2nd 7927  df-cur 8203  df-unc 8204  df-map 8774
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator