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

Theorem kmlem3 9556
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 3922 . . . 4 (𝑧 (𝑥 ∖ {𝑧})) = {𝑣𝑧 ∣ ¬ 𝑣 (𝑥 ∖ {𝑧})}
2 dfnul3 4272 . . . . . 6 ∅ = {𝑣𝑧 ∣ ¬ 𝑣𝑧}
32uneq2i 4115 . . . . 5 ({𝑣𝑧 ∣ ¬ 𝑣 (𝑥 ∖ {𝑧})} ∪ ∅) = ({𝑣𝑧 ∣ ¬ 𝑣 (𝑥 ∖ {𝑧})} ∪ {𝑣𝑧 ∣ ¬ 𝑣𝑧})
4 un0 4320 . . . . 5 ({𝑣𝑧 ∣ ¬ 𝑣 (𝑥 ∖ {𝑧})} ∪ ∅) = {𝑣𝑧 ∣ ¬ 𝑣 (𝑥 ∖ {𝑧})}
5 unrab 4252 . . . . 5 ({𝑣𝑧 ∣ ¬ 𝑣 (𝑥 ∖ {𝑧})} ∪ {𝑣𝑧 ∣ ¬ 𝑣𝑧}) = {𝑣𝑧 ∣ (¬ 𝑣 (𝑥 ∖ {𝑧}) ∨ ¬ 𝑣𝑧)}
63, 4, 53eqtr3i 2851 . . . 4 {𝑣𝑧 ∣ ¬ 𝑣 (𝑥 ∖ {𝑧})} = {𝑣𝑧 ∣ (¬ 𝑣 (𝑥 ∖ {𝑧}) ∨ ¬ 𝑣𝑧)}
7 ianor 978 . . . . . 6 (¬ (𝑣 (𝑥 ∖ {𝑧}) ∧ 𝑣𝑧) ↔ (¬ 𝑣 (𝑥 ∖ {𝑧}) ∨ ¬ 𝑣𝑧))
8 eluni 4817 . . . . . . . . 9 (𝑣 (𝑥 ∖ {𝑧}) ↔ ∃𝑤(𝑣𝑤𝑤 ∈ (𝑥 ∖ {𝑧})))
98anbi1i 625 . . . . . . . 8 ((𝑣 (𝑥 ∖ {𝑧}) ∧ 𝑣𝑧) ↔ (∃𝑤(𝑣𝑤𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣𝑧))
10 df-rex 3131 . . . . . . . . 9 (∃𝑤𝑥 ¬ (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤)) ↔ ∃𝑤(𝑤𝑥 ∧ ¬ (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤))))
11 elin 3929 . . . . . . . . . . . . . 14 (𝑣 ∈ (𝑧𝑤) ↔ (𝑣𝑧𝑣𝑤))
1211anbi2i 624 . . . . . . . . . . . . 13 ((𝑧𝑤𝑣 ∈ (𝑧𝑤)) ↔ (𝑧𝑤 ∧ (𝑣𝑧𝑣𝑤)))
13 df-an 399 . . . . . . . . . . . . 13 ((𝑧𝑤𝑣 ∈ (𝑧𝑤)) ↔ ¬ (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤)))
1412, 13bitr3i 279 . . . . . . . . . . . 12 ((𝑧𝑤 ∧ (𝑣𝑧𝑣𝑤)) ↔ ¬ (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤)))
1514anbi2i 624 . . . . . . . . . . 11 ((𝑤𝑥 ∧ (𝑧𝑤 ∧ (𝑣𝑧𝑣𝑤))) ↔ (𝑤𝑥 ∧ ¬ (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤))))
16 eldifsn 4695 . . . . . . . . . . . . . . 15 (𝑤 ∈ (𝑥 ∖ {𝑧}) ↔ (𝑤𝑥𝑤𝑧))
17 necom 3059 . . . . . . . . . . . . . . . 16 (𝑤𝑧𝑧𝑤)
1817anbi2i 624 . . . . . . . . . . . . . . 15 ((𝑤𝑥𝑤𝑧) ↔ (𝑤𝑥𝑧𝑤))
1916, 18bitri 277 . . . . . . . . . . . . . 14 (𝑤 ∈ (𝑥 ∖ {𝑧}) ↔ (𝑤𝑥𝑧𝑤))
2019anbi2i 624 . . . . . . . . . . . . 13 (((𝑣𝑤𝑣𝑧) ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ↔ ((𝑣𝑤𝑣𝑧) ∧ (𝑤𝑥𝑧𝑤)))
21 ancom 463 . . . . . . . . . . . . . 14 ((𝑣𝑤𝑣𝑧) ↔ (𝑣𝑧𝑣𝑤))
2221anbi2ci 626 . . . . . . . . . . . . 13 (((𝑣𝑤𝑣𝑧) ∧ (𝑤𝑥𝑧𝑤)) ↔ ((𝑤𝑥𝑧𝑤) ∧ (𝑣𝑧𝑣𝑤)))
23 anass 471 . . . . . . . . . . . . 13 (((𝑤𝑥𝑧𝑤) ∧ (𝑣𝑧𝑣𝑤)) ↔ (𝑤𝑥 ∧ (𝑧𝑤 ∧ (𝑣𝑧𝑣𝑤))))
2420, 22, 233bitri 299 . . . . . . . . . . . 12 (((𝑣𝑤𝑣𝑧) ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ↔ (𝑤𝑥 ∧ (𝑧𝑤 ∧ (𝑣𝑧𝑣𝑤))))
25 an32 644 . . . . . . . . . . . 12 (((𝑣𝑤𝑣𝑧) ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ↔ ((𝑣𝑤𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣𝑧))
2624, 25bitr3i 279 . . . . . . . . . . 11 ((𝑤𝑥 ∧ (𝑧𝑤 ∧ (𝑣𝑧𝑣𝑤))) ↔ ((𝑣𝑤𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣𝑧))
2715, 26bitr3i 279 . . . . . . . . . 10 ((𝑤𝑥 ∧ ¬ (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤))) ↔ ((𝑣𝑤𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣𝑧))
2827exbii 1848 . . . . . . . . 9 (∃𝑤(𝑤𝑥 ∧ ¬ (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤))) ↔ ∃𝑤((𝑣𝑤𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣𝑧))
29 19.41v 1950 . . . . . . . . 9 (∃𝑤((𝑣𝑤𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣𝑧) ↔ (∃𝑤(𝑣𝑤𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣𝑧))
3010, 28, 293bitri 299 . . . . . . . 8 (∃𝑤𝑥 ¬ (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤)) ↔ (∃𝑤(𝑣𝑤𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣𝑧))
31 rexnal 3225 . . . . . . . 8 (∃𝑤𝑥 ¬ (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤)) ↔ ¬ ∀𝑤𝑥 (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤)))
329, 30, 313bitr2ri 302 . . . . . . 7 (¬ ∀𝑤𝑥 (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤)) ↔ (𝑣 (𝑥 ∖ {𝑧}) ∧ 𝑣𝑧))
3332con1bii 359 . . . . . 6 (¬ (𝑣 (𝑥 ∖ {𝑧}) ∧ 𝑣𝑧) ↔ ∀𝑤𝑥 (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤)))
347, 33bitr3i 279 . . . . 5 ((¬ 𝑣 (𝑥 ∖ {𝑧}) ∨ ¬ 𝑣𝑧) ↔ ∀𝑤𝑥 (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤)))
3534rabbii 3452 . . . 4 {𝑣𝑧 ∣ (¬ 𝑣 (𝑥 ∖ {𝑧}) ∨ ¬ 𝑣𝑧)} = {𝑣𝑧 ∣ ∀𝑤𝑥 (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤))}
361, 6, 353eqtri 2847 . . 3 (𝑧 (𝑥 ∖ {𝑧})) = {𝑣𝑧 ∣ ∀𝑤𝑥 (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤))}
3736neeq1i 3070 . 2 ((𝑧 (𝑥 ∖ {𝑧})) ≠ ∅ ↔ {𝑣𝑧 ∣ ∀𝑤𝑥 (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤))} ≠ ∅)
38 rabn0 4315 . 2 ({𝑣𝑧 ∣ ∀𝑤𝑥 (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤))} ≠ ∅ ↔ ∃𝑣𝑧𝑤𝑥 (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤)))
3937, 38bitri 277 1 ((𝑧 (𝑥 ∖ {𝑧})) ≠ ∅ ↔ ∃𝑣𝑧𝑤𝑥 (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 208  wa 398  wo 843  wex 1780  wcel 2114  wne 3006  wral 3125  wrex 3126  {crab 3129  cdif 3910  cun 3911  cin 3912  c0 4269  {csn 4543   cuni 4814
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ne 3007  df-ral 3130  df-rex 3131  df-rab 3134  df-v 3475  df-dif 3916  df-un 3918  df-in 3920  df-nul 4270  df-sn 4544  df-uni 4815
This theorem is referenced by:  kmlem13  9566
  Copyright terms: Public domain W3C validator