Theorem kmlem4 3583

Description: Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4.

Assertion

Ref	Expression
kmlem4	⊢ ((w ∈ x ∧ ¬ z = w) → ((z ∖ ∪(x ∖ {z})) ∩ w) = ∅)

Proof of Theorem kmlem4

Step	Hyp	Ref	Expression
1		visset 1350	. . . . . 6 ⊢ w ∈ V
2		eleq1 1149	. . . . . . . 8 ⊢ (v = w → (v ∈ x ↔ w ∈ x))
3		cleq2 1110	. . . . . . . . 9 ⊢ (v = w → (z = v ↔ z = w))
4	3	negbid 463	. . . . . . . 8 ⊢ (v = w → (¬ z = v ↔ ¬ z = w))
5	2, 4	anbi12d 476	. . . . . . 7 ⊢ (v = w → ((v ∈ x ∧ ¬ z = v) ↔ (w ∈ x ∧ ¬ z = w)))
6		eleq2 1150	. . . . . . . 8 ⊢ (v = w → (y ∈ v ↔ y ∈ w))
7	6	negbid 463	. . . . . . 7 ⊢ (v = w → (¬ y ∈ v ↔ ¬ y ∈ w))
8	5, 7	imbi12d 474	. . . . . 6 ⊢ (v = w → (((v ∈ x ∧ ¬ z = v) → ¬ y ∈ v) ↔ ((w ∈ x ∧ ¬ z = w) → ¬ y ∈ w)))
9	1, 8	cla4v 1400	. . . . 5 ⊢ (∀v((v ∈ x ∧ ¬ z = v) → ¬ y ∈ v) → ((w ∈ x ∧ ¬ z = w) → ¬ y ∈ w))
10	9	com12 13	. . . 4 ⊢ ((w ∈ x ∧ ¬ z = w) → (∀v((v ∈ x ∧ ¬ z = v) → ¬ y ∈ v) → ¬ y ∈ w))
11		eldif 1496	. . . . 5 ⊢ (y ∈ (z ∖ ∪(x ∖ {z})) ↔ (y ∈ z ∧ ¬ y ∈ ∪(x ∖ {z})))
12		pm3.27 260	. . . . . 6 ⊢ ((y ∈ z ∧ ¬ y ∈ ∪(x ∖ {z})) → ¬ y ∈ ∪(x ∖ {z}))
13		eluni 1922	. . . . . . . 8 ⊢ (y ∈ ∪(x ∖ {z}) ↔ ∃v(y ∈ v ∧ v ∈ (x ∖ {z})))
14	13	negbii 162	. . . . . . 7 ⊢ (¬ y ∈ ∪(x ∖ {z}) ↔ ¬ ∃v(y ∈ v ∧ v ∈ (x ∖ {z})))
15		alnex 716	. . . . . . . 8 ⊢ (∀v ¬ (y ∈ v ∧ v ∈ (x ∖ {z})) ↔ ¬ ∃v(y ∈ v ∧ v ∈ (x ∖ {z})))
16		ianor 253	. . . . . . . . . 10 ⊢ (¬ (y ∈ v ∧ v ∈ (x ∖ {z})) ↔ (¬ y ∈ v ∨ ¬ v ∈ (x ∖ {z})))
17		eldif 1496	. . . . . . . . . . . . . . 15 ⊢ (v ∈ (x ∖ {z}) ↔ (v ∈ x ∧ ¬ v ∈ {z}))
18		elsn 1820	. . . . . . . . . . . . . . . . . 18 ⊢ (v ∈ {z} ↔ v = z)
19		cleqcom 1103	. . . . . . . . . . . . . . . . . 18 ⊢ (v = z ↔ z = v)
20	18, 19	bitr 151	. . . . . . . . . . . . . . . . 17 ⊢ (v ∈ {z} ↔ z = v)
21	20	negbii 162	. . . . . . . . . . . . . . . 16 ⊢ (¬ v ∈ {z} ↔ ¬ z = v)
22	21	anbi2i 367	. . . . . . . . . . . . . . 15 ⊢ ((v ∈ x ∧ ¬ v ∈ {z}) ↔ (v ∈ x ∧ ¬ z = v))
23	17, 22	bitr 151	. . . . . . . . . . . . . 14 ⊢ (v ∈ (x ∖ {z}) ↔ (v ∈ x ∧ ¬ z = v))
24	23	negbii 162	. . . . . . . . . . . . 13 ⊢ (¬ v ∈ (x ∖ {z}) ↔ ¬ (v ∈ x ∧ ¬ z = v))
25		iman 205	. . . . . . . . . . . . 13 ⊢ ((v ∈ x → z = v) ↔ ¬ (v ∈ x ∧ ¬ z = v))
26	24, 25	bitr4 154	. . . . . . . . . . . 12 ⊢ (¬ v ∈ (x ∖ {z}) ↔ (v ∈ x → z = v))
27	26	imbi2i 160	. . . . . . . . . . 11 ⊢ ((y ∈ v → ¬ v ∈ (x ∖ {z})) ↔ (y ∈ v → (v ∈ x → z = v)))
28		imor 204	. . . . . . . . . . 11 ⊢ ((y ∈ v → ¬ v ∈ (x ∖ {z})) ↔ (¬ y ∈ v ∨ ¬ v ∈ (x ∖ {z})))
29		pm4.1 143	. . . . . . . . . . . . 13 ⊢ ((y ∈ v → z = v) ↔ (¬ z = v → ¬ y ∈ v))
30	29	imbi2i 160	. . . . . . . . . . . 12 ⊢ ((v ∈ x → (y ∈ v → z = v)) ↔ (v ∈ x → (¬ z = v → ¬ y ∈ v)))
31		bi2.04 141	. . . . . . . . . . . 12 ⊢ ((y ∈ v → (v ∈ x → z = v)) ↔ (v ∈ x → (y ∈ v → z = v)))
32		impexp 276	. . . . . . . . . . . 12 ⊢ (((v ∈ x ∧ ¬ z = v) → ¬ y ∈ v) ↔ (v ∈ x → (¬ z = v → ¬ y ∈ v)))
33	30, 31, 32	3bitr4 158	. . . . . . . . . . 11 ⊢ ((y ∈ v → (v ∈ x → z = v)) ↔ ((v ∈ x ∧ ¬ z = v) → ¬ y ∈ v))
34	27, 28, 33	3bitr3 156	. . . . . . . . . 10 ⊢ ((¬ y ∈ v ∨ ¬ v ∈ (x ∖ {z})) ↔ ((v ∈ x ∧ ¬ z = v) → ¬ y ∈ v))
35	16, 34	bitr 151	. . . . . . . . 9 ⊢ (¬ (y ∈ v ∧ v ∈ (x ∖ {z})) ↔ ((v ∈ x ∧ ¬ z = v) → ¬ y ∈ v))
36	35	bial 695	. . . . . . . 8 ⊢ (∀v ¬ (y ∈ v ∧ v ∈ (x ∖ {z})) ↔ ∀v((v ∈ x ∧ ¬ z = v) → ¬ y ∈ v))
37	15, 36	bitr3 153	. . . . . . 7 ⊢ (¬ ∃v(y ∈ v ∧ v ∈ (x ∖ {z})) ↔ ∀v((v ∈ x ∧ ¬ z = v) → ¬ y ∈ v))
38	14, 37	bitr 151	. . . . . 6 ⊢ (¬ y ∈ ∪(x ∖ {z}) ↔ ∀v((v ∈ x ∧ ¬ z = v) → ¬ y ∈ v))
39	12, 38	sylib 173	. . . . 5 ⊢ ((y ∈ z ∧ ¬ y ∈ ∪(x ∖ {z})) → ∀v((v ∈ x ∧ ¬ z = v) → ¬ y ∈ v))
40	11, 39	sylbi 174	. . . 4 ⊢ (y ∈ (z ∖ ∪(x ∖ {z})) → ∀v((v ∈ x ∧ ¬ z = v) → ¬ y ∈ v))
41	10, 40	syl5 22	. . 3 ⊢ ((w ∈ x ∧ ¬ z = w) → (y ∈ (z ∖ ∪(x ∖ {z})) → ¬ y ∈ w))
42	41	r19.21aiv 1259	. 2 ⊢ ((w ∈ x ∧ ¬ z = w) → ∀y ∈ (z ∖ ∪(x ∖ {z})) ¬ y ∈ w)
43		disj 1733	. 2 ⊢ (((z ∖ ∪(x ∖ {z})) ∩ w) = ∅ ↔ ∀y ∈ (z ∖ ∪(x ∖ {z})) ¬ y ∈ w)
44	42, 43	sylibr 175	1 ⊢ ((w ∈ x ∧ ¬ z = w) → ((z ∖ ∪(x ∖ {z})) ∩ w) = ∅)

Syntax hints:  ¬ wn 1   → wi 2   ∨ wo 195   ∧ wa 196  ∀wal 672  ∃wex 678   = weq 797   ∈ wel 803   = wceq 1091   ∈ wcel 1092  ∀wral 1201   ∖ cdif 1484   ∩ cin 1486  ∅c0 1707  {csn 1808  ∪cuni 1919

This theorem is referenced by:  kmlem5 3584  kmlem10 3589

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-ral 1205  df-v 1349  df-dif 1489  df-in 1491  df-nul 1708  df-sn 1811  df-uni 1920

metamath.org