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

Theorem mo4 2563
Description: At-most-one quantifier expressed using implicit substitution. This theorem is also a direct consequence of mo4f 2564, 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 2153. (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 2537 . . 3 (∃*𝑥𝜑 ↔ ∃𝑧𝑥(𝜑𝑥 = 𝑧))
2 mo4.1 . . . . . . . 8 (𝑥 = 𝑦 → (𝜑𝜓))
3 equequ1 2024 . . . . . . . 8 (𝑥 = 𝑦 → (𝑥 = 𝑧𝑦 = 𝑧))
42, 3imbi12d 344 . . . . . . 7 (𝑥 = 𝑦 → ((𝜑𝑥 = 𝑧) ↔ (𝜓𝑦 = 𝑧)))
54cbvalvw 2035 . . . . . 6 (∀𝑥(𝜑𝑥 = 𝑧) ↔ ∀𝑦(𝜓𝑦 = 𝑧))
65biimpi 216 . . . . 5 (∀𝑥(𝜑𝑥 = 𝑧) → ∀𝑦(𝜓𝑦 = 𝑧))
7 pm2.27 42 . . . . . . . . . . . 12 (𝜑 → ((𝜑𝑥 = 𝑧) → 𝑥 = 𝑧))
87adantr 480 . . . . . . . . . . 11 ((𝜑𝜓) → ((𝜑𝑥 = 𝑧) → 𝑥 = 𝑧))
9 pm2.27 42 . . . . . . . . . . . 12 (𝜓 → ((𝜓𝑦 = 𝑧) → 𝑦 = 𝑧))
109adantl 481 . . . . . . . . . . 11 ((𝜑𝜓) → ((𝜓𝑦 = 𝑧) → 𝑦 = 𝑧))
118, 10anim12d 608 . . . . . . . . . 10 ((𝜑𝜓) → (((𝜑𝑥 = 𝑧) ∧ (𝜓𝑦 = 𝑧)) → (𝑥 = 𝑧𝑦 = 𝑧)))
12 equtr2 2026 . . . . . . . . . 10 ((𝑥 = 𝑧𝑦 = 𝑧) → 𝑥 = 𝑦)
1311, 12syl6com 37 . . . . . . . . 9 (((𝜑𝑥 = 𝑧) ∧ (𝜓𝑦 = 𝑧)) → ((𝜑𝜓) → 𝑥 = 𝑦))
1413ex 412 . . . . . . . 8 ((𝜑𝑥 = 𝑧) → ((𝜓𝑦 = 𝑧) → ((𝜑𝜓) → 𝑥 = 𝑦)))
1514alimdv 1915 . . . . . . 7 ((𝜑𝑥 = 𝑧) → (∀𝑦(𝜓𝑦 = 𝑧) → ∀𝑦((𝜑𝜓) → 𝑥 = 𝑦)))
1615com12 32 . . . . . 6 (∀𝑦(𝜓𝑦 = 𝑧) → ((𝜑𝑥 = 𝑧) → ∀𝑦((𝜑𝜓) → 𝑥 = 𝑦)))
1716alimdv 1915 . . . . 5 (∀𝑦(𝜓𝑦 = 𝑧) → (∀𝑥(𝜑𝑥 = 𝑧) → ∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦)))
186, 17mpcom 38 . . . 4 (∀𝑥(𝜑𝑥 = 𝑧) → ∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦))
1918exlimiv 1929 . . 3 (∃𝑧𝑥(𝜑𝑥 = 𝑧) → ∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦))
201, 19sylbi 217 . 2 (∃*𝑥𝜑 → ∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦))
212cbvexvw 2036 . . . . 5 (∃𝑥𝜑 ↔ ∃𝑦𝜓)
2221biimpri 228 . . . 4 (∃𝑦𝜓 → ∃𝑥𝜑)
23 ax6evr 2014 . . . . . . . 8 𝑧 𝑥 = 𝑧
24 pm3.2 469 . . . . . . . . . . . . . . 15 (𝜑 → (𝜓 → (𝜑𝜓)))
2524imim1d 82 . . . . . . . . . . . . . 14 (𝜑 → (((𝜑𝜓) → 𝑥 = 𝑦) → (𝜓𝑥 = 𝑦)))
26 ax7 2015 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → (𝑥 = 𝑧𝑦 = 𝑧))
2725, 26syl8 76 . . . . . . . . . . . . 13 (𝜑 → (((𝜑𝜓) → 𝑥 = 𝑦) → (𝜓 → (𝑥 = 𝑧𝑦 = 𝑧))))
2827com4r 94 . . . . . . . . . . . 12 (𝑥 = 𝑧 → (𝜑 → (((𝜑𝜓) → 𝑥 = 𝑦) → (𝜓𝑦 = 𝑧))))
2928impcom 407 . . . . . . . . . . 11 ((𝜑𝑥 = 𝑧) → (((𝜑𝜓) → 𝑥 = 𝑦) → (𝜓𝑦 = 𝑧)))
3029alimdv 1915 . . . . . . . . . 10 ((𝜑𝑥 = 𝑧) → (∀𝑦((𝜑𝜓) → 𝑥 = 𝑦) → ∀𝑦(𝜓𝑦 = 𝑧)))
3130impancom 451 . . . . . . . . 9 ((𝜑 ∧ ∀𝑦((𝜑𝜓) → 𝑥 = 𝑦)) → (𝑥 = 𝑧 → ∀𝑦(𝜓𝑦 = 𝑧)))
3231eximdv 1916 . . . . . . . 8 ((𝜑 ∧ ∀𝑦((𝜑𝜓) → 𝑥 = 𝑦)) → (∃𝑧 𝑥 = 𝑧 → ∃𝑧𝑦(𝜓𝑦 = 𝑧)))
3323, 32mpi 20 . . . . . . 7 ((𝜑 ∧ ∀𝑦((𝜑𝜓) → 𝑥 = 𝑦)) → ∃𝑧𝑦(𝜓𝑦 = 𝑧))
34 df-mo 2537 . . . . . . 7 (∃*𝑦𝜓 ↔ ∃𝑧𝑦(𝜓𝑦 = 𝑧))
3533, 34sylibr 234 . . . . . 6 ((𝜑 ∧ ∀𝑦((𝜑𝜓) → 𝑥 = 𝑦)) → ∃*𝑦𝜓)
3635expcom 413 . . . . 5 (∀𝑦((𝜑𝜓) → 𝑥 = 𝑦) → (𝜑 → ∃*𝑦𝜓))
3736aleximi 1830 . . . 4 (∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦) → (∃𝑥𝜑 → ∃𝑥∃*𝑦𝜓))
38 ax5e 1911 . . . 4 (∃𝑥∃*𝑦𝜓 → ∃*𝑦𝜓)
3922, 37, 38syl56 36 . . 3 (∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦) → (∃𝑦𝜓 → ∃*𝑦𝜓))
405exbii 1846 . . . . 5 (∃𝑧𝑥(𝜑𝑥 = 𝑧) ↔ ∃𝑧𝑦(𝜓𝑦 = 𝑧))
4140, 1, 343bitr4i 303 . . . 4 (∃*𝑥𝜑 ↔ ∃*𝑦𝜓)
42 moabs 2540 . . . 4 (∃*𝑦𝜓 ↔ (∃𝑦𝜓 → ∃*𝑦𝜓))
4341, 42bitri 275 . . 3 (∃*𝑥𝜑 ↔ (∃𝑦𝜓 → ∃*𝑦𝜓))
4439, 43sylibr 234 . 2 (∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦) → ∃*𝑥𝜑)
4520, 44impbii 209 1 (∃*𝑥𝜑 ↔ ∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wal 1535  wex 1777  ∃*wmo 2535
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-mo 2537
This theorem is referenced by:  eu4  2612  moel  3405  moelOLD  3408  moeq  3723  rmo4  3746  mosneq  4867  dffun6  6585  dffun3OLD  6587  fun11  6651  brprcneu  6909  brprcneuALT  6910  dff13  7290  caovmo  7683  wemoiso  8010  wemoiso2  8011  addsrmo  11138  mulsrmo  11139  summo  15761  prodmo  15978  hausflimi  24002  vitalilem3  25657  plyexmo  26365  nosupprefixmo  27754  noinfprefixmo  27755  tglineintmo  28659  ajmoi  30881  pjhthmo  31325  adjmo  31855  satfv0  35318  satfv0fun  35331  satffunlem1lem1  35362  satffunlem2lem1  35364  funtransport  35987  funray  36096  funline  36098  lineintmo  36113  cossssid4  38374  dffrege115  43880  mof0ALT  48471  mofsn  48475  f1omo  48492  thincmo  48614
  Copyright terms: Public domain W3C validator