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 33590
Description: Closed form of mo3 2609. (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 2141 . . 3 𝑥𝑥𝑦𝜑
2 nfmo1 2582 . . 3 𝑥∃*𝑥𝜑
3 nfnf1 2144 . . . . . . 7 𝑦𝑦𝜑
43nfal 2264 . . . . . 6 𝑦𝑥𝑦𝜑
5 sp 2164 . . . . . . 7 (∀𝑥𝑦𝜑 → Ⅎ𝑦𝜑)
61, 5nfmod 2586 . . . . . 6 (∀𝑥𝑦𝜑 → Ⅎ𝑦∃*𝑥𝜑)
74, 6nfan1 2179 . . . . 5 𝑦(∀𝑥𝑦𝜑 ∧ ∃*𝑥𝜑)
8 mo2v 2578 . . . . . . 7 (∃*𝑥𝜑 ↔ ∃𝑢𝑥(𝜑𝑥 = 𝑢))
9 sp 2164 . . . . . . . . . 10 (∀𝑥(𝜑𝑥 = 𝑢) → (𝜑𝑥 = 𝑢))
10 spsbim 2495 . . . . . . . . . . 11 (∀𝑥(𝜑𝑥 = 𝑢) → ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝑥 = 𝑢))
11 equsb3 2533 . . . . . . . . . . 11 ([𝑦 / 𝑥]𝑥 = 𝑢𝑦 = 𝑢)
1210, 11syl6ib 241 . . . . . . . . . 10 (∀𝑥(𝜑𝑥 = 𝑢) → ([𝑦 / 𝑥]𝜑𝑦 = 𝑢))
139, 12anim12d 587 . . . . . . . . 9 (∀𝑥(𝜑𝑥 = 𝑢) → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → (𝑥 = 𝑢𝑦 = 𝑢)))
14 equtr2 2073 . . . . . . . . 9 ((𝑥 = 𝑢𝑦 = 𝑢) → 𝑥 = 𝑦)
1513, 14syl6 35 . . . . . . . 8 (∀𝑥(𝜑𝑥 = 𝑢) → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
1615exlimiv 1971 . . . . . . 7 (∃𝑢𝑥(𝜑𝑥 = 𝑢) → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
178, 16sylbi 207 . . . . . 6 (∃*𝑥𝜑 → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
1817adantl 473 . . . . 5 ((∀𝑥𝑦𝜑 ∧ ∃*𝑥𝜑) → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
197, 18alrimi 2193 . . . 4 ((∀𝑥𝑦𝜑 ∧ ∃*𝑥𝜑) → ∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
2019ex 449 . . 3 (∀𝑥𝑦𝜑 → (∃*𝑥𝜑 → ∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
211, 2, 20alrimd 2195 . 2 (∀𝑥𝑦𝜑 → (∃*𝑥𝜑 → ∀𝑥𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
22 nfa1 2141 . . . . . 6 𝑥𝑥((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)
23 nfs1v 2538 . . . . . 6 𝑥[𝑦 / 𝑥]𝜑
24 pm3.3 459 . . . . . . . 8 (((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) → (𝜑 → ([𝑦 / 𝑥]𝜑𝑥 = 𝑦)))
2524com23 86 . . . . . . 7 (((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) → ([𝑦 / 𝑥]𝜑 → (𝜑𝑥 = 𝑦)))
2625sps 2166 . . . . . 6 (∀𝑥((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) → ([𝑦 / 𝑥]𝜑 → (𝜑𝑥 = 𝑦)))
2722, 23, 26alrimd 2195 . . . . 5 (∀𝑥((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) → ([𝑦 / 𝑥]𝜑 → ∀𝑥(𝜑𝑥 = 𝑦)))
2827aleximi 1872 . . . 4 (∀𝑦𝑥((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) → (∃𝑦[𝑦 / 𝑥]𝜑 → ∃𝑦𝑥(𝜑𝑥 = 𝑦)))
2928alcoms 2148 . . 3 (∀𝑥𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) → (∃𝑦[𝑦 / 𝑥]𝜑 → ∃𝑦𝑥(𝜑𝑥 = 𝑦)))
30 moabs 2603 . . . 4 (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃*𝑥𝜑))
31 wl-sb8et 33566 . . . . 5 (∀𝑥𝑦𝜑 → (∃𝑥𝜑 ↔ ∃𝑦[𝑦 / 𝑥]𝜑))
32 wl-mo2t 33589 . . . . 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 1594  wex 1817  wnf 1821  [wsb 2010  ∃*wmo 2572
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-eu 2575  df-mo 2576
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator