MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  kmlem1 Structured version   Visualization version   GIF version

Theorem kmlem1 9264
Description: Lemma for 5-quantifier AC of Kurt Maes, Th. 4, 1 => 2. (Contributed by NM, 5-Apr-2004.)
Assertion
Ref Expression
kmlem1 (∀𝑥((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 𝜑) → ∃𝑦𝑧𝑥 𝜓) → ∀𝑥(∀𝑧𝑥𝑤𝑥 𝜑 → ∃𝑦𝑧𝑥 (𝑧 ≠ ∅ → 𝜓)))
Distinct variable groups:   𝑥,𝑦,𝜑   𝜓,𝑥   𝑥,𝑤,𝑦,𝑧
Allowed substitution hints:   𝜑(𝑧,𝑤)   𝜓(𝑦,𝑧,𝑤)

Proof of Theorem kmlem1
Dummy variables 𝑣 𝑢 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vex 3405 . . . . . 6 𝑣 ∈ V
21rabex 5018 . . . . 5 {𝑢𝑣𝑢 ≠ ∅} ∈ V
3 raleq 3338 . . . . . . 7 (𝑥 = {𝑢𝑣𝑢 ≠ ∅} → (∀𝑧𝑥 𝑧 ≠ ∅ ↔ ∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝑧 ≠ ∅))
4 raleq 3338 . . . . . . . 8 (𝑥 = {𝑢𝑣𝑢 ≠ ∅} → (∀𝑤𝑥 𝜑 ↔ ∀𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜑))
54raleqbi1dv 3346 . . . . . . 7 (𝑥 = {𝑢𝑣𝑢 ≠ ∅} → (∀𝑧𝑥𝑤𝑥 𝜑 ↔ ∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}∀𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜑))
63, 5anbi12d 618 . . . . . 6 (𝑥 = {𝑢𝑣𝑢 ≠ ∅} → ((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 𝜑) ↔ (∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝑧 ≠ ∅ ∧ ∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}∀𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜑)))
7 raleq 3338 . . . . . . 7 (𝑥 = {𝑢𝑣𝑢 ≠ ∅} → (∀𝑧𝑥 𝜓 ↔ ∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜓))
87exbidv 2012 . . . . . 6 (𝑥 = {𝑢𝑣𝑢 ≠ ∅} → (∃𝑦𝑧𝑥 𝜓 ↔ ∃𝑦𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜓))
96, 8imbi12d 335 . . . . 5 (𝑥 = {𝑢𝑣𝑢 ≠ ∅} → (((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 𝜑) → ∃𝑦𝑧𝑥 𝜓) ↔ ((∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝑧 ≠ ∅ ∧ ∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}∀𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜑) → ∃𝑦𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜓)))
102, 9spcv 3503 . . . 4 (∀𝑥((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 𝜑) → ∃𝑦𝑧𝑥 𝜓) → ((∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝑧 ≠ ∅ ∧ ∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}∀𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜑) → ∃𝑦𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜓))
1110alrimiv 2018 . . 3 (∀𝑥((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 𝜑) → ∃𝑦𝑧𝑥 𝜓) → ∀𝑣((∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝑧 ≠ ∅ ∧ ∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}∀𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜑) → ∃𝑦𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜓))
12 elrabi 3565 . . . . . . 7 (𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅} → 𝑧𝑣)
13 elrabi 3565 . . . . . . . . 9 (𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅} → 𝑤𝑣)
1413imim1i 63 . . . . . . . 8 ((𝑤𝑣𝜑) → (𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅} → 𝜑))
1514ralimi2 3148 . . . . . . 7 (∀𝑤𝑣 𝜑 → ∀𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜑)
1612, 15imim12i 62 . . . . . 6 ((𝑧𝑣 → ∀𝑤𝑣 𝜑) → (𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅} → ∀𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜑))
1716ralimi2 3148 . . . . 5 (∀𝑧𝑣𝑤𝑣 𝜑 → ∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}∀𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜑)
18 neeq1 3051 . . . . . . . 8 (𝑢 = 𝑧 → (𝑢 ≠ ∅ ↔ 𝑧 ≠ ∅))
1918elrab 3570 . . . . . . 7 (𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅} ↔ (𝑧𝑣𝑧 ≠ ∅))
2019simprbi 486 . . . . . 6 (𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅} → 𝑧 ≠ ∅)
2120rgen 3121 . . . . 5 𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝑧 ≠ ∅
2217, 21jctil 511 . . . 4 (∀𝑧𝑣𝑤𝑣 𝜑 → (∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝑧 ≠ ∅ ∧ ∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}∀𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜑))
2319biimpri 219 . . . . . . . 8 ((𝑧𝑣𝑧 ≠ ∅) → 𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅})
2423imim1i 63 . . . . . . 7 ((𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅} → 𝜓) → ((𝑧𝑣𝑧 ≠ ∅) → 𝜓))
2524expd 402 . . . . . 6 ((𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅} → 𝜓) → (𝑧𝑣 → (𝑧 ≠ ∅ → 𝜓)))
2625ralimi2 3148 . . . . 5 (∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜓 → ∀𝑧𝑣 (𝑧 ≠ ∅ → 𝜓))
2726eximi 1919 . . . 4 (∃𝑦𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜓 → ∃𝑦𝑧𝑣 (𝑧 ≠ ∅ → 𝜓))
2822, 27imim12i 62 . . 3 (((∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝑧 ≠ ∅ ∧ ∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}∀𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜑) → ∃𝑦𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜓) → (∀𝑧𝑣𝑤𝑣 𝜑 → ∃𝑦𝑧𝑣 (𝑧 ≠ ∅ → 𝜓)))
2911, 28sylg 1907 . 2 (∀𝑥((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 𝜑) → ∃𝑦𝑧𝑥 𝜓) → ∀𝑣(∀𝑧𝑣𝑤𝑣 𝜑 → ∃𝑦𝑧𝑣 (𝑧 ≠ ∅ → 𝜓)))
30 raleq 3338 . . . . 5 (𝑣 = 𝑥 → (∀𝑤𝑣 𝜑 ↔ ∀𝑤𝑥 𝜑))
3130raleqbi1dv 3346 . . . 4 (𝑣 = 𝑥 → (∀𝑧𝑣𝑤𝑣 𝜑 ↔ ∀𝑧𝑥𝑤𝑥 𝜑))
32 raleq 3338 . . . . 5 (𝑣 = 𝑥 → (∀𝑧𝑣 (𝑧 ≠ ∅ → 𝜓) ↔ ∀𝑧𝑥 (𝑧 ≠ ∅ → 𝜓)))
3332exbidv 2012 . . . 4 (𝑣 = 𝑥 → (∃𝑦𝑧𝑣 (𝑧 ≠ ∅ → 𝜓) ↔ ∃𝑦𝑧𝑥 (𝑧 ≠ ∅ → 𝜓)))
3431, 33imbi12d 335 . . 3 (𝑣 = 𝑥 → ((∀𝑧𝑣𝑤𝑣 𝜑 → ∃𝑦𝑧𝑣 (𝑧 ≠ ∅ → 𝜓)) ↔ (∀𝑧𝑥𝑤𝑥 𝜑 → ∃𝑦𝑧𝑥 (𝑧 ≠ ∅ → 𝜓))))
3534cbvalvw 2137 . 2 (∀𝑣(∀𝑧𝑣𝑤𝑣 𝜑 → ∃𝑦𝑧𝑣 (𝑧 ≠ ∅ → 𝜓)) ↔ ∀𝑥(∀𝑧𝑥𝑤𝑥 𝜑 → ∃𝑦𝑧𝑥 (𝑧 ≠ ∅ → 𝜓)))
3629, 35sylib 209 1 (∀𝑥((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 𝜑) → ∃𝑦𝑧𝑥 𝜓) → ∀𝑥(∀𝑧𝑥𝑤𝑥 𝜑 → ∃𝑦𝑧𝑥 (𝑧 ≠ ∅ → 𝜓)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wal 1635   = wceq 1637  wex 1859  wcel 2157  wne 2989  wral 3107  {crab 3111  c0 4127
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-sep 4986
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ne 2990  df-ral 3112  df-rab 3116  df-v 3404  df-in 3787  df-ss 3794
This theorem is referenced by:  kmlem13  9276
  Copyright terms: Public domain W3C validator