Theorem kmlem3 9563

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 3890	. . . 4 ⊢ (𝑧 ∖ ∪ (𝑥 ∖ {𝑧})) = {𝑣 ∈ 𝑧 ∣ ¬ 𝑣 ∈ ∪ (𝑥 ∖ {𝑧})}
2		dfnul3 4246	. . . . . 6 ⊢ ∅ = {𝑣 ∈ 𝑧 ∣ ¬ 𝑣 ∈ 𝑧}
3	2	uneq2i 4087	. . . . 5 ⊢ ({𝑣 ∈ 𝑧 ∣ ¬ 𝑣 ∈ ∪ (𝑥 ∖ {𝑧})} ∪ ∅) = ({𝑣 ∈ 𝑧 ∣ ¬ 𝑣 ∈ ∪ (𝑥 ∖ {𝑧})} ∪ {𝑣 ∈ 𝑧 ∣ ¬ 𝑣 ∈ 𝑧})
4		un0 4298	. . . . 5 ⊢ ({𝑣 ∈ 𝑧 ∣ ¬ 𝑣 ∈ ∪ (𝑥 ∖ {𝑧})} ∪ ∅) = {𝑣 ∈ 𝑧 ∣ ¬ 𝑣 ∈ ∪ (𝑥 ∖ {𝑧})}
5		unrab 4226	. . . . 5 ⊢ ({𝑣 ∈ 𝑧 ∣ ¬ 𝑣 ∈ ∪ (𝑥 ∖ {𝑧})} ∪ {𝑣 ∈ 𝑧 ∣ ¬ 𝑣 ∈ 𝑧}) = {𝑣 ∈ 𝑧 ∣ (¬ 𝑣 ∈ ∪ (𝑥 ∖ {𝑧}) ∨ ¬ 𝑣 ∈ 𝑧)}
6	3, 4, 5	3eqtr3i 2829	. . . 4 ⊢ {𝑣 ∈ 𝑧 ∣ ¬ 𝑣 ∈ ∪ (𝑥 ∖ {𝑧})} = {𝑣 ∈ 𝑧 ∣ (¬ 𝑣 ∈ ∪ (𝑥 ∖ {𝑧}) ∨ ¬ 𝑣 ∈ 𝑧)}
7		ianor 979	. . . . . 6 ⊢ (¬ (𝑣 ∈ ∪ (𝑥 ∖ {𝑧}) ∧ 𝑣 ∈ 𝑧) ↔ (¬ 𝑣 ∈ ∪ (𝑥 ∖ {𝑧}) ∨ ¬ 𝑣 ∈ 𝑧))
8		eluni 4803	. . . . . . . . 9 ⊢ (𝑣 ∈ ∪ (𝑥 ∖ {𝑧}) ↔ ∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})))
9	8	anbi1i 626	. . . . . . . 8 ⊢ ((𝑣 ∈ ∪ (𝑥 ∖ {𝑧}) ∧ 𝑣 ∈ 𝑧) ↔ (∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣 ∈ 𝑧))
10		df-rex 3112	. . . . . . . . 9 ⊢ (∃𝑤 ∈ 𝑥 ¬ (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤)) ↔ ∃𝑤(𝑤 ∈ 𝑥 ∧ ¬ (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤))))
11		elin 3897	. . . . . . . . . . . . . 14 ⊢ (𝑣 ∈ (𝑧 ∩ 𝑤) ↔ (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑤))
12	11	anbi2i 625	. . . . . . . . . . . . 13 ⊢ ((𝑧 ≠ 𝑤 ∧ 𝑣 ∈ (𝑧 ∩ 𝑤)) ↔ (𝑧 ≠ 𝑤 ∧ (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑤)))
13		df-an 400	. . . . . . . . . . . . 13 ⊢ ((𝑧 ≠ 𝑤 ∧ 𝑣 ∈ (𝑧 ∩ 𝑤)) ↔ ¬ (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤)))
14	12, 13	bitr3i 280	. . . . . . . . . . . 12 ⊢ ((𝑧 ≠ 𝑤 ∧ (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑤)) ↔ ¬ (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤)))
15	14	anbi2i 625	. . . . . . . . . . 11 ⊢ ((𝑤 ∈ 𝑥 ∧ (𝑧 ≠ 𝑤 ∧ (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑤))) ↔ (𝑤 ∈ 𝑥 ∧ ¬ (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤))))
16		eldifsn 4680	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ (𝑥 ∖ {𝑧}) ↔ (𝑤 ∈ 𝑥 ∧ 𝑤 ≠ 𝑧))
17		necom 3040	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ≠ 𝑧 ↔ 𝑧 ≠ 𝑤)
18	17	anbi2i 625	. . . . . . . . . . . . . . 15 ⊢ ((𝑤 ∈ 𝑥 ∧ 𝑤 ≠ 𝑧) ↔ (𝑤 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤))
19	16, 18	bitri 278	. . . . . . . . . . . . . 14 ⊢ (𝑤 ∈ (𝑥 ∖ {𝑧}) ↔ (𝑤 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤))
20	19	anbi2i 625	. . . . . . . . . . . . 13 ⊢ (((𝑣 ∈ 𝑤 ∧ 𝑣 ∈ 𝑧) ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ↔ ((𝑣 ∈ 𝑤 ∧ 𝑣 ∈ 𝑧) ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤)))
21		ancom 464	. . . . . . . . . . . . . 14 ⊢ ((𝑣 ∈ 𝑤 ∧ 𝑣 ∈ 𝑧) ↔ (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑤))
22	21	anbi2ci 627	. . . . . . . . . . . . 13 ⊢ (((𝑣 ∈ 𝑤 ∧ 𝑣 ∈ 𝑧) ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤)) ↔ ((𝑤 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤) ∧ (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑤)))
23		anass 472	. . . . . . . . . . . . 13 ⊢ (((𝑤 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤) ∧ (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑤)) ↔ (𝑤 ∈ 𝑥 ∧ (𝑧 ≠ 𝑤 ∧ (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑤))))
24	20, 22, 23	3bitri 300	. . . . . . . . . . . 12 ⊢ (((𝑣 ∈ 𝑤 ∧ 𝑣 ∈ 𝑧) ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ↔ (𝑤 ∈ 𝑥 ∧ (𝑧 ≠ 𝑤 ∧ (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑤))))
25		an32 645	. . . . . . . . . . . 12 ⊢ (((𝑣 ∈ 𝑤 ∧ 𝑣 ∈ 𝑧) ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ↔ ((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣 ∈ 𝑧))
26	24, 25	bitr3i 280	. . . . . . . . . . 11 ⊢ ((𝑤 ∈ 𝑥 ∧ (𝑧 ≠ 𝑤 ∧ (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑤))) ↔ ((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣 ∈ 𝑧))
27	15, 26	bitr3i 280	. . . . . . . . . 10 ⊢ ((𝑤 ∈ 𝑥 ∧ ¬ (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤))) ↔ ((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣 ∈ 𝑧))
28	27	exbii 1849	. . . . . . . . 9 ⊢ (∃𝑤(𝑤 ∈ 𝑥 ∧ ¬ (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤))) ↔ ∃𝑤((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣 ∈ 𝑧))
29		19.41v 1950	. . . . . . . . 9 ⊢ (∃𝑤((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣 ∈ 𝑧) ↔ (∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣 ∈ 𝑧))
30	10, 28, 29	3bitri 300	. . . . . . . 8 ⊢ (∃𝑤 ∈ 𝑥 ¬ (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤)) ↔ (∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣 ∈ 𝑧))
31		rexnal 3201	. . . . . . . 8 ⊢ (∃𝑤 ∈ 𝑥 ¬ (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤)) ↔ ¬ ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤)))
32	9, 30, 31	3bitr2ri 303	. . . . . . 7 ⊢ (¬ ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤)) ↔ (𝑣 ∈ ∪ (𝑥 ∖ {𝑧}) ∧ 𝑣 ∈ 𝑧))
33	32	con1bii 360	. . . . . 6 ⊢ (¬ (𝑣 ∈ ∪ (𝑥 ∖ {𝑧}) ∧ 𝑣 ∈ 𝑧) ↔ ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤)))
34	7, 33	bitr3i 280	. . . . 5 ⊢ ((¬ 𝑣 ∈ ∪ (𝑥 ∖ {𝑧}) ∨ ¬ 𝑣 ∈ 𝑧) ↔ ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤)))
35	34	rabbii 3420	. . . 4 ⊢ {𝑣 ∈ 𝑧 ∣ (¬ 𝑣 ∈ ∪ (𝑥 ∖ {𝑧}) ∨ ¬ 𝑣 ∈ 𝑧)} = {𝑣 ∈ 𝑧 ∣ ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤))}
36	1, 6, 35	3eqtri 2825	. . 3 ⊢ (𝑧 ∖ ∪ (𝑥 ∖ {𝑧})) = {𝑣 ∈ 𝑧 ∣ ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤))}
37	36	neeq1i 3051	. 2 ⊢ ((𝑧 ∖ ∪ (𝑥 ∖ {𝑧})) ≠ ∅ ↔ {𝑣 ∈ 𝑧 ∣ ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤))} ≠ ∅)
38		rabn0 4293	. 2 ⊢ ({𝑣 ∈ 𝑧 ∣ ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤))} ≠ ∅ ↔ ∃𝑣 ∈ 𝑧 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤)))
39	37, 38	bitri 278	1 ⊢ ((𝑧 ∖ ∪ (𝑥 ∖ {𝑧})) ≠ ∅ ↔ ∃𝑣 ∈ 𝑧 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844  ∃wex 1781   ∈ wcel 2111   ≠ wne 2987  ∀wral 3106  ∃wrex 3107  {crab 3110   ∖ cdif 3878   ∪ cun 3879   ∩ cin 3880  ∅c0 4243  {csn 4525  ∪ cuni 4800

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-nul 4244  df-sn 4526  df-uni 4801

This theorem is referenced by:  kmlem13  9573