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

Theorem kmlem1 8916
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 3189 . . . . . 6 𝑣 ∈ V
21rabex 4773 . . . . 5 {𝑢𝑣𝑢 ≠ ∅} ∈ V
3 raleq 3127 . . . . . . 7 (𝑥 = {𝑢𝑣𝑢 ≠ ∅} → (∀𝑧𝑥 𝑧 ≠ ∅ ↔ ∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝑧 ≠ ∅))
4 raleq 3127 . . . . . . . 8 (𝑥 = {𝑢𝑣𝑢 ≠ ∅} → (∀𝑤𝑥 𝜑 ↔ ∀𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜑))
54raleqbi1dv 3135 . . . . . . 7 (𝑥 = {𝑢𝑣𝑢 ≠ ∅} → (∀𝑧𝑥𝑤𝑥 𝜑 ↔ ∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}∀𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜑))
63, 5anbi12d 746 . . . . . 6 (𝑥 = {𝑢𝑣𝑢 ≠ ∅} → ((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 𝜑) ↔ (∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝑧 ≠ ∅ ∧ ∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}∀𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜑)))
7 raleq 3127 . . . . . . 7 (𝑥 = {𝑢𝑣𝑢 ≠ ∅} → (∀𝑧𝑥 𝜓 ↔ ∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜓))
87exbidv 1847 . . . . . 6 (𝑥 = {𝑢𝑣𝑢 ≠ ∅} → (∃𝑦𝑧𝑥 𝜓 ↔ ∃𝑦𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜓))
96, 8imbi12d 334 . . . . 5 (𝑥 = {𝑢𝑣𝑢 ≠ ∅} → (((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 𝜑) → ∃𝑦𝑧𝑥 𝜓) ↔ ((∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝑧 ≠ ∅ ∧ ∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}∀𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜑) → ∃𝑦𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜓)))
102, 9spcv 3285 . . . 4 (∀𝑥((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 𝜑) → ∃𝑦𝑧𝑥 𝜓) → ((∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝑧 ≠ ∅ ∧ ∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}∀𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜑) → ∃𝑦𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜓))
1110alrimiv 1852 . . 3 (∀𝑥((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 𝜑) → ∃𝑦𝑧𝑥 𝜓) → ∀𝑣((∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝑧 ≠ ∅ ∧ ∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}∀𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜑) → ∃𝑦𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜓))
12 elrabi 3342 . . . . . . 7 (𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅} → 𝑧𝑣)
13 elrabi 3342 . . . . . . . . 9 (𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅} → 𝑤𝑣)
1413imim1i 63 . . . . . . . 8 ((𝑤𝑣𝜑) → (𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅} → 𝜑))
1514ralimi2 2944 . . . . . . 7 (∀𝑤𝑣 𝜑 → ∀𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜑)
1612, 15imim12i 62 . . . . . 6 ((𝑧𝑣 → ∀𝑤𝑣 𝜑) → (𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅} → ∀𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜑))
1716ralimi2 2944 . . . . 5 (∀𝑧𝑣𝑤𝑣 𝜑 → ∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}∀𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜑)
18 neeq1 2852 . . . . . . . 8 (𝑢 = 𝑧 → (𝑢 ≠ ∅ ↔ 𝑧 ≠ ∅))
1918elrab 3346 . . . . . . 7 (𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅} ↔ (𝑧𝑣𝑧 ≠ ∅))
2019simprbi 480 . . . . . 6 (𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅} → 𝑧 ≠ ∅)
2120rgen 2917 . . . . 5 𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝑧 ≠ ∅
2217, 21jctil 559 . . . 4 (∀𝑧𝑣𝑤𝑣 𝜑 → (∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝑧 ≠ ∅ ∧ ∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}∀𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜑))
2319biimpri 218 . . . . . . . 8 ((𝑧𝑣𝑧 ≠ ∅) → 𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅})
2423imim1i 63 . . . . . . 7 ((𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅} → 𝜓) → ((𝑧𝑣𝑧 ≠ ∅) → 𝜓))
2524expd 452 . . . . . 6 ((𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅} → 𝜓) → (𝑧𝑣 → (𝑧 ≠ ∅ → 𝜓)))
2625ralimi2 2944 . . . . 5 (∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜓 → ∀𝑧𝑣 (𝑧 ≠ ∅ → 𝜓))
2726eximi 1759 . . . 4 (∃𝑦𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜓 → ∃𝑦𝑧𝑣 (𝑧 ≠ ∅ → 𝜓))
2822, 27imim12i 62 . . 3 (((∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝑧 ≠ ∅ ∧ ∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}∀𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜑) → ∃𝑦𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜓) → (∀𝑧𝑣𝑤𝑣 𝜑 → ∃𝑦𝑧𝑣 (𝑧 ≠ ∅ → 𝜓)))
2911, 28sylg 1747 . 2 (∀𝑥((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 𝜑) → ∃𝑦𝑧𝑥 𝜓) → ∀𝑣(∀𝑧𝑣𝑤𝑣 𝜑 → ∃𝑦𝑧𝑣 (𝑧 ≠ ∅ → 𝜓)))
30 raleq 3127 . . . . 5 (𝑣 = 𝑥 → (∀𝑤𝑣 𝜑 ↔ ∀𝑤𝑥 𝜑))
3130raleqbi1dv 3135 . . . 4 (𝑣 = 𝑥 → (∀𝑧𝑣𝑤𝑣 𝜑 ↔ ∀𝑧𝑥𝑤𝑥 𝜑))
32 raleq 3127 . . . . 5 (𝑣 = 𝑥 → (∀𝑧𝑣 (𝑧 ≠ ∅ → 𝜓) ↔ ∀𝑧𝑥 (𝑧 ≠ ∅ → 𝜓)))
3332exbidv 1847 . . . 4 (𝑣 = 𝑥 → (∃𝑦𝑧𝑣 (𝑧 ≠ ∅ → 𝜓) ↔ ∃𝑦𝑧𝑥 (𝑧 ≠ ∅ → 𝜓)))
3431, 33imbi12d 334 . . 3 (𝑣 = 𝑥 → ((∀𝑧𝑣𝑤𝑣 𝜑 → ∃𝑦𝑧𝑣 (𝑧 ≠ ∅ → 𝜓)) ↔ (∀𝑧𝑥𝑤𝑥 𝜑 → ∃𝑦𝑧𝑥 (𝑧 ≠ ∅ → 𝜓))))
3534cbvalv 2272 . 2 (∀𝑣(∀𝑧𝑣𝑤𝑣 𝜑 → ∃𝑦𝑧𝑣 (𝑧 ≠ ∅ → 𝜓)) ↔ ∀𝑥(∀𝑧𝑥𝑤𝑥 𝜑 → ∃𝑦𝑧𝑥 (𝑧 ≠ ∅ → 𝜓)))
3629, 35sylib 208 1 (∀𝑥((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 𝜑) → ∃𝑦𝑧𝑥 𝜓) → ∀𝑥(∀𝑧𝑥𝑤𝑥 𝜑 → ∃𝑦𝑧𝑥 (𝑧 ≠ ∅ → 𝜓)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wal 1478   = wceq 1480  wex 1701  wcel 1987  wne 2790  wral 2907  {crab 2911  c0 3891
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rab 2916  df-v 3188  df-in 3562  df-ss 3569
This theorem is referenced by:  kmlem13  8928
  Copyright terms: Public domain W3C validator