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

Theorem kmlem8 9572
Description: Lemma for 5-quantifier AC of Kurt Maes, Th. 4 1 <=> 4. (Contributed by NM, 4-Apr-2004.)
Assertion
Ref Expression
kmlem8 ((¬ ∃𝑧𝑢𝑤𝑧 𝜓 → ∃𝑦𝑧𝑢 (𝑧 ≠ ∅ → ∃!𝑤 𝑤 ∈ (𝑧𝑦))) ↔ (∃𝑧𝑢𝑤𝑧 𝜓 ∨ ∃𝑦𝑦𝑢 ∧ ∀𝑧𝑢 ∃!𝑤 𝑤 ∈ (𝑧𝑦))))
Distinct variable group:   𝑦,𝑢,𝑤,𝑧
Allowed substitution hints:   𝜓(𝑦,𝑧,𝑤,𝑢)

Proof of Theorem kmlem8
StepHypRef Expression
1 ralnex 3202 . . . . 5 (∀𝑧𝑢 ¬ ∀𝑤𝑧 𝜓 ↔ ¬ ∃𝑧𝑢𝑤𝑧 𝜓)
2 df-rex 3115 . . . . . . . 8 (∃𝑤𝑧 ¬ 𝜓 ↔ ∃𝑤(𝑤𝑧 ∧ ¬ 𝜓))
3 rexnal 3204 . . . . . . . 8 (∃𝑤𝑧 ¬ 𝜓 ↔ ¬ ∀𝑤𝑧 𝜓)
42, 3bitr3i 280 . . . . . . 7 (∃𝑤(𝑤𝑧 ∧ ¬ 𝜓) ↔ ¬ ∀𝑤𝑧 𝜓)
5 exsimpl 1869 . . . . . . . 8 (∃𝑤(𝑤𝑧 ∧ ¬ 𝜓) → ∃𝑤 𝑤𝑧)
6 n0 4263 . . . . . . . 8 (𝑧 ≠ ∅ ↔ ∃𝑤 𝑤𝑧)
75, 6sylibr 237 . . . . . . 7 (∃𝑤(𝑤𝑧 ∧ ¬ 𝜓) → 𝑧 ≠ ∅)
84, 7sylbir 238 . . . . . 6 (¬ ∀𝑤𝑧 𝜓𝑧 ≠ ∅)
98ralimi 3131 . . . . 5 (∀𝑧𝑢 ¬ ∀𝑤𝑧 𝜓 → ∀𝑧𝑢 𝑧 ≠ ∅)
101, 9sylbir 238 . . . 4 (¬ ∃𝑧𝑢𝑤𝑧 𝜓 → ∀𝑧𝑢 𝑧 ≠ ∅)
11 biimt 364 . . . . . . . . 9 (𝑧 ≠ ∅ → (∃!𝑤 𝑤 ∈ (𝑧𝑦) ↔ (𝑧 ≠ ∅ → ∃!𝑤 𝑤 ∈ (𝑧𝑦))))
1211ralimi 3131 . . . . . . . 8 (∀𝑧𝑢 𝑧 ≠ ∅ → ∀𝑧𝑢 (∃!𝑤 𝑤 ∈ (𝑧𝑦) ↔ (𝑧 ≠ ∅ → ∃!𝑤 𝑤 ∈ (𝑧𝑦))))
13 ralbi 3138 . . . . . . . 8 (∀𝑧𝑢 (∃!𝑤 𝑤 ∈ (𝑧𝑦) ↔ (𝑧 ≠ ∅ → ∃!𝑤 𝑤 ∈ (𝑧𝑦))) → (∀𝑧𝑢 ∃!𝑤 𝑤 ∈ (𝑧𝑦) ↔ ∀𝑧𝑢 (𝑧 ≠ ∅ → ∃!𝑤 𝑤 ∈ (𝑧𝑦))))
1412, 13syl 17 . . . . . . 7 (∀𝑧𝑢 𝑧 ≠ ∅ → (∀𝑧𝑢 ∃!𝑤 𝑤 ∈ (𝑧𝑦) ↔ ∀𝑧𝑢 (𝑧 ≠ ∅ → ∃!𝑤 𝑤 ∈ (𝑧𝑦))))
1514anbi2d 631 . . . . . 6 (∀𝑧𝑢 𝑧 ≠ ∅ → ((¬ 𝑦𝑢 ∧ ∀𝑧𝑢 ∃!𝑤 𝑤 ∈ (𝑧𝑦)) ↔ (¬ 𝑦𝑢 ∧ ∀𝑧𝑢 (𝑧 ≠ ∅ → ∃!𝑤 𝑤 ∈ (𝑧𝑦)))))
1615exbidv 1922 . . . . 5 (∀𝑧𝑢 𝑧 ≠ ∅ → (∃𝑦𝑦𝑢 ∧ ∀𝑧𝑢 ∃!𝑤 𝑤 ∈ (𝑧𝑦)) ↔ ∃𝑦𝑦𝑢 ∧ ∀𝑧𝑢 (𝑧 ≠ ∅ → ∃!𝑤 𝑤 ∈ (𝑧𝑦)))))
17 kmlem2 9566 . . . . 5 (∃𝑦𝑧𝑢 (𝑧 ≠ ∅ → ∃!𝑤 𝑤 ∈ (𝑧𝑦)) ↔ ∃𝑦𝑦𝑢 ∧ ∀𝑧𝑢 (𝑧 ≠ ∅ → ∃!𝑤 𝑤 ∈ (𝑧𝑦))))
1816, 17syl6rbbr 293 . . . 4 (∀𝑧𝑢 𝑧 ≠ ∅ → (∃𝑦𝑧𝑢 (𝑧 ≠ ∅ → ∃!𝑤 𝑤 ∈ (𝑧𝑦)) ↔ ∃𝑦𝑦𝑢 ∧ ∀𝑧𝑢 ∃!𝑤 𝑤 ∈ (𝑧𝑦))))
1910, 18syl 17 . . 3 (¬ ∃𝑧𝑢𝑤𝑧 𝜓 → (∃𝑦𝑧𝑢 (𝑧 ≠ ∅ → ∃!𝑤 𝑤 ∈ (𝑧𝑦)) ↔ ∃𝑦𝑦𝑢 ∧ ∀𝑧𝑢 ∃!𝑤 𝑤 ∈ (𝑧𝑦))))
2019pm5.74i 274 . 2 ((¬ ∃𝑧𝑢𝑤𝑧 𝜓 → ∃𝑦𝑧𝑢 (𝑧 ≠ ∅ → ∃!𝑤 𝑤 ∈ (𝑧𝑦))) ↔ (¬ ∃𝑧𝑢𝑤𝑧 𝜓 → ∃𝑦𝑦𝑢 ∧ ∀𝑧𝑢 ∃!𝑤 𝑤 ∈ (𝑧𝑦))))
21 pm4.64 846 . 2 ((¬ ∃𝑧𝑢𝑤𝑧 𝜓 → ∃𝑦𝑦𝑢 ∧ ∀𝑧𝑢 ∃!𝑤 𝑤 ∈ (𝑧𝑦))) ↔ (∃𝑧𝑢𝑤𝑧 𝜓 ∨ ∃𝑦𝑦𝑢 ∧ ∀𝑧𝑢 ∃!𝑤 𝑤 ∈ (𝑧𝑦))))
2220, 21bitri 278 1 ((¬ ∃𝑧𝑢𝑤𝑧 𝜓 → ∃𝑦𝑧𝑢 (𝑧 ≠ ∅ → ∃!𝑤 𝑤 ∈ (𝑧𝑦))) ↔ (∃𝑧𝑢𝑤𝑧 𝜓 ∨ ∃𝑦𝑦𝑢 ∧ ∀𝑧𝑢 ∃!𝑤 𝑤 ∈ (𝑧𝑦))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wo 844  wex 1781  wcel 2112  ∃!weu 2631  wne 2990  wral 3109  wrex 3110  cin 3883  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-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pr 5298  ax-un 7445
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-ne 2991  df-ral 3114  df-rex 3115  df-rab 3118  df-v 3446  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-sn 4529  df-pr 4531  df-uni 4804
This theorem is referenced by:  dfackm  9581
  Copyright terms: Public domain W3C validator