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 35829
Description: Closed form of mo3 2562. (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 2147 . . 3 𝑥𝑥𝑦𝜑
2 nfmo1 2555 . . 3 𝑥∃*𝑥𝜑
3 nfnf1 2150 . . . . . . 7 𝑦𝑦𝜑
43nfal 2316 . . . . . 6 𝑦𝑥𝑦𝜑
5 sp 2175 . . . . . . 7 (∀𝑥𝑦𝜑 → Ⅎ𝑦𝜑)
61, 5nfmod 2559 . . . . . 6 (∀𝑥𝑦𝜑 → Ⅎ𝑦∃*𝑥𝜑)
74, 6nfan1 2192 . . . . 5 𝑦(∀𝑥𝑦𝜑 ∧ ∃*𝑥𝜑)
8 df-mo 2538 . . . . . . 7 (∃*𝑥𝜑 ↔ ∃𝑢𝑥(𝜑𝑥 = 𝑢))
9 sp 2175 . . . . . . . . . 10 (∀𝑥(𝜑𝑥 = 𝑢) → (𝜑𝑥 = 𝑢))
10 spsbim 2074 . . . . . . . . . . 11 (∀𝑥(𝜑𝑥 = 𝑢) → ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝑥 = 𝑢))
11 equsb3 2100 . . . . . . . . . . 11 ([𝑦 / 𝑥]𝑥 = 𝑢𝑦 = 𝑢)
1210, 11syl6ib 250 . . . . . . . . . 10 (∀𝑥(𝜑𝑥 = 𝑢) → ([𝑦 / 𝑥]𝜑𝑦 = 𝑢))
139, 12anim12d 609 . . . . . . . . 9 (∀𝑥(𝜑𝑥 = 𝑢) → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → (𝑥 = 𝑢𝑦 = 𝑢)))
14 equtr2 2029 . . . . . . . . 9 ((𝑥 = 𝑢𝑦 = 𝑢) → 𝑥 = 𝑦)
1513, 14syl6 35 . . . . . . . 8 (∀𝑥(𝜑𝑥 = 𝑢) → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
1615exlimiv 1932 . . . . . . 7 (∃𝑢𝑥(𝜑𝑥 = 𝑢) → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
178, 16sylbi 216 . . . . . 6 (∃*𝑥𝜑 → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
1817adantl 482 . . . . 5 ((∀𝑥𝑦𝜑 ∧ ∃*𝑥𝜑) → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
197, 18alrimi 2205 . . . 4 ((∀𝑥𝑦𝜑 ∧ ∃*𝑥𝜑) → ∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
2019ex 413 . . 3 (∀𝑥𝑦𝜑 → (∃*𝑥𝜑 → ∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
211, 2, 20alrimd 2207 . 2 (∀𝑥𝑦𝜑 → (∃*𝑥𝜑 → ∀𝑥𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
22 nfa1 2147 . . . . . 6 𝑥𝑥((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)
23 nfs1v 2152 . . . . . 6 𝑥[𝑦 / 𝑥]𝜑
24 pm3.3 449 . . . . . . . 8 (((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) → (𝜑 → ([𝑦 / 𝑥]𝜑𝑥 = 𝑦)))
2524com23 86 . . . . . . 7 (((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) → ([𝑦 / 𝑥]𝜑 → (𝜑𝑥 = 𝑦)))
2625sps 2177 . . . . . 6 (∀𝑥((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) → ([𝑦 / 𝑥]𝜑 → (𝜑𝑥 = 𝑦)))
2722, 23, 26alrimd 2207 . . . . 5 (∀𝑥((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) → ([𝑦 / 𝑥]𝜑 → ∀𝑥(𝜑𝑥 = 𝑦)))
2827aleximi 1833 . . . 4 (∀𝑦𝑥((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) → (∃𝑦[𝑦 / 𝑥]𝜑 → ∃𝑦𝑥(𝜑𝑥 = 𝑦)))
2928alcoms 2154 . . 3 (∀𝑥𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) → (∃𝑦[𝑦 / 𝑥]𝜑 → ∃𝑦𝑥(𝜑𝑥 = 𝑦)))
30 moabs 2541 . . . 4 (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃*𝑥𝜑))
31 wl-sb8et 35806 . . . . 5 (∀𝑥𝑦𝜑 → (∃𝑥𝜑 ↔ ∃𝑦[𝑦 / 𝑥]𝜑))
32 wl-mo2t 35828 . . . . 5 (∀𝑥𝑦𝜑 → (∃*𝑥𝜑 ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦)))
3331, 32imbi12d 344 . . . 4 (∀𝑥𝑦𝜑 → ((∃𝑥𝜑 → ∃*𝑥𝜑) ↔ (∃𝑦[𝑦 / 𝑥]𝜑 → ∃𝑦𝑥(𝜑𝑥 = 𝑦))))
3430, 33bitrid 282 . . 3 (∀𝑥𝑦𝜑 → (∃*𝑥𝜑 ↔ (∃𝑦[𝑦 / 𝑥]𝜑 → ∃𝑦𝑥(𝜑𝑥 = 𝑦))))
3529, 34syl5ibr 245 . 2 (∀𝑥𝑦𝜑 → (∀𝑥𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) → ∃*𝑥𝜑))
3621, 35impbid 211 1 (∀𝑥𝑦𝜑 → (∃*𝑥𝜑 ↔ ∀𝑥𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  wal 1538  wex 1780  wnf 1784  [wsb 2066  ∃*wmo 2536
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-10 2136  ax-11 2153  ax-12 2170  ax-13 2370
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1543  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator