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

Theorem kmlem3 9645
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 3850 . . . 4 (𝑧 (𝑥 ∖ {𝑧})) = {𝑣𝑧 ∣ ¬ 𝑣 (𝑥 ∖ {𝑧})}
2 dfnul3 4213 . . . . . 6 ∅ = {𝑣𝑧 ∣ ¬ 𝑣𝑧}
32uneq2i 4048 . . . . 5 ({𝑣𝑧 ∣ ¬ 𝑣 (𝑥 ∖ {𝑧})} ∪ ∅) = ({𝑣𝑧 ∣ ¬ 𝑣 (𝑥 ∖ {𝑧})} ∪ {𝑣𝑧 ∣ ¬ 𝑣𝑧})
4 un0 4276 . . . . 5 ({𝑣𝑧 ∣ ¬ 𝑣 (𝑥 ∖ {𝑧})} ∪ ∅) = {𝑣𝑧 ∣ ¬ 𝑣 (𝑥 ∖ {𝑧})}
5 unrab 4192 . . . . 5 ({𝑣𝑧 ∣ ¬ 𝑣 (𝑥 ∖ {𝑧})} ∪ {𝑣𝑧 ∣ ¬ 𝑣𝑧}) = {𝑣𝑧 ∣ (¬ 𝑣 (𝑥 ∖ {𝑧}) ∨ ¬ 𝑣𝑧)}
63, 4, 53eqtr3i 2769 . . . 4 {𝑣𝑧 ∣ ¬ 𝑣 (𝑥 ∖ {𝑧})} = {𝑣𝑧 ∣ (¬ 𝑣 (𝑥 ∖ {𝑧}) ∨ ¬ 𝑣𝑧)}
7 ianor 981 . . . . . 6 (¬ (𝑣 (𝑥 ∖ {𝑧}) ∧ 𝑣𝑧) ↔ (¬ 𝑣 (𝑥 ∖ {𝑧}) ∨ ¬ 𝑣𝑧))
8 eluni 4796 . . . . . . . . 9 (𝑣 (𝑥 ∖ {𝑧}) ↔ ∃𝑤(𝑣𝑤𝑤 ∈ (𝑥 ∖ {𝑧})))
98anbi1i 627 . . . . . . . 8 ((𝑣 (𝑥 ∖ {𝑧}) ∧ 𝑣𝑧) ↔ (∃𝑤(𝑣𝑤𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣𝑧))
10 df-rex 3059 . . . . . . . . 9 (∃𝑤𝑥 ¬ (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤)) ↔ ∃𝑤(𝑤𝑥 ∧ ¬ (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤))))
11 elin 3857 . . . . . . . . . . . . . 14 (𝑣 ∈ (𝑧𝑤) ↔ (𝑣𝑧𝑣𝑤))
1211anbi2i 626 . . . . . . . . . . . . 13 ((𝑧𝑤𝑣 ∈ (𝑧𝑤)) ↔ (𝑧𝑤 ∧ (𝑣𝑧𝑣𝑤)))
13 df-an 400 . . . . . . . . . . . . 13 ((𝑧𝑤𝑣 ∈ (𝑧𝑤)) ↔ ¬ (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤)))
1412, 13bitr3i 280 . . . . . . . . . . . 12 ((𝑧𝑤 ∧ (𝑣𝑧𝑣𝑤)) ↔ ¬ (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤)))
1514anbi2i 626 . . . . . . . . . . 11 ((𝑤𝑥 ∧ (𝑧𝑤 ∧ (𝑣𝑧𝑣𝑤))) ↔ (𝑤𝑥 ∧ ¬ (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤))))
16 eldifsn 4672 . . . . . . . . . . . . . . 15 (𝑤 ∈ (𝑥 ∖ {𝑧}) ↔ (𝑤𝑥𝑤𝑧))
17 necom 2987 . . . . . . . . . . . . . . . 16 (𝑤𝑧𝑧𝑤)
1817anbi2i 626 . . . . . . . . . . . . . . 15 ((𝑤𝑥𝑤𝑧) ↔ (𝑤𝑥𝑧𝑤))
1916, 18bitri 278 . . . . . . . . . . . . . 14 (𝑤 ∈ (𝑥 ∖ {𝑧}) ↔ (𝑤𝑥𝑧𝑤))
2019anbi2i 626 . . . . . . . . . . . . 13 (((𝑣𝑤𝑣𝑧) ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ↔ ((𝑣𝑤𝑣𝑧) ∧ (𝑤𝑥𝑧𝑤)))
21 ancom 464 . . . . . . . . . . . . . 14 ((𝑣𝑤𝑣𝑧) ↔ (𝑣𝑧𝑣𝑤))
2221anbi2ci 628 . . . . . . . . . . . . 13 (((𝑣𝑤𝑣𝑧) ∧ (𝑤𝑥𝑧𝑤)) ↔ ((𝑤𝑥𝑧𝑤) ∧ (𝑣𝑧𝑣𝑤)))
23 anass 472 . . . . . . . . . . . . 13 (((𝑤𝑥𝑧𝑤) ∧ (𝑣𝑧𝑣𝑤)) ↔ (𝑤𝑥 ∧ (𝑧𝑤 ∧ (𝑣𝑧𝑣𝑤))))
2420, 22, 233bitri 300 . . . . . . . . . . . 12 (((𝑣𝑤𝑣𝑧) ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ↔ (𝑤𝑥 ∧ (𝑧𝑤 ∧ (𝑣𝑧𝑣𝑤))))
25 an32 646 . . . . . . . . . . . 12 (((𝑣𝑤𝑣𝑧) ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ↔ ((𝑣𝑤𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣𝑧))
2624, 25bitr3i 280 . . . . . . . . . . 11 ((𝑤𝑥 ∧ (𝑧𝑤 ∧ (𝑣𝑧𝑣𝑤))) ↔ ((𝑣𝑤𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣𝑧))
2715, 26bitr3i 280 . . . . . . . . . 10 ((𝑤𝑥 ∧ ¬ (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤))) ↔ ((𝑣𝑤𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣𝑧))
2827exbii 1854 . . . . . . . . 9 (∃𝑤(𝑤𝑥 ∧ ¬ (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤))) ↔ ∃𝑤((𝑣𝑤𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣𝑧))
29 19.41v 1956 . . . . . . . . 9 (∃𝑤((𝑣𝑤𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣𝑧) ↔ (∃𝑤(𝑣𝑤𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣𝑧))
3010, 28, 293bitri 300 . . . . . . . 8 (∃𝑤𝑥 ¬ (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤)) ↔ (∃𝑤(𝑣𝑤𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣𝑧))
31 rexnal 3150 . . . . . . . 8 (∃𝑤𝑥 ¬ (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤)) ↔ ¬ ∀𝑤𝑥 (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤)))
329, 30, 313bitr2ri 303 . . . . . . 7 (¬ ∀𝑤𝑥 (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤)) ↔ (𝑣 (𝑥 ∖ {𝑧}) ∧ 𝑣𝑧))
3332con1bii 360 . . . . . 6 (¬ (𝑣 (𝑥 ∖ {𝑧}) ∧ 𝑣𝑧) ↔ ∀𝑤𝑥 (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤)))
347, 33bitr3i 280 . . . . 5 ((¬ 𝑣 (𝑥 ∖ {𝑧}) ∨ ¬ 𝑣𝑧) ↔ ∀𝑤𝑥 (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤)))
3534rabbii 3373 . . . 4 {𝑣𝑧 ∣ (¬ 𝑣 (𝑥 ∖ {𝑧}) ∨ ¬ 𝑣𝑧)} = {𝑣𝑧 ∣ ∀𝑤𝑥 (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤))}
361, 6, 353eqtri 2765 . . 3 (𝑧 (𝑥 ∖ {𝑧})) = {𝑣𝑧 ∣ ∀𝑤𝑥 (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤))}
3736neeq1i 2998 . 2 ((𝑧 (𝑥 ∖ {𝑧})) ≠ ∅ ↔ {𝑣𝑧 ∣ ∀𝑤𝑥 (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤))} ≠ ∅)
38 rabn0 4271 . 2 ({𝑣𝑧 ∣ ∀𝑤𝑥 (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤))} ≠ ∅ ↔ ∃𝑣𝑧𝑤𝑥 (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤)))
3937, 38bitri 278 1 ((𝑧 (𝑥 ∖ {𝑧})) ≠ ∅ ↔ ∃𝑣𝑧𝑤𝑥 (𝑧𝑤 → ¬ 𝑣 ∈ (𝑧𝑤)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wo 846  wex 1786  wcel 2113  wne 2934  wral 3053  wrex 3054  {crab 3057  cdif 3838  cun 3839  cin 3840  c0 4209  {csn 4513   cuni 4793
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2161  ax-12 2178  ax-ext 2710
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2074  df-clab 2717  df-cleq 2730  df-clel 2811  df-ne 2935  df-ral 3058  df-rex 3059  df-rab 3062  df-v 3399  df-dif 3844  df-un 3846  df-in 3848  df-nul 4210  df-sn 4514  df-uni 4794
This theorem is referenced by:  kmlem13  9655
  Copyright terms: Public domain W3C validator