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 32987
Description: Closed form of mo3 2506. (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 2025 . . 3 𝑥𝑥𝑦𝜑
2 nfmo1 2480 . . 3 𝑥∃*𝑥𝜑
3 nfnf1 2028 . . . . . . 7 𝑦𝑦𝜑
43nfal 2150 . . . . . 6 𝑦𝑥𝑦𝜑
5 sp 2051 . . . . . . 7 (∀𝑥𝑦𝜑 → Ⅎ𝑦𝜑)
61, 5nfmod 2484 . . . . . 6 (∀𝑥𝑦𝜑 → Ⅎ𝑦∃*𝑥𝜑)
74, 6nfan1 2066 . . . . 5 𝑦(∀𝑥𝑦𝜑 ∧ ∃*𝑥𝜑)
8 mo2v 2476 . . . . . . 7 (∃*𝑥𝜑 ↔ ∃𝑢𝑥(𝜑𝑥 = 𝑢))
9 sp 2051 . . . . . . . . . 10 (∀𝑥(𝜑𝑥 = 𝑢) → (𝜑𝑥 = 𝑢))
10 spsbim 2393 . . . . . . . . . . 11 (∀𝑥(𝜑𝑥 = 𝑢) → ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝑥 = 𝑢))
11 equsb3 2431 . . . . . . . . . . 11 ([𝑦 / 𝑥]𝑥 = 𝑢𝑦 = 𝑢)
1210, 11syl6ib 241 . . . . . . . . . 10 (∀𝑥(𝜑𝑥 = 𝑢) → ([𝑦 / 𝑥]𝜑𝑦 = 𝑢))
139, 12anim12d 585 . . . . . . . . 9 (∀𝑥(𝜑𝑥 = 𝑢) → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → (𝑥 = 𝑢𝑦 = 𝑢)))
14 equtr2 1951 . . . . . . . . 9 ((𝑥 = 𝑢𝑦 = 𝑢) → 𝑥 = 𝑦)
1513, 14syl6 35 . . . . . . . 8 (∀𝑥(𝜑𝑥 = 𝑢) → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
1615exlimiv 1855 . . . . . . 7 (∃𝑢𝑥(𝜑𝑥 = 𝑢) → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
178, 16sylbi 207 . . . . . 6 (∃*𝑥𝜑 → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
1817adantl 482 . . . . 5 ((∀𝑥𝑦𝜑 ∧ ∃*𝑥𝜑) → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
197, 18alrimi 2080 . . . 4 ((∀𝑥𝑦𝜑 ∧ ∃*𝑥𝜑) → ∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
2019ex 450 . . 3 (∀𝑥𝑦𝜑 → (∃*𝑥𝜑 → ∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
211, 2, 20alrimd 2082 . 2 (∀𝑥𝑦𝜑 → (∃*𝑥𝜑 → ∀𝑥𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
22 nfa1 2025 . . . . . 6 𝑥𝑥((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)
23 nfs1v 2436 . . . . . 6 𝑥[𝑦 / 𝑥]𝜑
24 pm3.3 460 . . . . . . . 8 (((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) → (𝜑 → ([𝑦 / 𝑥]𝜑𝑥 = 𝑦)))
2524com23 86 . . . . . . 7 (((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) → ([𝑦 / 𝑥]𝜑 → (𝜑𝑥 = 𝑦)))
2625sps 2053 . . . . . 6 (∀𝑥((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) → ([𝑦 / 𝑥]𝜑 → (𝜑𝑥 = 𝑦)))
2722, 23, 26alrimd 2082 . . . . 5 (∀𝑥((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) → ([𝑦 / 𝑥]𝜑 → ∀𝑥(𝜑𝑥 = 𝑦)))
2827aleximi 1756 . . . 4 (∀𝑦𝑥((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) → (∃𝑦[𝑦 / 𝑥]𝜑 → ∃𝑦𝑥(𝜑𝑥 = 𝑦)))
2928alcoms 2032 . . 3 (∀𝑥𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) → (∃𝑦[𝑦 / 𝑥]𝜑 → ∃𝑦𝑥(𝜑𝑥 = 𝑦)))
30 moabs 2500 . . . 4 (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃*𝑥𝜑))
31 wl-sb8et 32963 . . . . 5 (∀𝑥𝑦𝜑 → (∃𝑥𝜑 ↔ ∃𝑦[𝑦 / 𝑥]𝜑))
32 wl-mo2t 32986 . . . . 5 (∀𝑥𝑦𝜑 → (∃*𝑥𝜑 ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦)))
3331, 32imbi12d 334 . . . 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 384  wal 1478  wex 1701  wnf 1705  [wsb 1877  ∃*wmo 2470
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-10 2016  ax-11 2031  ax-12 2044  ax-13 2245
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator