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 ∈ x z ≠ 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 ↔ ∃ w v ∈ w ∧ w ∈ x ∖ z
9 8 anbi1i ⊢ v ∈ ⋃ x ∖ z ∧ v ∈ z ↔ ∃ w v ∈ w ∧ w ∈ x ∖ z ∧ v ∈ z
10 df-rex ⊢ ∃ w ∈ x ¬ z ≠ w → ¬ v ∈ z ∩ w ↔ ∃ w w ∈ 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 ⊢ ∃ w w ∈ x ∧ ¬ z ≠ w → ¬ v ∈ z ∩ w ↔ ∃ w v ∈ w ∧ w ∈ x ∖ z ∧ v ∈ z
29 19.41v ⊢ ∃ w v ∈ w ∧ w ∈ x ∖ z ∧ v ∈ z ↔ ∃ w v ∈ w ∧ w ∈ x ∖ z ∧ v ∈ z
30 10 28 29 3bitri ⊢ ∃ w ∈ x ¬ z ≠ w → ¬ v ∈ z ∩ w ↔ ∃ w v ∈ w ∧ w ∈ x ∖ z ∧ v ∈ z
31 rexnal ⊢ ∃ w ∈ x ¬ z ≠ w → ¬ v ∈ z ∩ w ↔ ¬ ∀ w ∈ x z ≠ w → ¬ v ∈ z ∩ w
32 9 30 31 3bitr2ri ⊢ ¬ ∀ w ∈ x z ≠ w → ¬ v ∈ z ∩ w ↔ v ∈ ⋃ x ∖ z ∧ v ∈ z
33 32 con1bii ⊢ ¬ v ∈ ⋃ x ∖ z ∧ v ∈ z ↔ ∀ w ∈ x z ≠ w → ¬ v ∈ z ∩ w
34 7 33 bitr3i ⊢ ¬ v ∈ ⋃ x ∖ z ∨ ¬ v ∈ z ↔ ∀ w ∈ x z ≠ w → ¬ v ∈ z ∩ w
35 34 rabbii ⊢ v ∈ z | ¬ v ∈ ⋃ x ∖ z ∨ ¬ v ∈ z = v ∈ z | ∀ w ∈ x z ≠ w → ¬ v ∈ z ∩ w
36 1 6 35 3eqtri ⊢ z ∖ ⋃ x ∖ z = v ∈ z | ∀ w ∈ x z ≠ w → ¬ v ∈ z ∩ w
37 36 neeq1i ⊢ z ∖ ⋃ x ∖ z ≠ ∅ ↔ v ∈ z | ∀ w ∈ x z ≠ w → ¬ v ∈ z ∩ w ≠ ∅
38 rabn0 ⊢ v ∈ z | ∀ w ∈ x z ≠ w → ¬ v ∈ z ∩ w ≠ ∅ ↔ ∃ v ∈ z ∀ w ∈ x z ≠ w → ¬ v ∈ z ∩ w
39 37 38 bitri ⊢ z ∖ ⋃ x ∖ z ≠ ∅ ↔ ∃ v ∈ z ∀ w ∈ x z ≠ w → ¬ v ∈ z ∩ w