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

Theorem mo4 2559
Description: At-most-one quantifier expressed using implicit substitution. This theorem is also a direct consequence of mo4f 2560, but this proof is based on fewer axioms.

By the way, swapping 𝑥, 𝑦 and 𝜑, 𝜓 leads to an expression for ∃*𝑦𝜓, which is equivalent to ∃*𝑥𝜑 (is a proof line), so the right hand side is a rare instance of an expression where swapping the quantifiers can be done without ax-11 2154. (Contributed by NM, 26-Jul-1995.) Reduce axiom usage. (Revised by Wolf Lammen, 18-Oct-2023.)

Hypothesis
Ref Expression
mo4.1 (𝑥 = 𝑦 → (𝜑𝜓))
Assertion
Ref Expression
mo4 (∃*𝑥𝜑 ↔ ∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦))
Distinct variable groups:   𝑥,𝑦   𝜑,𝑦   𝜓,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem mo4
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 df-mo 2533 . . 3 (∃*𝑥𝜑 ↔ ∃𝑧𝑥(𝜑𝑥 = 𝑧))
2 mo4.1 . . . . . . . 8 (𝑥 = 𝑦 → (𝜑𝜓))
3 equequ1 2028 . . . . . . . 8 (𝑥 = 𝑦 → (𝑥 = 𝑧𝑦 = 𝑧))
42, 3imbi12d 344 . . . . . . 7 (𝑥 = 𝑦 → ((𝜑𝑥 = 𝑧) ↔ (𝜓𝑦 = 𝑧)))
54cbvalvw 2039 . . . . . 6 (∀𝑥(𝜑𝑥 = 𝑧) ↔ ∀𝑦(𝜓𝑦 = 𝑧))
65biimpi 215 . . . . 5 (∀𝑥(𝜑𝑥 = 𝑧) → ∀𝑦(𝜓𝑦 = 𝑧))
7 pm2.27 42 . . . . . . . . . . . 12 (𝜑 → ((𝜑𝑥 = 𝑧) → 𝑥 = 𝑧))
87adantr 481 . . . . . . . . . . 11 ((𝜑𝜓) → ((𝜑𝑥 = 𝑧) → 𝑥 = 𝑧))
9 pm2.27 42 . . . . . . . . . . . 12 (𝜓 → ((𝜓𝑦 = 𝑧) → 𝑦 = 𝑧))
109adantl 482 . . . . . . . . . . 11 ((𝜑𝜓) → ((𝜓𝑦 = 𝑧) → 𝑦 = 𝑧))
118, 10anim12d 609 . . . . . . . . . 10 ((𝜑𝜓) → (((𝜑𝑥 = 𝑧) ∧ (𝜓𝑦 = 𝑧)) → (𝑥 = 𝑧𝑦 = 𝑧)))
12 equtr2 2030 . . . . . . . . . 10 ((𝑥 = 𝑧𝑦 = 𝑧) → 𝑥 = 𝑦)
1311, 12syl6com 37 . . . . . . . . 9 (((𝜑𝑥 = 𝑧) ∧ (𝜓𝑦 = 𝑧)) → ((𝜑𝜓) → 𝑥 = 𝑦))
1413ex 413 . . . . . . . 8 ((𝜑𝑥 = 𝑧) → ((𝜓𝑦 = 𝑧) → ((𝜑𝜓) → 𝑥 = 𝑦)))
1514alimdv 1919 . . . . . . 7 ((𝜑𝑥 = 𝑧) → (∀𝑦(𝜓𝑦 = 𝑧) → ∀𝑦((𝜑𝜓) → 𝑥 = 𝑦)))
1615com12 32 . . . . . 6 (∀𝑦(𝜓𝑦 = 𝑧) → ((𝜑𝑥 = 𝑧) → ∀𝑦((𝜑𝜓) → 𝑥 = 𝑦)))
1716alimdv 1919 . . . . 5 (∀𝑦(𝜓𝑦 = 𝑧) → (∀𝑥(𝜑𝑥 = 𝑧) → ∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦)))
186, 17mpcom 38 . . . 4 (∀𝑥(𝜑𝑥 = 𝑧) → ∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦))
1918exlimiv 1933 . . 3 (∃𝑧𝑥(𝜑𝑥 = 𝑧) → ∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦))
201, 19sylbi 216 . 2 (∃*𝑥𝜑 → ∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦))
212cbvexvw 2040 . . . . 5 (∃𝑥𝜑 ↔ ∃𝑦𝜓)
2221biimpri 227 . . . 4 (∃𝑦𝜓 → ∃𝑥𝜑)
23 ax6evr 2018 . . . . . . . 8 𝑧 𝑥 = 𝑧
24 pm3.2 470 . . . . . . . . . . . . . . 15 (𝜑 → (𝜓 → (𝜑𝜓)))
2524imim1d 82 . . . . . . . . . . . . . 14 (𝜑 → (((𝜑𝜓) → 𝑥 = 𝑦) → (𝜓𝑥 = 𝑦)))
26 ax7 2019 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → (𝑥 = 𝑧𝑦 = 𝑧))
2725, 26syl8 76 . . . . . . . . . . . . 13 (𝜑 → (((𝜑𝜓) → 𝑥 = 𝑦) → (𝜓 → (𝑥 = 𝑧𝑦 = 𝑧))))
2827com4r 94 . . . . . . . . . . . 12 (𝑥 = 𝑧 → (𝜑 → (((𝜑𝜓) → 𝑥 = 𝑦) → (𝜓𝑦 = 𝑧))))
2928impcom 408 . . . . . . . . . . 11 ((𝜑𝑥 = 𝑧) → (((𝜑𝜓) → 𝑥 = 𝑦) → (𝜓𝑦 = 𝑧)))
3029alimdv 1919 . . . . . . . . . 10 ((𝜑𝑥 = 𝑧) → (∀𝑦((𝜑𝜓) → 𝑥 = 𝑦) → ∀𝑦(𝜓𝑦 = 𝑧)))
3130impancom 452 . . . . . . . . 9 ((𝜑 ∧ ∀𝑦((𝜑𝜓) → 𝑥 = 𝑦)) → (𝑥 = 𝑧 → ∀𝑦(𝜓𝑦 = 𝑧)))
3231eximdv 1920 . . . . . . . 8 ((𝜑 ∧ ∀𝑦((𝜑𝜓) → 𝑥 = 𝑦)) → (∃𝑧 𝑥 = 𝑧 → ∃𝑧𝑦(𝜓𝑦 = 𝑧)))
3323, 32mpi 20 . . . . . . 7 ((𝜑 ∧ ∀𝑦((𝜑𝜓) → 𝑥 = 𝑦)) → ∃𝑧𝑦(𝜓𝑦 = 𝑧))
34 df-mo 2533 . . . . . . 7 (∃*𝑦𝜓 ↔ ∃𝑧𝑦(𝜓𝑦 = 𝑧))
3533, 34sylibr 233 . . . . . 6 ((𝜑 ∧ ∀𝑦((𝜑𝜓) → 𝑥 = 𝑦)) → ∃*𝑦𝜓)
3635expcom 414 . . . . 5 (∀𝑦((𝜑𝜓) → 𝑥 = 𝑦) → (𝜑 → ∃*𝑦𝜓))
3736aleximi 1834 . . . 4 (∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦) → (∃𝑥𝜑 → ∃𝑥∃*𝑦𝜓))
38 ax5e 1915 . . . 4 (∃𝑥∃*𝑦𝜓 → ∃*𝑦𝜓)
3922, 37, 38syl56 36 . . 3 (∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦) → (∃𝑦𝜓 → ∃*𝑦𝜓))
405exbii 1850 . . . . 5 (∃𝑧𝑥(𝜑𝑥 = 𝑧) ↔ ∃𝑧𝑦(𝜓𝑦 = 𝑧))
4140, 1, 343bitr4i 302 . . . 4 (∃*𝑥𝜑 ↔ ∃*𝑦𝜓)
42 moabs 2536 . . . 4 (∃*𝑦𝜓 ↔ (∃𝑦𝜓 → ∃*𝑦𝜓))
4341, 42bitri 274 . . 3 (∃*𝑥𝜑 ↔ (∃𝑦𝜓 → ∃*𝑦𝜓))
4439, 43sylibr 233 . 2 (∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦) → ∃*𝑥𝜑)
4520, 44impbii 208 1 (∃*𝑥𝜑 ↔ ∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  wal 1539  wex 1781  ∃*wmo 2531
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-mo 2533
This theorem is referenced by:  eu4  2610  moel  3397  moelOLD  3400  moeq  3699  rmo4  3722  mosneq  4836  dffun6  6545  dffun3OLD  6547  fun11  6611  brprcneu  6868  brprcneuALT  6869  dff13  7238  mpofunOLD  7517  caovmo  7627  wemoiso  7942  wemoiso2  7943  addsrmo  11050  mulsrmo  11051  summo  15645  prodmo  15862  hausflimi  23413  vitalilem3  25056  plyexmo  25755  nosupprefixmo  27130  noinfprefixmo  27131  tglineintmo  27758  ajmoi  29974  pjhthmo  30418  adjmo  30948  satfv0  34180  satfv0fun  34193  satffunlem1lem1  34224  satffunlem2lem1  34226  funtransport  34833  funray  34942  funline  34944  lineintmo  34959  cossssid4  37145  dffrege115  42500  mof0ALT  47154  mofsn  47158  f1omo  47175  thincmo  47297
  Copyright terms: Public domain W3C validator