Metamath Proof Explorer

Theorem kmlem3

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)

Ref Expression
Assertion kmlem3 ⊢z∖⋃x∖z≠∅↔∃v∈z∀w∈xz≠w→¬v∈z∩w

Proof

Step Hyp Ref Expression
1 dfdif2 ⊢z∖⋃x∖z=v∈z|¬v∈⋃x∖z
2 dfnul3 ⊢∅=v∈z|¬v∈z
3 2 uneq2i ⊢v∈z|¬v∈⋃x∖z∪∅=v∈z|¬v∈⋃x∖z∪v∈z|¬v∈z
4 un0 ⊢v∈z|¬v∈⋃x∖z∪∅=v∈z|¬v∈⋃x∖z
5 unrab ⊢v∈z|¬v∈⋃x∖z∪v∈z|¬v∈z=v∈z|¬v∈⋃x∖z∨¬v∈z
6 3 4 5 3eqtr3i ⊢v∈z|¬v∈⋃x∖z=v∈z|¬v∈⋃x∖z∨¬v∈z
7 ianor ⊢¬v∈⋃x∖z∧v∈z↔¬v∈⋃x∖z∨¬v∈z
8 eluni ⊢v∈⋃x∖z↔∃wv∈w∧w∈x∖z
9 8 anbi1i ⊢v∈⋃x∖z∧v∈z↔∃wv∈w∧w∈x∖z∧v∈z
10 df-rex ⊢∃w∈x¬z≠w→¬v∈z∩w↔∃ww∈x∧¬z≠w→¬v∈z∩w
11 elin ⊢v∈z∩w↔v∈z∧v∈w
12 11 anbi2i ⊢z≠w∧v∈z∩w↔z≠w∧v∈z∧v∈w
13 df-an ⊢z≠w∧v∈z∩w↔¬z≠w→¬v∈z∩w
14 12 13 bitr3i ⊢z≠w∧v∈z∧v∈w↔¬z≠w→¬v∈z∩w
15 14 anbi2i ⊢w∈x∧z≠w∧v∈z∧v∈w↔w∈x∧¬z≠w→¬v∈z∩w
16 eldifsn ⊢w∈x∖z↔w∈x∧w≠z
17 necom ⊢w≠z↔z≠w
18 17 anbi2i ⊢w∈x∧w≠z↔w∈x∧z≠w
19 16 18 bitri ⊢w∈x∖z↔w∈x∧z≠w
20 19 anbi2i ⊢v∈w∧v∈z∧w∈x∖z↔v∈w∧v∈z∧w∈x∧z≠w
21 ancom ⊢v∈w∧v∈z↔v∈z∧v∈w
22 21 anbi2ci ⊢v∈w∧v∈z∧w∈x∧z≠w↔w∈x∧z≠w∧v∈z∧v∈w
23 anass ⊢w∈x∧z≠w∧v∈z∧v∈w↔w∈x∧z≠w∧v∈z∧v∈w
24 20 22 23 3bitri ⊢v∈w∧v∈z∧w∈x∖z↔w∈x∧z≠w∧v∈z∧v∈w
25 an32 ⊢v∈w∧v∈z∧w∈x∖z↔v∈w∧w∈x∖z∧v∈z
26 24 25 bitr3i ⊢w∈x∧z≠w∧v∈z∧v∈w↔v∈w∧w∈x∖z∧v∈z
27 15 26 bitr3i ⊢w∈x∧¬z≠w→¬v∈z∩w↔v∈w∧w∈x∖z∧v∈z
28 27 exbii ⊢∃ww∈x∧¬z≠w→¬v∈z∩w↔∃wv∈w∧w∈x∖z∧v∈z
29 19.41v ⊢∃wv∈w∧w∈x∖z∧v∈z↔∃wv∈w∧w∈x∖z∧v∈z
30 10 28 29 3bitri ⊢∃w∈x¬z≠w→¬v∈z∩w↔∃wv∈w∧w∈x∖z∧v∈z
31 rexnal ⊢∃w∈x¬z≠w→¬v∈z∩w↔¬∀w∈xz≠w→¬v∈z∩w
32 9 30 31 3bitr2ri ⊢¬∀w∈xz≠w→¬v∈z∩w↔v∈⋃x∖z∧v∈z
33 32 con1bii ⊢¬v∈⋃x∖z∧v∈z↔∀w∈xz≠w→¬v∈z∩w
34 7 33 bitr3i ⊢¬v∈⋃x∖z∨¬v∈z↔∀w∈xz≠w→¬v∈z∩w
35 34 rabbii ⊢v∈z|¬v∈⋃x∖z∨¬v∈z=v∈z|∀w∈xz≠w→¬v∈z∩w
36 1 6 35 3eqtri ⊢z∖⋃x∖z=v∈z|∀w∈xz≠w→¬v∈z∩w
37 36 neeq1i ⊢z∖⋃x∖z≠∅↔v∈z|∀w∈xz≠w→¬v∈z∩w≠∅
38 rabn0 ⊢v∈z|∀w∈xz≠w→¬v∈z∩w≠∅↔∃v∈z∀w∈xz≠w→¬v∈z∩w
39 37 38 bitri ⊢z∖⋃x∖z≠∅↔∃v∈z∀w∈xz≠w→¬v∈z∩w