Users' Mathboxes Mathbox for Wolf Lammen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  wl-mo3t Structured version   Visualization version   GIF version

Theorem wl-mo3t 33488
Description: Closed form of mo3 2536. (Contributed by Wolf Lammen, 18-Aug-2019.)
Assertion
Ref Expression
wl-mo3t (∀𝑥𝑦𝜑 → (∃*𝑥𝜑 ↔ ∀𝑥𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
Distinct variable group:   𝑥,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)

Proof of Theorem wl-mo3t
Dummy variable 𝑢 is distinct from all other variables.
StepHypRef Expression
1 nfa1 2068 . . 3 𝑥𝑥𝑦𝜑
2 nfmo1 2509 . . 3 𝑥∃*𝑥𝜑
3 nfnf1 2071 . . . . . . 7 𝑦𝑦𝜑
43nfal 2191 . . . . . 6 𝑦𝑥𝑦𝜑
5 sp 2091 . . . . . . 7 (∀𝑥𝑦𝜑 → Ⅎ𝑦𝜑)
61, 5nfmod 2513 . . . . . 6 (∀𝑥𝑦𝜑 → Ⅎ𝑦∃*𝑥𝜑)
74, 6nfan1 2106 . . . . 5 𝑦(∀𝑥𝑦𝜑 ∧ ∃*𝑥𝜑)
8 mo2v 2505 . . . . . . 7 (∃*𝑥𝜑 ↔ ∃𝑢𝑥(𝜑𝑥 = 𝑢))
9 sp 2091 . . . . . . . . . 10 (∀𝑥(𝜑𝑥 = 𝑢) → (𝜑𝑥 = 𝑢))
10 spsbim 2422 . . . . . . . . . . 11 (∀𝑥(𝜑𝑥 = 𝑢) → ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝑥 = 𝑢))
11 equsb3 2460 . . . . . . . . . . 11 ([𝑦 / 𝑥]𝑥 = 𝑢𝑦 = 𝑢)
1210, 11syl6ib 241 . . . . . . . . . 10 (∀𝑥(𝜑𝑥 = 𝑢) → ([𝑦 / 𝑥]𝜑𝑦 = 𝑢))
139, 12anim12d 585 . . . . . . . . 9 (∀𝑥(𝜑𝑥 = 𝑢) → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → (𝑥 = 𝑢𝑦 = 𝑢)))
14 equtr2 2000 . . . . . . . . 9 ((𝑥 = 𝑢𝑦 = 𝑢) → 𝑥 = 𝑦)
1513, 14syl6 35 . . . . . . . 8 (∀𝑥(𝜑𝑥 = 𝑢) → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
1615exlimiv 1898 . . . . . . 7 (∃𝑢𝑥(𝜑𝑥 = 𝑢) → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
178, 16sylbi 207 . . . . . 6 (∃*𝑥𝜑 → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
1817adantl 481 . . . . 5 ((∀𝑥𝑦𝜑 ∧ ∃*𝑥𝜑) → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
197, 18alrimi 2120 . . . 4 ((∀𝑥𝑦𝜑 ∧ ∃*𝑥𝜑) → ∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
2019ex 449 . . 3 (∀𝑥𝑦𝜑 → (∃*𝑥𝜑 → ∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
211, 2, 20alrimd 2122 . 2 (∀𝑥𝑦𝜑 → (∃*𝑥𝜑 → ∀𝑥𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
22 nfa1 2068 . . . . . 6 𝑥𝑥((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)
23 nfs1v 2465 . . . . . 6 𝑥[𝑦 / 𝑥]𝜑
24 pm3.3 459 . . . . . . . 8 (((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) → (𝜑 → ([𝑦 / 𝑥]𝜑𝑥 = 𝑦)))
2524com23 86 . . . . . . 7 (((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) → ([𝑦 / 𝑥]𝜑 → (𝜑𝑥 = 𝑦)))
2625sps 2093 . . . . . 6 (∀𝑥((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) → ([𝑦 / 𝑥]𝜑 → (𝜑𝑥 = 𝑦)))
2722, 23, 26alrimd 2122 . . . . 5 (∀𝑥((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) → ([𝑦 / 𝑥]𝜑 → ∀𝑥(𝜑𝑥 = 𝑦)))
2827aleximi 1799 . . . 4 (∀𝑦𝑥((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) → (∃𝑦[𝑦 / 𝑥]𝜑 → ∃𝑦𝑥(𝜑𝑥 = 𝑦)))
2928alcoms 2075 . . 3 (∀𝑥𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) → (∃𝑦[𝑦 / 𝑥]𝜑 → ∃𝑦𝑥(𝜑𝑥 = 𝑦)))
30 moabs 2530 . . . 4 (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃*𝑥𝜑))
31 wl-sb8et 33464 . . . . 5 (∀𝑥𝑦𝜑 → (∃𝑥𝜑 ↔ ∃𝑦[𝑦 / 𝑥]𝜑))
32 wl-mo2t 33487 . . . . 5 (∀𝑥𝑦𝜑 → (∃*𝑥𝜑 ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦)))
3331, 32imbi12d 333 . . . 4 (∀𝑥𝑦𝜑 → ((∃𝑥𝜑 → ∃*𝑥𝜑) ↔ (∃𝑦[𝑦 / 𝑥]𝜑 → ∃𝑦𝑥(𝜑𝑥 = 𝑦))))
3430, 33syl5bb 272 . . 3 (∀𝑥𝑦𝜑 → (∃*𝑥𝜑 ↔ (∃𝑦[𝑦 / 𝑥]𝜑 → ∃𝑦𝑥(𝜑𝑥 = 𝑦))))
3529, 34syl5ibr 236 . 2 (∀𝑥𝑦𝜑 → (∀𝑥𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) → ∃*𝑥𝜑))
3621, 35impbid 202 1 (∀𝑥𝑦𝜑 → (∃*𝑥𝜑 ↔ ∀𝑥𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  wal 1521  wex 1744  wnf 1748  [wsb 1937  ∃*wmo 2499
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator