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

Theorem kmlem3 9566
Description: Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. The right-hand side is part of the hypothesis of 4. (Contributed by NM, 25-Mar-2004.)
Assertion
Ref Expression
kmlem3 ((𝑧 (𝑥 ∖ {𝑧})) ≠ ∅ ↔ ∃𝑣𝑧𝑤𝑥 (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤)))
Distinct variable group:   𝑥,𝑣,𝑤,𝑧

Proof of Theorem kmlem3
StepHypRef Expression
1 dfdif2 3942 . . . 4 (𝑧 (𝑥 ∖ {𝑧})) = {𝑣𝑧 ∣ ¬ 𝑣 (𝑥 ∖ {𝑧})}
2 dfnul3 4292 . . . . . 6 ∅ = {𝑣𝑧 ∣ ¬ 𝑣𝑧}
32uneq2i 4133 . . . . 5 ({𝑣𝑧 ∣ ¬ 𝑣 (𝑥 ∖ {𝑧})} ∪ ∅) = ({𝑣𝑧 ∣ ¬ 𝑣 (𝑥 ∖ {𝑧})} ∪ {𝑣𝑧 ∣ ¬ 𝑣𝑧})
4 un0 4341 . . . . 5 ({𝑣𝑧 ∣ ¬ 𝑣 (𝑥 ∖ {𝑧})} ∪ ∅) = {𝑣𝑧 ∣ ¬ 𝑣 (𝑥 ∖ {𝑧})}
5 unrab 4271 . . . . 5 ({𝑣𝑧 ∣ ¬ 𝑣 (𝑥 ∖ {𝑧})} ∪ {𝑣𝑧 ∣ ¬ 𝑣𝑧}) = {𝑣𝑧 ∣ (¬ 𝑣 (𝑥 ∖ {𝑧}) ∨ ¬ 𝑣𝑧)}
63, 4, 53eqtr3i 2849 . . . 4 {𝑣𝑧 ∣ ¬ 𝑣 (𝑥 ∖ {𝑧})} = {𝑣𝑧 ∣ (¬ 𝑣 (𝑥 ∖ {𝑧}) ∨ ¬ 𝑣𝑧)}
7 ianor 975 . . . . . 6 (¬ (𝑣 (𝑥 ∖ {𝑧}) ∧ 𝑣𝑧) ↔ (¬ 𝑣 (𝑥 ∖ {𝑧}) ∨ ¬ 𝑣𝑧))
8 eluni 4833 . . . . . . . . 9 (𝑣 (𝑥 ∖ {𝑧}) ↔ ∃𝑤(𝑣𝑤𝑤 ∈ (𝑥 ∖ {𝑧})))
98anbi1i 623 . . . . . . . 8 ((𝑣 (𝑥 ∖ {𝑧}) ∧ 𝑣𝑧) ↔ (∃𝑤(𝑣𝑤𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣𝑧))
10 df-rex 3141 . . . . . . . . 9 (∃𝑤𝑥 ¬ (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤)) ↔ ∃𝑤(𝑤𝑥 ∧ ¬ (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤))))
11 elin 4166 . . . . . . . . . . . . . 14 (𝑣 ∈ (𝑧𝑤) ↔ (𝑣𝑧𝑣𝑤))
1211anbi2i 622 . . . . . . . . . . . . 13 ((𝑧𝑤𝑣 ∈ (𝑧𝑤)) ↔ (𝑧𝑤 ∧ (𝑣𝑧𝑣𝑤)))
13 df-an 397 . . . . . . . . . . . . 13 ((𝑧𝑤𝑣 ∈ (𝑧𝑤)) ↔ ¬ (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤)))
1412, 13bitr3i 278 . . . . . . . . . . . 12 ((𝑧𝑤 ∧ (𝑣𝑧𝑣𝑤)) ↔ ¬ (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤)))
1514anbi2i 622 . . . . . . . . . . 11 ((𝑤𝑥 ∧ (𝑧𝑤 ∧ (𝑣𝑧𝑣𝑤))) ↔ (𝑤𝑥 ∧ ¬ (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤))))
16 eldifsn 4711 . . . . . . . . . . . . . . 15 (𝑤 ∈ (𝑥 ∖ {𝑧}) ↔ (𝑤𝑥𝑤𝑧))
17 necom 3066 . . . . . . . . . . . . . . . 16 (𝑤𝑧𝑧𝑤)
1817anbi2i 622 . . . . . . . . . . . . . . 15 ((𝑤𝑥𝑤𝑧) ↔ (𝑤𝑥𝑧𝑤))
1916, 18bitri 276 . . . . . . . . . . . . . 14 (𝑤 ∈ (𝑥 ∖ {𝑧}) ↔ (𝑤𝑥𝑧𝑤))
2019anbi2i 622 . . . . . . . . . . . . 13 (((𝑣𝑤𝑣𝑧) ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ↔ ((𝑣𝑤𝑣𝑧) ∧ (𝑤𝑥𝑧𝑤)))
21 ancom 461 . . . . . . . . . . . . . 14 ((𝑣𝑤𝑣𝑧) ↔ (𝑣𝑧𝑣𝑤))
2221anbi2ci 624 . . . . . . . . . . . . 13 (((𝑣𝑤𝑣𝑧) ∧ (𝑤𝑥𝑧𝑤)) ↔ ((𝑤𝑥𝑧𝑤) ∧ (𝑣𝑧𝑣𝑤)))
23 anass 469 . . . . . . . . . . . . 13 (((𝑤𝑥𝑧𝑤) ∧ (𝑣𝑧𝑣𝑤)) ↔ (𝑤𝑥 ∧ (𝑧𝑤 ∧ (𝑣𝑧𝑣𝑤))))
2420, 22, 233bitri 298 . . . . . . . . . . . 12 (((𝑣𝑤𝑣𝑧) ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ↔ (𝑤𝑥 ∧ (𝑧𝑤 ∧ (𝑣𝑧𝑣𝑤))))
25 an32 642 . . . . . . . . . . . 12 (((𝑣𝑤𝑣𝑧) ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ↔ ((𝑣𝑤𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣𝑧))
2624, 25bitr3i 278 . . . . . . . . . . 11 ((𝑤𝑥 ∧ (𝑧𝑤 ∧ (𝑣𝑧𝑣𝑤))) ↔ ((𝑣𝑤𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣𝑧))
2715, 26bitr3i 278 . . . . . . . . . 10 ((𝑤𝑥 ∧ ¬ (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤))) ↔ ((𝑣𝑤𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣𝑧))
2827exbii 1839 . . . . . . . . 9 (∃𝑤(𝑤𝑥 ∧ ¬ (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤))) ↔ ∃𝑤((𝑣𝑤𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣𝑧))
29 19.41v 1941 . . . . . . . . 9 (∃𝑤((𝑣𝑤𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣𝑧) ↔ (∃𝑤(𝑣𝑤𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣𝑧))
3010, 28, 293bitri 298 . . . . . . . 8 (∃𝑤𝑥 ¬ (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤)) ↔ (∃𝑤(𝑣𝑤𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣𝑧))
31 rexnal 3235 . . . . . . . 8 (∃𝑤𝑥 ¬ (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤)) ↔ ¬ ∀𝑤𝑥 (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤)))
329, 30, 313bitr2ri 301 . . . . . . 7 (¬ ∀𝑤𝑥 (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤)) ↔ (𝑣 (𝑥 ∖ {𝑧}) ∧ 𝑣𝑧))
3332con1bii 358 . . . . . 6 (¬ (𝑣 (𝑥 ∖ {𝑧}) ∧ 𝑣𝑧) ↔ ∀𝑤𝑥 (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤)))
347, 33bitr3i 278 . . . . 5 ((¬ 𝑣 (𝑥 ∖ {𝑧}) ∨ ¬ 𝑣𝑧) ↔ ∀𝑤𝑥 (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤)))
3534rabbii 3471 . . . 4 {𝑣𝑧 ∣ (¬ 𝑣 (𝑥 ∖ {𝑧}) ∨ ¬ 𝑣𝑧)} = {𝑣𝑧 ∣ ∀𝑤𝑥 (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤))}
361, 6, 353eqtri 2845 . . 3 (𝑧 (𝑥 ∖ {𝑧})) = {𝑣𝑧 ∣ ∀𝑤𝑥 (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤))}
3736neeq1i 3077 . 2 ((𝑧 (𝑥 ∖ {𝑧})) ≠ ∅ ↔ {𝑣𝑧 ∣ ∀𝑤𝑥 (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤))} ≠ ∅)
38 rabn0 4336 . 2 ({𝑣𝑧 ∣ ∀𝑤𝑥 (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤))} ≠ ∅ ↔ ∃𝑣𝑧𝑤𝑥 (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤)))
3937, 38bitri 276 1 ((𝑧 (𝑥 ∖ {𝑧})) ≠ ∅ ↔ ∃𝑣𝑧𝑤𝑥 (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  wo 841  wex 1771  wcel 2105  wne 3013  wral 3135  wrex 3136  {crab 3139  cdif 3930  cun 3931  cin 3932  c0 4288  {csn 4557   cuni 4830
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-nul 4289  df-sn 4558  df-uni 4831
This theorem is referenced by:  kmlem13  9576
  Copyright terms: Public domain W3C validator