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

Theorem kmlem1 9565
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 3447 . . . . . 6 𝑣 ∈ V
21rabex 5202 . . . . 5 {𝑢𝑣𝑢 ≠ ∅} ∈ V
3 raleq 3361 . . . . . . 7 (𝑥 = {𝑢𝑣𝑢 ≠ ∅} → (∀𝑧𝑥 𝑧 ≠ ∅ ↔ ∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝑧 ≠ ∅))
4 raleq 3361 . . . . . . . 8 (𝑥 = {𝑢𝑣𝑢 ≠ ∅} → (∀𝑤𝑥 𝜑 ↔ ∀𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜑))
54raleqbi1dv 3359 . . . . . . 7 (𝑥 = {𝑢𝑣𝑢 ≠ ∅} → (∀𝑧𝑥𝑤𝑥 𝜑 ↔ ∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}∀𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜑))
63, 5anbi12d 633 . . . . . 6 (𝑥 = {𝑢𝑣𝑢 ≠ ∅} → ((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 𝜑) ↔ (∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝑧 ≠ ∅ ∧ ∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}∀𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜑)))
7 raleq 3361 . . . . . . 7 (𝑥 = {𝑢𝑣𝑢 ≠ ∅} → (∀𝑧𝑥 𝜓 ↔ ∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜓))
87exbidv 1922 . . . . . 6 (𝑥 = {𝑢𝑣𝑢 ≠ ∅} → (∃𝑦𝑧𝑥 𝜓 ↔ ∃𝑦𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜓))
96, 8imbi12d 348 . . . . 5 (𝑥 = {𝑢𝑣𝑢 ≠ ∅} → (((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 𝜑) → ∃𝑦𝑧𝑥 𝜓) ↔ ((∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝑧 ≠ ∅ ∧ ∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}∀𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜑) → ∃𝑦𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜓)))
102, 9spcv 3557 . . . 4 (∀𝑥((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 𝜑) → ∃𝑦𝑧𝑥 𝜓) → ((∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝑧 ≠ ∅ ∧ ∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}∀𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜑) → ∃𝑦𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜓))
1110alrimiv 1928 . . 3 (∀𝑥((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 𝜑) → ∃𝑦𝑧𝑥 𝜓) → ∀𝑣((∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝑧 ≠ ∅ ∧ ∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}∀𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜑) → ∃𝑦𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜓))
12 elrabi 3626 . . . . . . 7 (𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅} → 𝑧𝑣)
13 elrabi 3626 . . . . . . . . 9 (𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅} → 𝑤𝑣)
1413imim1i 63 . . . . . . . 8 ((𝑤𝑣𝜑) → (𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅} → 𝜑))
1514ralimi2 3128 . . . . . . 7 (∀𝑤𝑣 𝜑 → ∀𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜑)
1612, 15imim12i 62 . . . . . 6 ((𝑧𝑣 → ∀𝑤𝑣 𝜑) → (𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅} → ∀𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜑))
1716ralimi2 3128 . . . . 5 (∀𝑧𝑣𝑤𝑣 𝜑 → ∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}∀𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜑)
18 neeq1 3052 . . . . . . . 8 (𝑢 = 𝑧 → (𝑢 ≠ ∅ ↔ 𝑧 ≠ ∅))
1918elrab 3631 . . . . . . 7 (𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅} ↔ (𝑧𝑣𝑧 ≠ ∅))
2019simprbi 500 . . . . . 6 (𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅} → 𝑧 ≠ ∅)
2120rgen 3119 . . . . 5 𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝑧 ≠ ∅
2217, 21jctil 523 . . . 4 (∀𝑧𝑣𝑤𝑣 𝜑 → (∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝑧 ≠ ∅ ∧ ∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}∀𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜑))
2319biimpri 231 . . . . . . . 8 ((𝑧𝑣𝑧 ≠ ∅) → 𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅})
2423imim1i 63 . . . . . . 7 ((𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅} → 𝜓) → ((𝑧𝑣𝑧 ≠ ∅) → 𝜓))
2524expd 419 . . . . . 6 ((𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅} → 𝜓) → (𝑧𝑣 → (𝑧 ≠ ∅ → 𝜓)))
2625ralimi2 3128 . . . . 5 (∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜓 → ∀𝑧𝑣 (𝑧 ≠ ∅ → 𝜓))
2726eximi 1836 . . . 4 (∃𝑦𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜓 → ∃𝑦𝑧𝑣 (𝑧 ≠ ∅ → 𝜓))
2822, 27imim12i 62 . . 3 (((∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝑧 ≠ ∅ ∧ ∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}∀𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜑) → ∃𝑦𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜓) → (∀𝑧𝑣𝑤𝑣 𝜑 → ∃𝑦𝑧𝑣 (𝑧 ≠ ∅ → 𝜓)))
2911, 28sylg 1824 . 2 (∀𝑥((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 𝜑) → ∃𝑦𝑧𝑥 𝜓) → ∀𝑣(∀𝑧𝑣𝑤𝑣 𝜑 → ∃𝑦𝑧𝑣 (𝑧 ≠ ∅ → 𝜓)))
30 raleq 3361 . . . . 5 (𝑣 = 𝑥 → (∀𝑤𝑣 𝜑 ↔ ∀𝑤𝑥 𝜑))
3130raleqbi1dv 3359 . . . 4 (𝑣 = 𝑥 → (∀𝑧𝑣𝑤𝑣 𝜑 ↔ ∀𝑧𝑥𝑤𝑥 𝜑))
32 raleq 3361 . . . . 5 (𝑣 = 𝑥 → (∀𝑧𝑣 (𝑧 ≠ ∅ → 𝜓) ↔ ∀𝑧𝑥 (𝑧 ≠ ∅ → 𝜓)))
3332exbidv 1922 . . . 4 (𝑣 = 𝑥 → (∃𝑦𝑧𝑣 (𝑧 ≠ ∅ → 𝜓) ↔ ∃𝑦𝑧𝑥 (𝑧 ≠ ∅ → 𝜓)))
3431, 33imbi12d 348 . . 3 (𝑣 = 𝑥 → ((∀𝑧𝑣𝑤𝑣 𝜑 → ∃𝑦𝑧𝑣 (𝑧 ≠ ∅ → 𝜓)) ↔ (∀𝑧𝑥𝑤𝑥 𝜑 → ∃𝑦𝑧𝑥 (𝑧 ≠ ∅ → 𝜓))))
3534cbvalvw 2043 . 2 (∀𝑣(∀𝑧𝑣𝑤𝑣 𝜑 → ∃𝑦𝑧𝑣 (𝑧 ≠ ∅ → 𝜓)) ↔ ∀𝑥(∀𝑧𝑥𝑤𝑥 𝜑 → ∃𝑦𝑧𝑥 (𝑧 ≠ ∅ → 𝜓)))
3629, 35sylib 221 1 (∀𝑥((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 𝜑) → ∃𝑦𝑧𝑥 𝜓) → ∀𝑥(∀𝑧𝑥𝑤𝑥 𝜑 → ∃𝑦𝑧𝑥 (𝑧 ≠ ∅ → 𝜓)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  wal 1536   = wceq 1538  wex 1781  wcel 2112  wne 2990  wral 3109  {crab 3113  c0 4246
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-ral 3114  df-rab 3118  df-v 3446  df-in 3891  df-ss 3901
This theorem is referenced by:  kmlem13  9577
  Copyright terms: Public domain W3C validator