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

Theorem kmlem3 9166
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 3724 . . . 4 (𝑧 (𝑥 ∖ {𝑧})) = {𝑣𝑧 ∣ ¬ 𝑣 (𝑥 ∖ {𝑧})}
2 dfnul3 4061 . . . . . 6 ∅ = {𝑣𝑧 ∣ ¬ 𝑣𝑧}
32uneq2i 3907 . . . . 5 ({𝑣𝑧 ∣ ¬ 𝑣 (𝑥 ∖ {𝑧})} ∪ ∅) = ({𝑣𝑧 ∣ ¬ 𝑣 (𝑥 ∖ {𝑧})} ∪ {𝑣𝑧 ∣ ¬ 𝑣𝑧})
4 un0 4110 . . . . 5 ({𝑣𝑧 ∣ ¬ 𝑣 (𝑥 ∖ {𝑧})} ∪ ∅) = {𝑣𝑧 ∣ ¬ 𝑣 (𝑥 ∖ {𝑧})}
5 unrab 4041 . . . . 5 ({𝑣𝑧 ∣ ¬ 𝑣 (𝑥 ∖ {𝑧})} ∪ {𝑣𝑧 ∣ ¬ 𝑣𝑧}) = {𝑣𝑧 ∣ (¬ 𝑣 (𝑥 ∖ {𝑧}) ∨ ¬ 𝑣𝑧)}
63, 4, 53eqtr3i 2790 . . . 4 {𝑣𝑧 ∣ ¬ 𝑣 (𝑥 ∖ {𝑧})} = {𝑣𝑧 ∣ (¬ 𝑣 (𝑥 ∖ {𝑧}) ∨ ¬ 𝑣𝑧)}
7 ianor 510 . . . . . 6 (¬ (𝑣 (𝑥 ∖ {𝑧}) ∧ 𝑣𝑧) ↔ (¬ 𝑣 (𝑥 ∖ {𝑧}) ∨ ¬ 𝑣𝑧))
8 eluni 4591 . . . . . . . . 9 (𝑣 (𝑥 ∖ {𝑧}) ↔ ∃𝑤(𝑣𝑤𝑤 ∈ (𝑥 ∖ {𝑧})))
98anbi1i 733 . . . . . . . 8 ((𝑣 (𝑥 ∖ {𝑧}) ∧ 𝑣𝑧) ↔ (∃𝑤(𝑣𝑤𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣𝑧))
10 df-rex 3056 . . . . . . . . 9 (∃𝑤𝑥 ¬ (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤)) ↔ ∃𝑤(𝑤𝑥 ∧ ¬ (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤))))
11 elin 3939 . . . . . . . . . . . . . 14 (𝑣 ∈ (𝑧𝑤) ↔ (𝑣𝑧𝑣𝑤))
1211anbi2i 732 . . . . . . . . . . . . 13 ((𝑧𝑤𝑣 ∈ (𝑧𝑤)) ↔ (𝑧𝑤 ∧ (𝑣𝑧𝑣𝑤)))
13 df-an 385 . . . . . . . . . . . . 13 ((𝑧𝑤𝑣 ∈ (𝑧𝑤)) ↔ ¬ (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤)))
1412, 13bitr3i 266 . . . . . . . . . . . 12 ((𝑧𝑤 ∧ (𝑣𝑧𝑣𝑤)) ↔ ¬ (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤)))
1514anbi2i 732 . . . . . . . . . . 11 ((𝑤𝑥 ∧ (𝑧𝑤 ∧ (𝑣𝑧𝑣𝑤))) ↔ (𝑤𝑥 ∧ ¬ (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤))))
16 eldifsn 4462 . . . . . . . . . . . . . . 15 (𝑤 ∈ (𝑥 ∖ {𝑧}) ↔ (𝑤𝑥𝑤𝑧))
17 necom 2985 . . . . . . . . . . . . . . . 16 (𝑤𝑧𝑧𝑤)
1817anbi2i 732 . . . . . . . . . . . . . . 15 ((𝑤𝑥𝑤𝑧) ↔ (𝑤𝑥𝑧𝑤))
1916, 18bitri 264 . . . . . . . . . . . . . 14 (𝑤 ∈ (𝑥 ∖ {𝑧}) ↔ (𝑤𝑥𝑧𝑤))
2019anbi2i 732 . . . . . . . . . . . . 13 (((𝑣𝑤𝑣𝑧) ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ↔ ((𝑣𝑤𝑣𝑧) ∧ (𝑤𝑥𝑧𝑤)))
21 ancom 465 . . . . . . . . . . . . . 14 ((𝑣𝑤𝑣𝑧) ↔ (𝑣𝑧𝑣𝑤))
2221anbi2ci 734 . . . . . . . . . . . . 13 (((𝑣𝑤𝑣𝑧) ∧ (𝑤𝑥𝑧𝑤)) ↔ ((𝑤𝑥𝑧𝑤) ∧ (𝑣𝑧𝑣𝑤)))
23 anass 684 . . . . . . . . . . . . 13 (((𝑤𝑥𝑧𝑤) ∧ (𝑣𝑧𝑣𝑤)) ↔ (𝑤𝑥 ∧ (𝑧𝑤 ∧ (𝑣𝑧𝑣𝑤))))
2420, 22, 233bitri 286 . . . . . . . . . . . 12 (((𝑣𝑤𝑣𝑧) ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ↔ (𝑤𝑥 ∧ (𝑧𝑤 ∧ (𝑣𝑧𝑣𝑤))))
25 an32 874 . . . . . . . . . . . 12 (((𝑣𝑤𝑣𝑧) ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ↔ ((𝑣𝑤𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣𝑧))
2624, 25bitr3i 266 . . . . . . . . . . 11 ((𝑤𝑥 ∧ (𝑧𝑤 ∧ (𝑣𝑧𝑣𝑤))) ↔ ((𝑣𝑤𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣𝑧))
2715, 26bitr3i 266 . . . . . . . . . 10 ((𝑤𝑥 ∧ ¬ (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤))) ↔ ((𝑣𝑤𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣𝑧))
2827exbii 1923 . . . . . . . . 9 (∃𝑤(𝑤𝑥 ∧ ¬ (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤))) ↔ ∃𝑤((𝑣𝑤𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣𝑧))
29 19.41v 2026 . . . . . . . . 9 (∃𝑤((𝑣𝑤𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣𝑧) ↔ (∃𝑤(𝑣𝑤𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣𝑧))
3010, 28, 293bitri 286 . . . . . . . 8 (∃𝑤𝑥 ¬ (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤)) ↔ (∃𝑤(𝑣𝑤𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣𝑧))
31 rexnal 3133 . . . . . . . 8 (∃𝑤𝑥 ¬ (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤)) ↔ ¬ ∀𝑤𝑥 (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤)))
329, 30, 313bitr2ri 289 . . . . . . 7 (¬ ∀𝑤𝑥 (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤)) ↔ (𝑣 (𝑥 ∖ {𝑧}) ∧ 𝑣𝑧))
3332con1bii 345 . . . . . 6 (¬ (𝑣 (𝑥 ∖ {𝑧}) ∧ 𝑣𝑧) ↔ ∀𝑤𝑥 (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤)))
347, 33bitr3i 266 . . . . 5 ((¬ 𝑣 (𝑥 ∖ {𝑧}) ∨ ¬ 𝑣𝑧) ↔ ∀𝑤𝑥 (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤)))
3534rabbii 3325 . . . 4 {𝑣𝑧 ∣ (¬ 𝑣 (𝑥 ∖ {𝑧}) ∨ ¬ 𝑣𝑧)} = {𝑣𝑧 ∣ ∀𝑤𝑥 (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤))}
361, 6, 353eqtri 2786 . . 3 (𝑧 (𝑥 ∖ {𝑧})) = {𝑣𝑧 ∣ ∀𝑤𝑥 (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤))}
3736neeq1i 2996 . 2 ((𝑧 (𝑥 ∖ {𝑧})) ≠ ∅ ↔ {𝑣𝑧 ∣ ∀𝑤𝑥 (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤))} ≠ ∅)
38 rabn0 4101 . 2 ({𝑣𝑧 ∣ ∀𝑤𝑥 (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤))} ≠ ∅ ↔ ∃𝑣𝑧𝑤𝑥 (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤)))
3937, 38bitri 264 1 ((𝑧 (𝑥 ∖ {𝑧})) ≠ ∅ ↔ ∃𝑣𝑧𝑤𝑥 (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383  wex 1853  wcel 2139  wne 2932  wral 3050  wrex 3051  {crab 3054  cdif 3712  cun 3713  cin 3714  c0 4058  {csn 4321   cuni 4588
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-nul 4059  df-sn 4322  df-uni 4589
This theorem is referenced by:  kmlem13  9176
  Copyright terms: Public domain W3C validator