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

Theorem mo4 2561
Description: At-most-one quantifier expressed using implicit substitution. This theorem is also a direct consequence of mo4f 2562, 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 2155. (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 2535 . . 3 (∃*𝑥𝜑 ↔ ∃𝑧𝑥(𝜑𝑥 = 𝑧))
2 mo4.1 . . . . . . . 8 (𝑥 = 𝑦 → (𝜑𝜓))
3 equequ1 2029 . . . . . . . 8 (𝑥 = 𝑦 → (𝑥 = 𝑧𝑦 = 𝑧))
42, 3imbi12d 345 . . . . . . 7 (𝑥 = 𝑦 → ((𝜑𝑥 = 𝑧) ↔ (𝜓𝑦 = 𝑧)))
54cbvalvw 2040 . . . . . 6 (∀𝑥(𝜑𝑥 = 𝑧) ↔ ∀𝑦(𝜓𝑦 = 𝑧))
65biimpi 215 . . . . 5 (∀𝑥(𝜑𝑥 = 𝑧) → ∀𝑦(𝜓𝑦 = 𝑧))
7 pm2.27 42 . . . . . . . . . . . 12 (𝜑 → ((𝜑𝑥 = 𝑧) → 𝑥 = 𝑧))
87adantr 482 . . . . . . . . . . 11 ((𝜑𝜓) → ((𝜑𝑥 = 𝑧) → 𝑥 = 𝑧))
9 pm2.27 42 . . . . . . . . . . . 12 (𝜓 → ((𝜓𝑦 = 𝑧) → 𝑦 = 𝑧))
109adantl 483 . . . . . . . . . . 11 ((𝜑𝜓) → ((𝜓𝑦 = 𝑧) → 𝑦 = 𝑧))
118, 10anim12d 610 . . . . . . . . . 10 ((𝜑𝜓) → (((𝜑𝑥 = 𝑧) ∧ (𝜓𝑦 = 𝑧)) → (𝑥 = 𝑧𝑦 = 𝑧)))
12 equtr2 2031 . . . . . . . . . 10 ((𝑥 = 𝑧𝑦 = 𝑧) → 𝑥 = 𝑦)
1311, 12syl6com 37 . . . . . . . . 9 (((𝜑𝑥 = 𝑧) ∧ (𝜓𝑦 = 𝑧)) → ((𝜑𝜓) → 𝑥 = 𝑦))
1413ex 414 . . . . . . . 8 ((𝜑𝑥 = 𝑧) → ((𝜓𝑦 = 𝑧) → ((𝜑𝜓) → 𝑥 = 𝑦)))
1514alimdv 1920 . . . . . . 7 ((𝜑𝑥 = 𝑧) → (∀𝑦(𝜓𝑦 = 𝑧) → ∀𝑦((𝜑𝜓) → 𝑥 = 𝑦)))
1615com12 32 . . . . . 6 (∀𝑦(𝜓𝑦 = 𝑧) → ((𝜑𝑥 = 𝑧) → ∀𝑦((𝜑𝜓) → 𝑥 = 𝑦)))
1716alimdv 1920 . . . . 5 (∀𝑦(𝜓𝑦 = 𝑧) → (∀𝑥(𝜑𝑥 = 𝑧) → ∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦)))
186, 17mpcom 38 . . . 4 (∀𝑥(𝜑𝑥 = 𝑧) → ∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦))
1918exlimiv 1934 . . 3 (∃𝑧𝑥(𝜑𝑥 = 𝑧) → ∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦))
201, 19sylbi 216 . 2 (∃*𝑥𝜑 → ∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦))
212cbvexvw 2041 . . . . 5 (∃𝑥𝜑 ↔ ∃𝑦𝜓)
2221biimpri 227 . . . 4 (∃𝑦𝜓 → ∃𝑥𝜑)
23 ax6evr 2019 . . . . . . . 8 𝑧 𝑥 = 𝑧
24 pm3.2 471 . . . . . . . . . . . . . . 15 (𝜑 → (𝜓 → (𝜑𝜓)))
2524imim1d 82 . . . . . . . . . . . . . 14 (𝜑 → (((𝜑𝜓) → 𝑥 = 𝑦) → (𝜓𝑥 = 𝑦)))
26 ax7 2020 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → (𝑥 = 𝑧𝑦 = 𝑧))
2725, 26syl8 76 . . . . . . . . . . . . 13 (𝜑 → (((𝜑𝜓) → 𝑥 = 𝑦) → (𝜓 → (𝑥 = 𝑧𝑦 = 𝑧))))
2827com4r 94 . . . . . . . . . . . 12 (𝑥 = 𝑧 → (𝜑 → (((𝜑𝜓) → 𝑥 = 𝑦) → (𝜓𝑦 = 𝑧))))
2928impcom 409 . . . . . . . . . . 11 ((𝜑𝑥 = 𝑧) → (((𝜑𝜓) → 𝑥 = 𝑦) → (𝜓𝑦 = 𝑧)))
3029alimdv 1920 . . . . . . . . . 10 ((𝜑𝑥 = 𝑧) → (∀𝑦((𝜑𝜓) → 𝑥 = 𝑦) → ∀𝑦(𝜓𝑦 = 𝑧)))
3130impancom 453 . . . . . . . . 9 ((𝜑 ∧ ∀𝑦((𝜑𝜓) → 𝑥 = 𝑦)) → (𝑥 = 𝑧 → ∀𝑦(𝜓𝑦 = 𝑧)))
3231eximdv 1921 . . . . . . . 8 ((𝜑 ∧ ∀𝑦((𝜑𝜓) → 𝑥 = 𝑦)) → (∃𝑧 𝑥 = 𝑧 → ∃𝑧𝑦(𝜓𝑦 = 𝑧)))
3323, 32mpi 20 . . . . . . 7 ((𝜑 ∧ ∀𝑦((𝜑𝜓) → 𝑥 = 𝑦)) → ∃𝑧𝑦(𝜓𝑦 = 𝑧))
34 df-mo 2535 . . . . . . 7 (∃*𝑦𝜓 ↔ ∃𝑧𝑦(𝜓𝑦 = 𝑧))
3533, 34sylibr 233 . . . . . 6 ((𝜑 ∧ ∀𝑦((𝜑𝜓) → 𝑥 = 𝑦)) → ∃*𝑦𝜓)
3635expcom 415 . . . . 5 (∀𝑦((𝜑𝜓) → 𝑥 = 𝑦) → (𝜑 → ∃*𝑦𝜓))
3736aleximi 1835 . . . 4 (∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦) → (∃𝑥𝜑 → ∃𝑥∃*𝑦𝜓))
38 ax5e 1916 . . . 4 (∃𝑥∃*𝑦𝜓 → ∃*𝑦𝜓)
3922, 37, 38syl56 36 . . 3 (∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦) → (∃𝑦𝜓 → ∃*𝑦𝜓))
405exbii 1851 . . . . 5 (∃𝑧𝑥(𝜑𝑥 = 𝑧) ↔ ∃𝑧𝑦(𝜓𝑦 = 𝑧))
4140, 1, 343bitr4i 303 . . . 4 (∃*𝑥𝜑 ↔ ∃*𝑦𝜓)
42 moabs 2538 . . . 4 (∃*𝑦𝜓 ↔ (∃𝑦𝜓 → ∃*𝑦𝜓))
4341, 42bitri 275 . . 3 (∃*𝑥𝜑 ↔ (∃𝑦𝜓 → ∃*𝑦𝜓))
4439, 43sylibr 233 . 2 (∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦) → ∃*𝑥𝜑)
4520, 44impbii 208 1 (∃*𝑥𝜑 ↔ ∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397  wal 1540  wex 1782  ∃*wmo 2533
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
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-mo 2535
This theorem is referenced by:  eu4  2612  moel  3399  moelOLD  3402  moeq  3704  rmo4  3727  mosneq  4844  dffun6  6557  dffun3OLD  6559  fun11  6623  brprcneu  6882  brprcneuALT  6883  dff13  7254  mpofunOLD  7533  caovmo  7644  wemoiso  7960  wemoiso2  7961  addsrmo  11068  mulsrmo  11069  summo  15663  prodmo  15880  hausflimi  23484  vitalilem3  25127  plyexmo  25826  nosupprefixmo  27203  noinfprefixmo  27204  tglineintmo  27893  ajmoi  30111  pjhthmo  30555  adjmo  31085  satfv0  34349  satfv0fun  34362  satffunlem1lem1  34393  satffunlem2lem1  34395  funtransport  35003  funray  35112  funline  35114  lineintmo  35129  cossssid4  37340  dffrege115  42729  mof0ALT  47506  mofsn  47510  f1omo  47527  thincmo  47649
  Copyright terms: Public domain W3C validator