Theorem kmlem3 10235

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 4048	. . . 4 ⊢ (𝑧 ∖ ∪ (𝑥 ∖ {𝑧})) = {𝑣 ∈ 𝑧 ∣ ¬ 𝑣 ∈ ∪ (𝑥 ∖ {𝑧})}
2		dfnul3 4282	. . . . . 6 ⊢ ∅ = {𝑣 ∈ 𝑧 ∣ ¬ 𝑣 ∈ 𝑧}
3	2	uneq2i 4164	. . . . 5 ⊢ ({𝑣 ∈ 𝑧 ∣ ¬ 𝑣 ∈ ∪ (𝑥 ∖ {𝑧})} ∪ ∅) = ({𝑣 ∈ 𝑧 ∣ ¬ 𝑣 ∈ ∪ (𝑥 ∖ {𝑧})} ∪ {𝑣 ∈ 𝑧 ∣ ¬ 𝑣 ∈ 𝑧})
4		un0 4343	. . . . 5 ⊢ ({𝑣 ∈ 𝑧 ∣ ¬ 𝑣 ∈ ∪ (𝑥 ∖ {𝑧})} ∪ ∅) = {𝑣 ∈ 𝑧 ∣ ¬ 𝑣 ∈ ∪ (𝑥 ∖ {𝑧})}
5		unrab 4260	. . . . 5 ⊢ ({𝑣 ∈ 𝑧 ∣ ¬ 𝑣 ∈ ∪ (𝑥 ∖ {𝑧})} ∪ {𝑣 ∈ 𝑧 ∣ ¬ 𝑣 ∈ 𝑧}) = {𝑣 ∈ 𝑧 ∣ (¬ 𝑣 ∈ ∪ (𝑥 ∖ {𝑧}) ∨ ¬ 𝑣 ∈ 𝑧)}
6	3, 4, 5	3eqtr3i 2791	. . . 4 ⊢ {𝑣 ∈ 𝑧 ∣ ¬ 𝑣 ∈ ∪ (𝑥 ∖ {𝑧})} = {𝑣 ∈ 𝑧 ∣ (¬ 𝑣 ∈ ∪ (𝑥 ∖ {𝑧}) ∨ ¬ 𝑣 ∈ 𝑧)}
7		ianor 997	. . . . . 6 ⊢ (¬ (𝑣 ∈ ∪ (𝑥 ∖ {𝑧}) ∧ 𝑣 ∈ 𝑧) ↔ (¬ 𝑣 ∈ ∪ (𝑥 ∖ {𝑧}) ∨ ¬ 𝑣 ∈ 𝑧))
8		eluni 4869	. . . . . . . . 9 ⊢ (𝑣 ∈ ∪ (𝑥 ∖ {𝑧}) ↔ ∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})))
9	8	anbi1i 636	. . . . . . . 8 ⊢ ((𝑣 ∈ ∪ (𝑥 ∖ {𝑧}) ∧ 𝑣 ∈ 𝑧) ↔ (∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣 ∈ 𝑧))
10		df-rex 3087	. . . . . . . . 9 ⊢ (∃𝑤 ∈ 𝑥 ¬ (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤)) ↔ ∃𝑤(𝑤 ∈ 𝑥 ∧ ¬ (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤))))
11		elin 4093	. . . . . . . . . . . . . 14 ⊢ (𝑣 ∈ (𝑧 ∩ 𝑤) ↔ (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑤))
12	11	anbi2i 635	. . . . . . . . . . . . 13 ⊢ ((𝑧 ≠ 𝑤 ∧ 𝑣 ∈ (𝑧 ∩ 𝑤)) ↔ (𝑧 ≠ 𝑤 ∧ (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑤)))
13		df-an 402	. . . . . . . . . . . . 13 ⊢ ((𝑧 ≠ 𝑤 ∧ 𝑣 ∈ (𝑧 ∩ 𝑤)) ↔ ¬ (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤)))
14	12, 13	bitr3i 280	. . . . . . . . . . . 12 ⊢ ((𝑧 ≠ 𝑤 ∧ (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑤)) ↔ ¬ (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤)))
15	14	anbi2i 635	. . . . . . . . . . 11 ⊢ ((𝑤 ∈ 𝑥 ∧ (𝑧 ≠ 𝑤 ∧ (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑤))) ↔ (𝑤 ∈ 𝑥 ∧ ¬ (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤))))
16		eldifsn 4744	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ (𝑥 ∖ {𝑧}) ↔ (𝑤 ∈ 𝑥 ∧ 𝑤 ≠ 𝑧))
17		necom 3008	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ≠ 𝑧 ↔ 𝑧 ≠ 𝑤)
18	17	anbi2i 635	. . . . . . . . . . . . . . 15 ⊢ ((𝑤 ∈ 𝑥 ∧ 𝑤 ≠ 𝑧) ↔ (𝑤 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤))
19	16, 18	bitri 278	. . . . . . . . . . . . . 14 ⊢ (𝑤 ∈ (𝑥 ∖ {𝑧}) ↔ (𝑤 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤))
20	19	anbi2i 635	. . . . . . . . . . . . 13 ⊢ (((𝑣 ∈ 𝑤 ∧ 𝑣 ∈ 𝑧) ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ↔ ((𝑣 ∈ 𝑤 ∧ 𝑣 ∈ 𝑧) ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤)))
21		ancom 466	. . . . . . . . . . . . . 14 ⊢ ((𝑣 ∈ 𝑤 ∧ 𝑣 ∈ 𝑧) ↔ (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑤))
22	21	anbi2ci 637	. . . . . . . . . . . . 13 ⊢ (((𝑣 ∈ 𝑤 ∧ 𝑣 ∈ 𝑧) ∧ (𝑤 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤)) ↔ ((𝑤 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤) ∧ (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑤)))
23		anass 474	. . . . . . . . . . . . 13 ⊢ (((𝑤 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤) ∧ (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑤)) ↔ (𝑤 ∈ 𝑥 ∧ (𝑧 ≠ 𝑤 ∧ (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑤))))
24	20, 22, 23	3bitri 300	. . . . . . . . . . . 12 ⊢ (((𝑣 ∈ 𝑤 ∧ 𝑣 ∈ 𝑧) ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ↔ (𝑤 ∈ 𝑥 ∧ (𝑧 ≠ 𝑤 ∧ (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑤))))
25		an32 659	. . . . . . . . . . . 12 ⊢ (((𝑣 ∈ 𝑤 ∧ 𝑣 ∈ 𝑧) ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ↔ ((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣 ∈ 𝑧))
26	24, 25	bitr3i 280	. . . . . . . . . . 11 ⊢ ((𝑤 ∈ 𝑥 ∧ (𝑧 ≠ 𝑤 ∧ (𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑤))) ↔ ((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣 ∈ 𝑧))
27	15, 26	bitr3i 280	. . . . . . . . . 10 ⊢ ((𝑤 ∈ 𝑥 ∧ ¬ (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤))) ↔ ((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣 ∈ 𝑧))
28	27	exbii 1880	. . . . . . . . 9 ⊢ (∃𝑤(𝑤 ∈ 𝑥 ∧ ¬ (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤))) ↔ ∃𝑤((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣 ∈ 𝑧))
29		19.41v 1981	. . . . . . . . 9 ⊢ (∃𝑤((𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣 ∈ 𝑧) ↔ (∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣 ∈ 𝑧))
30	10, 28, 29	3bitri 300	. . . . . . . 8 ⊢ (∃𝑤 ∈ 𝑥 ¬ (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤)) ↔ (∃𝑤(𝑣 ∈ 𝑤 ∧ 𝑤 ∈ (𝑥 ∖ {𝑧})) ∧ 𝑣 ∈ 𝑧))
31		rexnal 3114	. . . . . . . 8 ⊢ (∃𝑤 ∈ 𝑥 ¬ (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤)) ↔ ¬ ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤)))
32	9, 30, 31	3bitr2ri 303	. . . . . . 7 ⊢ (¬ ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤)) ↔ (𝑣 ∈ ∪ (𝑥 ∖ {𝑧}) ∧ 𝑣 ∈ 𝑧))
33	32	con1bii 359	. . . . . 6 ⊢ (¬ (𝑣 ∈ ∪ (𝑥 ∖ {𝑧}) ∧ 𝑣 ∈ 𝑧) ↔ ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤)))
34	7, 33	bitr3i 280	. . . . 5 ⊢ ((¬ 𝑣 ∈ ∪ (𝑥 ∖ {𝑧}) ∨ ¬ 𝑣 ∈ 𝑧) ↔ ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤)))
35	34	rabbii 3417	. . . 4 ⊢ {𝑣 ∈ 𝑧 ∣ (¬ 𝑣 ∈ ∪ (𝑥 ∖ {𝑧}) ∨ ¬ 𝑣 ∈ 𝑧)} = {𝑣 ∈ 𝑧 ∣ ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤))}
36	1, 6, 35	3eqtri 2787	. . 3 ⊢ (𝑧 ∖ ∪ (𝑥 ∖ {𝑧})) = {𝑣 ∈ 𝑧 ∣ ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤))}
37	36	neeq1i 3019	. 2 ⊢ ((𝑧 ∖ ∪ (𝑥 ∖ {𝑧})) ≠ ∅ ↔ {𝑣 ∈ 𝑧 ∣ ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤))} ≠ ∅)
38		rabn0 4338	. 2 ⊢ ({𝑣 ∈ 𝑧 ∣ ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤))} ≠ ∅ ↔ ∃𝑣 ∈ 𝑧 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤)))
39	37, 38	bitri 278	1 ⊢ ((𝑧 ∖ ∪ (𝑥 ∖ {𝑧})) ≠ ∅ ↔ ∃𝑣 ∈ 𝑧 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ (𝑧 ∩ 𝑤)))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861  ∃wex 1811   ∈ wcel 2144   ≠ wne 2955  ∀wral 3076  ∃wrex 3086  {crab 3412   ∖ cdif 4045   ∩ cin 4089   ∪ cun 4149  ∅c0 4278  {csn 4584  ∪ cuni 4866

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-sn 4585  df-uni 4867

This theorem is used by:  kmlem13  10245