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

Theorem kmlem1 10193
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 3466 . . . . . 6 𝑣 ∈ V
21rabex 5339 . . . . 5 {𝑢𝑣𝑢 ≠ ∅} ∈ V
3 raleq 3312 . . . . . . 7 (𝑥 = {𝑢𝑣𝑢 ≠ ∅} → (∀𝑧𝑥 𝑧 ≠ ∅ ↔ ∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝑧 ≠ ∅))
4 raleq 3312 . . . . . . . 8 (𝑥 = {𝑢𝑣𝑢 ≠ ∅} → (∀𝑤𝑥 𝜑 ↔ ∀𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜑))
54raleqbi1dv 3323 . . . . . . 7 (𝑥 = {𝑢𝑣𝑢 ≠ ∅} → (∀𝑧𝑥𝑤𝑥 𝜑 ↔ ∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}∀𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜑))
63, 5anbi12d 630 . . . . . 6 (𝑥 = {𝑢𝑣𝑢 ≠ ∅} → ((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 𝜑) ↔ (∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝑧 ≠ ∅ ∧ ∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}∀𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜑)))
7 raleq 3312 . . . . . . 7 (𝑥 = {𝑢𝑣𝑢 ≠ ∅} → (∀𝑧𝑥 𝜓 ↔ ∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜓))
87exbidv 1917 . . . . . 6 (𝑥 = {𝑢𝑣𝑢 ≠ ∅} → (∃𝑦𝑧𝑥 𝜓 ↔ ∃𝑦𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜓))
96, 8imbi12d 343 . . . . 5 (𝑥 = {𝑢𝑣𝑢 ≠ ∅} → (((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 𝜑) → ∃𝑦𝑧𝑥 𝜓) ↔ ((∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝑧 ≠ ∅ ∧ ∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}∀𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜑) → ∃𝑦𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜓)))
102, 9spcv 3591 . . . 4 (∀𝑥((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 𝜑) → ∃𝑦𝑧𝑥 𝜓) → ((∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝑧 ≠ ∅ ∧ ∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}∀𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜑) → ∃𝑦𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜓))
1110alrimiv 1923 . . 3 (∀𝑥((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 𝜑) → ∃𝑦𝑧𝑥 𝜓) → ∀𝑣((∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝑧 ≠ ∅ ∧ ∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}∀𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜑) → ∃𝑦𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜓))
12 elrabi 3675 . . . . . . 7 (𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅} → 𝑧𝑣)
13 elrabi 3675 . . . . . . . . 9 (𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅} → 𝑤𝑣)
1413imim1i 63 . . . . . . . 8 ((𝑤𝑣𝜑) → (𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅} → 𝜑))
1514ralimi2 3068 . . . . . . 7 (∀𝑤𝑣 𝜑 → ∀𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜑)
1612, 15imim12i 62 . . . . . 6 ((𝑧𝑣 → ∀𝑤𝑣 𝜑) → (𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅} → ∀𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜑))
1716ralimi2 3068 . . . . 5 (∀𝑧𝑣𝑤𝑣 𝜑 → ∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}∀𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜑)
18 neeq1 2993 . . . . . . . 8 (𝑢 = 𝑧 → (𝑢 ≠ ∅ ↔ 𝑧 ≠ ∅))
1918elrab 3681 . . . . . . 7 (𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅} ↔ (𝑧𝑣𝑧 ≠ ∅))
2019simprbi 495 . . . . . 6 (𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅} → 𝑧 ≠ ∅)
2120rgen 3053 . . . . 5 𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝑧 ≠ ∅
2217, 21jctil 518 . . . 4 (∀𝑧𝑣𝑤𝑣 𝜑 → (∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝑧 ≠ ∅ ∧ ∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}∀𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜑))
2319biimpri 227 . . . . . . . 8 ((𝑧𝑣𝑧 ≠ ∅) → 𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅})
2423imim1i 63 . . . . . . 7 ((𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅} → 𝜓) → ((𝑧𝑣𝑧 ≠ ∅) → 𝜓))
2524expd 414 . . . . . 6 ((𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅} → 𝜓) → (𝑧𝑣 → (𝑧 ≠ ∅ → 𝜓)))
2625ralimi2 3068 . . . . 5 (∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜓 → ∀𝑧𝑣 (𝑧 ≠ ∅ → 𝜓))
2726eximi 1830 . . . 4 (∃𝑦𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜓 → ∃𝑦𝑧𝑣 (𝑧 ≠ ∅ → 𝜓))
2822, 27imim12i 62 . . 3 (((∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝑧 ≠ ∅ ∧ ∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}∀𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜑) → ∃𝑦𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜓) → (∀𝑧𝑣𝑤𝑣 𝜑 → ∃𝑦𝑧𝑣 (𝑧 ≠ ∅ → 𝜓)))
2911, 28sylg 1818 . 2 (∀𝑥((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 𝜑) → ∃𝑦𝑧𝑥 𝜓) → ∀𝑣(∀𝑧𝑣𝑤𝑣 𝜑 → ∃𝑦𝑧𝑣 (𝑧 ≠ ∅ → 𝜓)))
30 raleq 3312 . . . . 5 (𝑣 = 𝑥 → (∀𝑤𝑣 𝜑 ↔ ∀𝑤𝑥 𝜑))
3130raleqbi1dv 3323 . . . 4 (𝑣 = 𝑥 → (∀𝑧𝑣𝑤𝑣 𝜑 ↔ ∀𝑧𝑥𝑤𝑥 𝜑))
32 raleq 3312 . . . . 5 (𝑣 = 𝑥 → (∀𝑧𝑣 (𝑧 ≠ ∅ → 𝜓) ↔ ∀𝑧𝑥 (𝑧 ≠ ∅ → 𝜓)))
3332exbidv 1917 . . . 4 (𝑣 = 𝑥 → (∃𝑦𝑧𝑣 (𝑧 ≠ ∅ → 𝜓) ↔ ∃𝑦𝑧𝑥 (𝑧 ≠ ∅ → 𝜓)))
3431, 33imbi12d 343 . . 3 (𝑣 = 𝑥 → ((∀𝑧𝑣𝑤𝑣 𝜑 → ∃𝑦𝑧𝑣 (𝑧 ≠ ∅ → 𝜓)) ↔ (∀𝑧𝑥𝑤𝑥 𝜑 → ∃𝑦𝑧𝑥 (𝑧 ≠ ∅ → 𝜓))))
3534cbvalvw 2032 . 2 (∀𝑣(∀𝑧𝑣𝑤𝑣 𝜑 → ∃𝑦𝑧𝑣 (𝑧 ≠ ∅ → 𝜓)) ↔ ∀𝑥(∀𝑧𝑥𝑤𝑥 𝜑 → ∃𝑦𝑧𝑥 (𝑧 ≠ ∅ → 𝜓)))
3629, 35sylib 217 1 (∀𝑥((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 𝜑) → ∃𝑦𝑧𝑥 𝜓) → ∀𝑥(∀𝑧𝑥𝑤𝑥 𝜑 → ∃𝑦𝑧𝑥 (𝑧 ≠ ∅ → 𝜓)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  wal 1532   = wceq 1534  wex 1774  wcel 2099  wne 2930  wral 3051  {crab 3419  c0 4325
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697  ax-sep 5304
This theorem depends on definitions:  df-bi 206  df-an 395  df-3an 1086  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-ne 2931  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3464  df-in 3954  df-ss 3964
This theorem is referenced by:  kmlem13  10205
  Copyright terms: Public domain W3C validator