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

Theorem kmlem3 10191
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 3972 . . . 4 (𝑧 (𝑥 ∖ {𝑧})) = {𝑣𝑧 ∣ ¬ 𝑣 (𝑥 ∖ {𝑧})}
2 dfnul3 4343 . . . . . 6 ∅ = {𝑣𝑧 ∣ ¬ 𝑣𝑧}
32uneq2i 4175 . . . . 5 ({𝑣𝑧 ∣ ¬ 𝑣 (𝑥 ∖ {𝑧})} ∪ ∅) = ({𝑣𝑧 ∣ ¬ 𝑣 (𝑥 ∖ {𝑧})} ∪ {𝑣𝑧 ∣ ¬ 𝑣𝑧})
4 un0 4400 . . . . 5 ({𝑣𝑧 ∣ ¬ 𝑣 (𝑥 ∖ {𝑧})} ∪ ∅) = {𝑣𝑧 ∣ ¬ 𝑣 (𝑥 ∖ {𝑧})}
5 unrab 4321 . . . . 5 ({𝑣𝑧 ∣ ¬ 𝑣 (𝑥 ∖ {𝑧})} ∪ {𝑣𝑧 ∣ ¬ 𝑣𝑧}) = {𝑣𝑧 ∣ (¬ 𝑣 (𝑥 ∖ {𝑧}) ∨ ¬ 𝑣𝑧)}
63, 4, 53eqtr3i 2771 . . . 4 {𝑣𝑧 ∣ ¬ 𝑣 (𝑥 ∖ {𝑧})} = {𝑣𝑧 ∣ (¬ 𝑣 (𝑥 ∖ {𝑧}) ∨ ¬ 𝑣𝑧)}
7 ianor 983 . . . . . 6 (¬ (𝑣 (𝑥 ∖ {𝑧}) ∧ 𝑣𝑧) ↔ (¬ 𝑣 (𝑥 ∖ {𝑧}) ∨ ¬ 𝑣𝑧))
8 eluni 4915 . . . . . . . . 9 (𝑣 (𝑥 ∖ {𝑧}) ↔ ∃𝑤(𝑣𝑤𝑤 ∈ (𝑥 ∖ {𝑧})))
98anbi1i 624 . . . . . . . 8 ((𝑣 (𝑥 ∖ {𝑧}) ∧ 𝑣𝑧) ↔ (∃𝑤(𝑣𝑤𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣𝑧))
10 df-rex 3069 . . . . . . . . 9 (∃𝑤𝑥 ¬ (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤)) ↔ ∃𝑤(𝑤𝑥 ∧ ¬ (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤))))
11 elin 3979 . . . . . . . . . . . . . 14 (𝑣 ∈ (𝑧𝑤) ↔ (𝑣𝑧𝑣𝑤))
1211anbi2i 623 . . . . . . . . . . . . 13 ((𝑧𝑤𝑣 ∈ (𝑧𝑤)) ↔ (𝑧𝑤 ∧ (𝑣𝑧𝑣𝑤)))
13 df-an 396 . . . . . . . . . . . . 13 ((𝑧𝑤𝑣 ∈ (𝑧𝑤)) ↔ ¬ (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤)))
1412, 13bitr3i 277 . . . . . . . . . . . 12 ((𝑧𝑤 ∧ (𝑣𝑧𝑣𝑤)) ↔ ¬ (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤)))
1514anbi2i 623 . . . . . . . . . . 11 ((𝑤𝑥 ∧ (𝑧𝑤 ∧ (𝑣𝑧𝑣𝑤))) ↔ (𝑤𝑥 ∧ ¬ (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤))))
16 eldifsn 4791 . . . . . . . . . . . . . . 15 (𝑤 ∈ (𝑥 ∖ {𝑧}) ↔ (𝑤𝑥𝑤𝑧))
17 necom 2992 . . . . . . . . . . . . . . . 16 (𝑤𝑧𝑧𝑤)
1817anbi2i 623 . . . . . . . . . . . . . . 15 ((𝑤𝑥𝑤𝑧) ↔ (𝑤𝑥𝑧𝑤))
1916, 18bitri 275 . . . . . . . . . . . . . 14 (𝑤 ∈ (𝑥 ∖ {𝑧}) ↔ (𝑤𝑥𝑧𝑤))
2019anbi2i 623 . . . . . . . . . . . . 13 (((𝑣𝑤𝑣𝑧) ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ↔ ((𝑣𝑤𝑣𝑧) ∧ (𝑤𝑥𝑧𝑤)))
21 ancom 460 . . . . . . . . . . . . . 14 ((𝑣𝑤𝑣𝑧) ↔ (𝑣𝑧𝑣𝑤))
2221anbi2ci 625 . . . . . . . . . . . . 13 (((𝑣𝑤𝑣𝑧) ∧ (𝑤𝑥𝑧𝑤)) ↔ ((𝑤𝑥𝑧𝑤) ∧ (𝑣𝑧𝑣𝑤)))
23 anass 468 . . . . . . . . . . . . 13 (((𝑤𝑥𝑧𝑤) ∧ (𝑣𝑧𝑣𝑤)) ↔ (𝑤𝑥 ∧ (𝑧𝑤 ∧ (𝑣𝑧𝑣𝑤))))
2420, 22, 233bitri 297 . . . . . . . . . . . 12 (((𝑣𝑤𝑣𝑧) ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ↔ (𝑤𝑥 ∧ (𝑧𝑤 ∧ (𝑣𝑧𝑣𝑤))))
25 an32 646 . . . . . . . . . . . 12 (((𝑣𝑤𝑣𝑧) ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ↔ ((𝑣𝑤𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣𝑧))
2624, 25bitr3i 277 . . . . . . . . . . 11 ((𝑤𝑥 ∧ (𝑧𝑤 ∧ (𝑣𝑧𝑣𝑤))) ↔ ((𝑣𝑤𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣𝑧))
2715, 26bitr3i 277 . . . . . . . . . 10 ((𝑤𝑥 ∧ ¬ (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤))) ↔ ((𝑣𝑤𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣𝑧))
2827exbii 1845 . . . . . . . . 9 (∃𝑤(𝑤𝑥 ∧ ¬ (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤))) ↔ ∃𝑤((𝑣𝑤𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣𝑧))
29 19.41v 1947 . . . . . . . . 9 (∃𝑤((𝑣𝑤𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣𝑧) ↔ (∃𝑤(𝑣𝑤𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣𝑧))
3010, 28, 293bitri 297 . . . . . . . 8 (∃𝑤𝑥 ¬ (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤)) ↔ (∃𝑤(𝑣𝑤𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣𝑧))
31 rexnal 3098 . . . . . . . 8 (∃𝑤𝑥 ¬ (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤)) ↔ ¬ ∀𝑤𝑥 (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤)))
329, 30, 313bitr2ri 300 . . . . . . 7 (¬ ∀𝑤𝑥 (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤)) ↔ (𝑣 (𝑥 ∖ {𝑧}) ∧ 𝑣𝑧))
3332con1bii 356 . . . . . 6 (¬ (𝑣 (𝑥 ∖ {𝑧}) ∧ 𝑣𝑧) ↔ ∀𝑤𝑥 (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤)))
347, 33bitr3i 277 . . . . 5 ((¬ 𝑣 (𝑥 ∖ {𝑧}) ∨ ¬ 𝑣𝑧) ↔ ∀𝑤𝑥 (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤)))
3534rabbii 3439 . . . 4 {𝑣𝑧 ∣ (¬ 𝑣 (𝑥 ∖ {𝑧}) ∨ ¬ 𝑣𝑧)} = {𝑣𝑧 ∣ ∀𝑤𝑥 (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤))}
361, 6, 353eqtri 2767 . . 3 (𝑧 (𝑥 ∖ {𝑧})) = {𝑣𝑧 ∣ ∀𝑤𝑥 (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤))}
3736neeq1i 3003 . 2 ((𝑧 (𝑥 ∖ {𝑧})) ≠ ∅ ↔ {𝑣𝑧 ∣ ∀𝑤𝑥 (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤))} ≠ ∅)
38 rabn0 4395 . 2 ({𝑣𝑧 ∣ ∀𝑤𝑥 (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤))} ≠ ∅ ↔ ∃𝑣𝑧𝑤𝑥 (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤)))
3937, 38bitri 275 1 ((𝑧 (𝑥 ∖ {𝑧})) ≠ ∅ ↔ ∃𝑣𝑧𝑤𝑥 (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 847  wex 1776  wcel 2106  wne 2938  wral 3059  wrex 3068  {crab 3433  cdif 3960  cun 3961  cin 3962  c0 4339  {csn 4631   cuni 4912
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-nul 4340  df-sn 4632  df-uni 4913
This theorem is referenced by:  kmlem13  10201
  Copyright terms: Public domain W3C validator