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

Theorem mosubopt 4932
Description: "At most one" remains true inside ordered pair quantification. (Contributed by NM, 28-Aug-2007.)
Assertion
Ref Expression
mosubopt (∀𝑦𝑧∃*𝑥𝜑 → ∃*𝑥𝑦𝑧(𝐴 = ⟨𝑦, 𝑧⟩ ∧ 𝜑))
Distinct variable group:   𝑥,𝑦,𝑧,𝐴
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧)

Proof of Theorem mosubopt
StepHypRef Expression
1 nfa1 2025 . . 3 𝑦𝑦𝑧∃*𝑥𝜑
2 nfe1 2024 . . . 4 𝑦𝑦𝑧(𝐴 = ⟨𝑦, 𝑧⟩ ∧ 𝜑)
32nfmo 2486 . . 3 𝑦∃*𝑥𝑦𝑧(𝐴 = ⟨𝑦, 𝑧⟩ ∧ 𝜑)
4 nfa1 2025 . . . . 5 𝑧𝑧∃*𝑥𝜑
5 nfe1 2024 . . . . . . 7 𝑧𝑧(𝐴 = ⟨𝑦, 𝑧⟩ ∧ 𝜑)
65nfex 2151 . . . . . 6 𝑧𝑦𝑧(𝐴 = ⟨𝑦, 𝑧⟩ ∧ 𝜑)
76nfmo 2486 . . . . 5 𝑧∃*𝑥𝑦𝑧(𝐴 = ⟨𝑦, 𝑧⟩ ∧ 𝜑)
8 copsexg 4916 . . . . . . . 8 (𝐴 = ⟨𝑦, 𝑧⟩ → (𝜑 ↔ ∃𝑦𝑧(𝐴 = ⟨𝑦, 𝑧⟩ ∧ 𝜑)))
98mobidv 2490 . . . . . . 7 (𝐴 = ⟨𝑦, 𝑧⟩ → (∃*𝑥𝜑 ↔ ∃*𝑥𝑦𝑧(𝐴 = ⟨𝑦, 𝑧⟩ ∧ 𝜑)))
109biimpcd 239 . . . . . 6 (∃*𝑥𝜑 → (𝐴 = ⟨𝑦, 𝑧⟩ → ∃*𝑥𝑦𝑧(𝐴 = ⟨𝑦, 𝑧⟩ ∧ 𝜑)))
1110sps 2053 . . . . 5 (∀𝑧∃*𝑥𝜑 → (𝐴 = ⟨𝑦, 𝑧⟩ → ∃*𝑥𝑦𝑧(𝐴 = ⟨𝑦, 𝑧⟩ ∧ 𝜑)))
124, 7, 11exlimd 2085 . . . 4 (∀𝑧∃*𝑥𝜑 → (∃𝑧 𝐴 = ⟨𝑦, 𝑧⟩ → ∃*𝑥𝑦𝑧(𝐴 = ⟨𝑦, 𝑧⟩ ∧ 𝜑)))
1312sps 2053 . . 3 (∀𝑦𝑧∃*𝑥𝜑 → (∃𝑧 𝐴 = ⟨𝑦, 𝑧⟩ → ∃*𝑥𝑦𝑧(𝐴 = ⟨𝑦, 𝑧⟩ ∧ 𝜑)))
141, 3, 13exlimd 2085 . 2 (∀𝑦𝑧∃*𝑥𝜑 → (∃𝑦𝑧 𝐴 = ⟨𝑦, 𝑧⟩ → ∃*𝑥𝑦𝑧(𝐴 = ⟨𝑦, 𝑧⟩ ∧ 𝜑)))
15 simpl 473 . . . . . 6 ((𝐴 = ⟨𝑦, 𝑧⟩ ∧ 𝜑) → 𝐴 = ⟨𝑦, 𝑧⟩)
16152eximi 1760 . . . . 5 (∃𝑦𝑧(𝐴 = ⟨𝑦, 𝑧⟩ ∧ 𝜑) → ∃𝑦𝑧 𝐴 = ⟨𝑦, 𝑧⟩)
1716exlimiv 1855 . . . 4 (∃𝑥𝑦𝑧(𝐴 = ⟨𝑦, 𝑧⟩ ∧ 𝜑) → ∃𝑦𝑧 𝐴 = ⟨𝑦, 𝑧⟩)
1817con3i 150 . . 3 (¬ ∃𝑦𝑧 𝐴 = ⟨𝑦, 𝑧⟩ → ¬ ∃𝑥𝑦𝑧(𝐴 = ⟨𝑦, 𝑧⟩ ∧ 𝜑))
19 exmo 2494 . . . 4 (∃𝑥𝑦𝑧(𝐴 = ⟨𝑦, 𝑧⟩ ∧ 𝜑) ∨ ∃*𝑥𝑦𝑧(𝐴 = ⟨𝑦, 𝑧⟩ ∧ 𝜑))
2019ori 390 . . 3 (¬ ∃𝑥𝑦𝑧(𝐴 = ⟨𝑦, 𝑧⟩ ∧ 𝜑) → ∃*𝑥𝑦𝑧(𝐴 = ⟨𝑦, 𝑧⟩ ∧ 𝜑))
2118, 20syl 17 . 2 (¬ ∃𝑦𝑧 𝐴 = ⟨𝑦, 𝑧⟩ → ∃*𝑥𝑦𝑧(𝐴 = ⟨𝑦, 𝑧⟩ ∧ 𝜑))
2214, 21pm2.61d1 171 1 (∀𝑦𝑧∃*𝑥𝜑 → ∃*𝑥𝑦𝑧(𝐴 = ⟨𝑦, 𝑧⟩ ∧ 𝜑))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 384  wal 1478   = wceq 1480  wex 1701  ∃*wmo 2470  cop 4154
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741  ax-nul 4749  ax-pr 4867
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rab 2916  df-v 3188  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-sn 4149  df-pr 4151  df-op 4155
This theorem is referenced by:  mosubop  4933  funoprabg  6712
  Copyright terms: Public domain W3C validator