Theorem kmlem3 10193

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

Step	Hyp	Ref	Expression
1		dfdif2 3960	. . . 4 ⊢ (𝑧 ∖ ∪ (𝑥 ∖ {𝑧})) = {𝑣 ∈ 𝑧 ∣ ¬ 𝑣 ∈ ∪ (𝑥 ∖ {𝑧})}
2		dfnul3 4337	. . . . . 6 ⊢ ∅ = {𝑣 ∈ 𝑧 ∣ ¬ 𝑣 ∈ 𝑧}
3	2	uneq2i 4165	. . . . 5 ⊢ ({𝑣 ∈ 𝑧 ∣ ¬ 𝑣 ∈ ∪ (𝑥 ∖ {𝑧})} ∪ ∅) = ({𝑣 ∈ 𝑧 ∣ ¬ 𝑣 ∈ ∪ (𝑥 ∖ {𝑧})} ∪ {𝑣 ∈ 𝑧 ∣ ¬ 𝑣 ∈ 𝑧})
4		un0 4394	. . . . 5 ⊢ ({𝑣 ∈ 𝑧 ∣ ¬ 𝑣 ∈ ∪ (𝑥 ∖ {𝑧})} ∪ ∅) = {𝑣 ∈ 𝑧 ∣ ¬ 𝑣 ∈ ∪ (𝑥 ∖ {𝑧})}
5		unrab 4315	. . . . 5 ⊢ ({𝑣 ∈ 𝑧 ∣ ¬ 𝑣 ∈ ∪ (𝑥 ∖ {𝑧})} ∪ {𝑣 ∈ 𝑧 ∣ ¬ 𝑣 ∈ 𝑧}) = {𝑣 ∈ 𝑧 ∣ (¬ 𝑣 ∈ ∪ (𝑥 ∖ {𝑧}) ∨ ¬ 𝑣 ∈ 𝑧)}
6	3, 4, 5	3eqtr3i 2773	. . . 4 ⊢ {𝑣 ∈ 𝑧 ∣ ¬ 𝑣 ∈ ∪ (𝑥 ∖ {𝑧})} = {𝑣 ∈ 𝑧 ∣ (¬ 𝑣 ∈ ∪ (𝑥 ∖ {𝑧}) ∨ ¬ 𝑣 ∈ 𝑧)}
7		ianor 984	. . . . . 6 ⊢ (¬ (𝑣 ∈ ∪ (𝑥 ∖ {𝑧}) ∧ 𝑣 ∈ 𝑧) ↔ (¬ 𝑣 ∈ ∪ (𝑥 ∖ {𝑧}) ∨ ¬ 𝑣 ∈ 𝑧))
8		eluni 4910	. . . . . . . . 9 ⊢ (𝑣 ∈ ∪ (𝑥 ∖ {𝑧}) ↔ ∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})))
9	8	anbi1i 624	. . . . . . . 8 ⊢ ((𝑣 ∈ ∪ (𝑥 ∖ {𝑧}) ∧ 𝑣 ∈ 𝑧) ↔ (∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣 ∈ 𝑧))
10		df-rex 3071	. . . . . . . . 9 ⊢ (∃𝑤 ∈ 𝑥 ¬ (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤)) ↔ ∃𝑤(𝑤 ∈ 𝑥 ∧ ¬ (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤))))
11		elin 3967	. . . . . . . . . . . . . 14 ⊢ (𝑣 ∈ (𝑧 ∩ 𝑤) ↔ (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑤))
12	11	anbi2i 623	. . . . . . . . . . . . 13 ⊢ ((𝑧 ≠ 𝑤 ∧ 𝑣 ∈ (𝑧 ∩ 𝑤)) ↔ (𝑧 ≠ 𝑤 ∧ (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑤)))
13		df-an 396	. . . . . . . . . . . . 13 ⊢ ((𝑧 ≠ 𝑤 ∧ 𝑣 ∈ (𝑧 ∩ 𝑤)) ↔ ¬ (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤)))
14	12, 13	bitr3i 277	. . . . . . . . . . . 12 ⊢ ((𝑧 ≠ 𝑤 ∧ (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑤)) ↔ ¬ (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤)))
15	14	anbi2i 623	. . . . . . . . . . 11 ⊢ ((𝑤 ∈ 𝑥 ∧ (𝑧 ≠ 𝑤 ∧ (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑤))) ↔ (𝑤 ∈ 𝑥 ∧ ¬ (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤))))
16		eldifsn 4786	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ (𝑥 ∖ {𝑧}) ↔ (𝑤 ∈ 𝑥 ∧ 𝑤 ≠ 𝑧))
17		necom 2994	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ≠ 𝑧 ↔ 𝑧 ≠ 𝑤)
18	17	anbi2i 623	. . . . . . . . . . . . . . 15 ⊢ ((𝑤 ∈ 𝑥 ∧ 𝑤 ≠ 𝑧) ↔ (𝑤 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤))
19	16, 18	bitri 275	. . . . . . . . . . . . . 14 ⊢ (𝑤 ∈ (𝑥 ∖ {𝑧}) ↔ (𝑤 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤))
20	19	anbi2i 623	. . . . . . . . . . . . 13 ⊢ (((𝑣 ∈ 𝑤 ∧ 𝑣 ∈ 𝑧) ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ↔ ((𝑣 ∈ 𝑤 ∧ 𝑣 ∈ 𝑧) ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤)))
21		ancom 460	. . . . . . . . . . . . . 14 ⊢ ((𝑣 ∈ 𝑤 ∧ 𝑣 ∈ 𝑧) ↔ (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑤))
22	21	anbi2ci 625	. . . . . . . . . . . . 13 ⊢ (((𝑣 ∈ 𝑤 ∧ 𝑣 ∈ 𝑧) ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤)) ↔ ((𝑤 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤) ∧ (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑤)))
23		anass 468	. . . . . . . . . . . . 13 ⊢ (((𝑤 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤) ∧ (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑤)) ↔ (𝑤 ∈ 𝑥 ∧ (𝑧 ≠ 𝑤 ∧ (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑤))))
24	20, 22, 23	3bitri 297	. . . . . . . . . . . 12 ⊢ (((𝑣 ∈ 𝑤 ∧ 𝑣 ∈ 𝑧) ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ↔ (𝑤 ∈ 𝑥 ∧ (𝑧 ≠ 𝑤 ∧ (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑤))))
25		an32 646	. . . . . . . . . . . 12 ⊢ (((𝑣 ∈ 𝑤 ∧ 𝑣 ∈ 𝑧) ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ↔ ((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣 ∈ 𝑧))
26	24, 25	bitr3i 277	. . . . . . . . . . 11 ⊢ ((𝑤 ∈ 𝑥 ∧ (𝑧 ≠ 𝑤 ∧ (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑤))) ↔ ((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣 ∈ 𝑧))
27	15, 26	bitr3i 277	. . . . . . . . . 10 ⊢ ((𝑤 ∈ 𝑥 ∧ ¬ (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤))) ↔ ((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣 ∈ 𝑧))
28	27	exbii 1848	. . . . . . . . 9 ⊢ (∃𝑤(𝑤 ∈ 𝑥 ∧ ¬ (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤))) ↔ ∃𝑤((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣 ∈ 𝑧))
29		19.41v 1949	. . . . . . . . 9 ⊢ (∃𝑤((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣 ∈ 𝑧) ↔ (∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣 ∈ 𝑧))
30	10, 28, 29	3bitri 297	. . . . . . . 8 ⊢ (∃𝑤 ∈ 𝑥 ¬ (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤)) ↔ (∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣 ∈ 𝑧))
31		rexnal 3100	. . . . . . . 8 ⊢ (∃𝑤 ∈ 𝑥 ¬ (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤)) ↔ ¬ ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤)))
32	9, 30, 31	3bitr2ri 300	. . . . . . 7 ⊢ (¬ ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤)) ↔ (𝑣 ∈ ∪ (𝑥 ∖ {𝑧}) ∧ 𝑣 ∈ 𝑧))
33	32	con1bii 356	. . . . . 6 ⊢ (¬ (𝑣 ∈ ∪ (𝑥 ∖ {𝑧}) ∧ 𝑣 ∈ 𝑧) ↔ ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤)))
34	7, 33	bitr3i 277	. . . . 5 ⊢ ((¬ 𝑣 ∈ ∪ (𝑥 ∖ {𝑧}) ∨ ¬ 𝑣 ∈ 𝑧) ↔ ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤)))
35	34	rabbii 3442	. . . 4 ⊢ {𝑣 ∈ 𝑧 ∣ (¬ 𝑣 ∈ ∪ (𝑥 ∖ {𝑧}) ∨ ¬ 𝑣 ∈ 𝑧)} = {𝑣 ∈ 𝑧 ∣ ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤))}
36	1, 6, 35	3eqtri 2769	. . 3 ⊢ (𝑧 ∖ ∪ (𝑥 ∖ {𝑧})) = {𝑣 ∈ 𝑧 ∣ ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤))}
37	36	neeq1i 3005	. 2 ⊢ ((𝑧 ∖ ∪ (𝑥 ∖ {𝑧})) ≠ ∅ ↔ {𝑣 ∈ 𝑧 ∣ ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤))} ≠ ∅)
38		rabn0 4389	. 2 ⊢ ({𝑣 ∈ 𝑧 ∣ ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤))} ≠ ∅ ↔ ∃𝑣 ∈ 𝑧 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤)))
39	37, 38	bitri 275	1 ⊢ ((𝑧 ∖ ∪ (𝑥 ∖ {𝑧})) ≠ ∅ ↔ ∃𝑣 ∈ 𝑧 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 848  ∃wex 1779   ∈ wcel 2108   ≠ wne 2940  ∀wral 3061  ∃wrex 3070  {crab 3436   ∖ cdif 3948   ∪ cun 3949   ∩ cin 3950  ∅c0 4333  {csn 4626  ∪ cuni 4907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-nul 4334  df-sn 4627  df-uni 4908

This theorem is referenced by:  kmlem13  10203