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

Theorem kmlem1 8957
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 3198 . . . . . 6 𝑣 ∈ V
21rabex 4804 . . . . 5 {𝑢𝑣𝑢 ≠ ∅} ∈ V
3 raleq 3133 . . . . . . 7 (𝑥 = {𝑢𝑣𝑢 ≠ ∅} → (∀𝑧𝑥 𝑧 ≠ ∅ ↔ ∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝑧 ≠ ∅))
4 raleq 3133 . . . . . . . 8 (𝑥 = {𝑢𝑣𝑢 ≠ ∅} → (∀𝑤𝑥 𝜑 ↔ ∀𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜑))
54raleqbi1dv 3141 . . . . . . 7 (𝑥 = {𝑢𝑣𝑢 ≠ ∅} → (∀𝑧𝑥𝑤𝑥 𝜑 ↔ ∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}∀𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜑))
63, 5anbi12d 746 . . . . . 6 (𝑥 = {𝑢𝑣𝑢 ≠ ∅} → ((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 𝜑) ↔ (∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝑧 ≠ ∅ ∧ ∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}∀𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜑)))
7 raleq 3133 . . . . . . 7 (𝑥 = {𝑢𝑣𝑢 ≠ ∅} → (∀𝑧𝑥 𝜓 ↔ ∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜓))
87exbidv 1848 . . . . . 6 (𝑥 = {𝑢𝑣𝑢 ≠ ∅} → (∃𝑦𝑧𝑥 𝜓 ↔ ∃𝑦𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜓))
96, 8imbi12d 334 . . . . 5 (𝑥 = {𝑢𝑣𝑢 ≠ ∅} → (((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 𝜑) → ∃𝑦𝑧𝑥 𝜓) ↔ ((∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝑧 ≠ ∅ ∧ ∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}∀𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜑) → ∃𝑦𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜓)))
102, 9spcv 3294 . . . 4 (∀𝑥((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 𝜑) → ∃𝑦𝑧𝑥 𝜓) → ((∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝑧 ≠ ∅ ∧ ∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}∀𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜑) → ∃𝑦𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜓))
1110alrimiv 1853 . . 3 (∀𝑥((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 𝜑) → ∃𝑦𝑧𝑥 𝜓) → ∀𝑣((∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝑧 ≠ ∅ ∧ ∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}∀𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜑) → ∃𝑦𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜓))
12 elrabi 3353 . . . . . . 7 (𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅} → 𝑧𝑣)
13 elrabi 3353 . . . . . . . . 9 (𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅} → 𝑤𝑣)
1413imim1i 63 . . . . . . . 8 ((𝑤𝑣𝜑) → (𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅} → 𝜑))
1514ralimi2 2946 . . . . . . 7 (∀𝑤𝑣 𝜑 → ∀𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜑)
1612, 15imim12i 62 . . . . . 6 ((𝑧𝑣 → ∀𝑤𝑣 𝜑) → (𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅} → ∀𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜑))
1716ralimi2 2946 . . . . 5 (∀𝑧𝑣𝑤𝑣 𝜑 → ∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}∀𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜑)
18 neeq1 2853 . . . . . . . 8 (𝑢 = 𝑧 → (𝑢 ≠ ∅ ↔ 𝑧 ≠ ∅))
1918elrab 3357 . . . . . . 7 (𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅} ↔ (𝑧𝑣𝑧 ≠ ∅))
2019simprbi 480 . . . . . 6 (𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅} → 𝑧 ≠ ∅)
2120rgen 2919 . . . . 5 𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝑧 ≠ ∅
2217, 21jctil 559 . . . 4 (∀𝑧𝑣𝑤𝑣 𝜑 → (∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝑧 ≠ ∅ ∧ ∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}∀𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜑))
2319biimpri 218 . . . . . . . 8 ((𝑧𝑣𝑧 ≠ ∅) → 𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅})
2423imim1i 63 . . . . . . 7 ((𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅} → 𝜓) → ((𝑧𝑣𝑧 ≠ ∅) → 𝜓))
2524expd 452 . . . . . 6 ((𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅} → 𝜓) → (𝑧𝑣 → (𝑧 ≠ ∅ → 𝜓)))
2625ralimi2 2946 . . . . 5 (∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜓 → ∀𝑧𝑣 (𝑧 ≠ ∅ → 𝜓))
2726eximi 1760 . . . 4 (∃𝑦𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜓 → ∃𝑦𝑧𝑣 (𝑧 ≠ ∅ → 𝜓))
2822, 27imim12i 62 . . 3 (((∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝑧 ≠ ∅ ∧ ∀𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}∀𝑤 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜑) → ∃𝑦𝑧 ∈ {𝑢𝑣𝑢 ≠ ∅}𝜓) → (∀𝑧𝑣𝑤𝑣 𝜑 → ∃𝑦𝑧𝑣 (𝑧 ≠ ∅ → 𝜓)))
2911, 28sylg 1748 . 2 (∀𝑥((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 𝜑) → ∃𝑦𝑧𝑥 𝜓) → ∀𝑣(∀𝑧𝑣𝑤𝑣 𝜑 → ∃𝑦𝑧𝑣 (𝑧 ≠ ∅ → 𝜓)))
30 raleq 3133 . . . . 5 (𝑣 = 𝑥 → (∀𝑤𝑣 𝜑 ↔ ∀𝑤𝑥 𝜑))
3130raleqbi1dv 3141 . . . 4 (𝑣 = 𝑥 → (∀𝑧𝑣𝑤𝑣 𝜑 ↔ ∀𝑧𝑥𝑤𝑥 𝜑))
32 raleq 3133 . . . . 5 (𝑣 = 𝑥 → (∀𝑧𝑣 (𝑧 ≠ ∅ → 𝜓) ↔ ∀𝑧𝑥 (𝑧 ≠ ∅ → 𝜓)))
3332exbidv 1848 . . . 4 (𝑣 = 𝑥 → (∃𝑦𝑧𝑣 (𝑧 ≠ ∅ → 𝜓) ↔ ∃𝑦𝑧𝑥 (𝑧 ≠ ∅ → 𝜓)))
3431, 33imbi12d 334 . . 3 (𝑣 = 𝑥 → ((∀𝑧𝑣𝑤𝑣 𝜑 → ∃𝑦𝑧𝑣 (𝑧 ≠ ∅ → 𝜓)) ↔ (∀𝑧𝑥𝑤𝑥 𝜑 → ∃𝑦𝑧𝑥 (𝑧 ≠ ∅ → 𝜓))))
3534cbvalv 2271 . 2 (∀𝑣(∀𝑧𝑣𝑤𝑣 𝜑 → ∃𝑦𝑧𝑣 (𝑧 ≠ ∅ → 𝜓)) ↔ ∀𝑥(∀𝑧𝑥𝑤𝑥 𝜑 → ∃𝑦𝑧𝑥 (𝑧 ≠ ∅ → 𝜓)))
3629, 35sylib 208 1 (∀𝑥((∀𝑧𝑥 𝑧 ≠ ∅ ∧ ∀𝑧𝑥𝑤𝑥 𝜑) → ∃𝑦𝑧𝑥 𝜓) → ∀𝑥(∀𝑧𝑥𝑤𝑥 𝜑 → ∃𝑦𝑧𝑥 (𝑧 ≠ ∅ → 𝜓)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wal 1479   = wceq 1481  wex 1702  wcel 1988  wne 2791  wral 2909  {crab 2913  c0 3907
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-ral 2914  df-rab 2918  df-v 3197  df-in 3574  df-ss 3581
This theorem is referenced by:  kmlem13  8969
  Copyright terms: Public domain W3C validator