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 33715
Description: Closed form of mo3 2627. (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 2193 . . 3 𝑥𝑥𝑦𝜑
2 nfmo1 2569 . . 3 𝑥∃*𝑥𝜑
3 nfnf1 2196 . . . . . . 7 𝑦𝑦𝜑
43nfal 2323 . . . . . 6 𝑦𝑥𝑦𝜑
5 sp 2215 . . . . . . 7 (∀𝑥𝑦𝜑 → Ⅎ𝑦𝜑)
61, 5nfmod 2577 . . . . . 6 (∀𝑥𝑦𝜑 → Ⅎ𝑦∃*𝑥𝜑)
74, 6nfan1 2230 . . . . 5 𝑦(∀𝑥𝑦𝜑 ∧ ∃*𝑥𝜑)
8 df-mo 2564 . . . . . . 7 (∃*𝑥𝜑 ↔ ∃𝑢𝑥(𝜑𝑥 = 𝑢))
9 sp 2215 . . . . . . . . . 10 (∀𝑥(𝜑𝑥 = 𝑢) → (𝜑𝑥 = 𝑢))
10 spsbim 2482 . . . . . . . . . . 11 (∀𝑥(𝜑𝑥 = 𝑢) → ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝑥 = 𝑢))
11 equsb3 2523 . . . . . . . . . . 11 ([𝑦 / 𝑥]𝑥 = 𝑢𝑦 = 𝑢)
1210, 11syl6ib 242 . . . . . . . . . 10 (∀𝑥(𝜑𝑥 = 𝑢) → ([𝑦 / 𝑥]𝜑𝑦 = 𝑢))
139, 12anim12d 602 . . . . . . . . 9 (∀𝑥(𝜑𝑥 = 𝑢) → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → (𝑥 = 𝑢𝑦 = 𝑢)))
14 equtr2 2124 . . . . . . . . 9 ((𝑥 = 𝑢𝑦 = 𝑢) → 𝑥 = 𝑦)
1513, 14syl6 35 . . . . . . . 8 (∀𝑥(𝜑𝑥 = 𝑢) → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
1615exlimiv 2025 . . . . . . 7 (∃𝑢𝑥(𝜑𝑥 = 𝑢) → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
178, 16sylbi 208 . . . . . 6 (∃*𝑥𝜑 → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
1817adantl 473 . . . . 5 ((∀𝑥𝑦𝜑 ∧ ∃*𝑥𝜑) → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
197, 18alrimi 2246 . . . 4 ((∀𝑥𝑦𝜑 ∧ ∃*𝑥𝜑) → ∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
2019ex 401 . . 3 (∀𝑥𝑦𝜑 → (∃*𝑥𝜑 → ∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
211, 2, 20alrimd 2248 . 2 (∀𝑥𝑦𝜑 → (∃*𝑥𝜑 → ∀𝑥𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
22 nfa1 2193 . . . . . 6 𝑥𝑥((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)
23 nfs1v 2284 . . . . . 6 𝑥[𝑦 / 𝑥]𝜑
24 pm3.3 439 . . . . . . . 8 (((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) → (𝜑 → ([𝑦 / 𝑥]𝜑𝑥 = 𝑦)))
2524com23 86 . . . . . . 7 (((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) → ([𝑦 / 𝑥]𝜑 → (𝜑𝑥 = 𝑦)))
2625sps 2217 . . . . . 6 (∀𝑥((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) → ([𝑦 / 𝑥]𝜑 → (𝜑𝑥 = 𝑦)))
2722, 23, 26alrimd 2248 . . . . 5 (∀𝑥((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) → ([𝑦 / 𝑥]𝜑 → ∀𝑥(𝜑𝑥 = 𝑦)))
2827aleximi 1926 . . . 4 (∀𝑦𝑥((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) → (∃𝑦[𝑦 / 𝑥]𝜑 → ∃𝑦𝑥(𝜑𝑥 = 𝑦)))
2928alcoms 2199 . . 3 (∀𝑥𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) → (∃𝑦[𝑦 / 𝑥]𝜑 → ∃𝑦𝑥(𝜑𝑥 = 𝑦)))
30 moabs 2574 . . . 4 (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃*𝑥𝜑))
31 wl-sb8et 33692 . . . . 5 (∀𝑥𝑦𝜑 → (∃𝑥𝜑 ↔ ∃𝑦[𝑦 / 𝑥]𝜑))
32 wl-mo2t 33714 . . . . 5 (∀𝑥𝑦𝜑 → (∃*𝑥𝜑 ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦)))
3331, 32imbi12d 335 . . . 4 (∀𝑥𝑦𝜑 → ((∃𝑥𝜑 → ∃*𝑥𝜑) ↔ (∃𝑦[𝑦 / 𝑥]𝜑 → ∃𝑦𝑥(𝜑𝑥 = 𝑦))))
3430, 33syl5bb 274 . . 3 (∀𝑥𝑦𝜑 → (∃*𝑥𝜑 ↔ (∃𝑦[𝑦 / 𝑥]𝜑 → ∃𝑦𝑥(𝜑𝑥 = 𝑦))))
3529, 34syl5ibr 237 . 2 (∀𝑥𝑦𝜑 → (∀𝑥𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) → ∃*𝑥𝜑))
3621, 35impbid 203 1 (∀𝑥𝑦𝜑 → (∃*𝑥𝜑 ↔ ∀𝑥𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  wal 1650  wex 1874  wnf 1878  [wsb 2061  ∃*wmo 2562
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2349
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2564
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator