Metamath Proof Explorer

Theorem kmlem4

Description: Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. (Contributed by NM, 26-Mar-2004)

Ref Expression
Assertion kmlem4 ⊢ w ∈ x ∧ z ≠ w → z ∖ ⋃ x ∖ z ∩ w = ∅

Proof

Step Hyp Ref Expression
1 elequ1 ⊢ v = w → v ∈ x ↔ w ∈ x
2 neeq2 ⊢ v = w → z ≠ v ↔ z ≠ w
3 1 2 anbi12d ⊢ v = w → v ∈ x ∧ z ≠ v ↔ w ∈ x ∧ z ≠ w
4 elequ2 ⊢ v = w → y ∈ v ↔ y ∈ w
5 4 notbid ⊢ v = w → ¬ y ∈ v ↔ ¬ y ∈ w
6 3 5 imbi12d ⊢ v = w → v ∈ x ∧ z ≠ v → ¬ y ∈ v ↔ w ∈ x ∧ z ≠ w → ¬ y ∈ w
7 6 spvv ⊢ ∀ v v ∈ x ∧ z ≠ v → ¬ y ∈ v → w ∈ x ∧ z ≠ w → ¬ y ∈ w
8 eldif ⊢ y ∈ z ∖ ⋃ x ∖ z ↔ y ∈ z ∧ ¬ y ∈ ⋃ x ∖ z
9 eluni ⊢ y ∈ ⋃ x ∖ z ↔ ∃ v y ∈ v ∧ v ∈ x ∖ z
10 9 notbii ⊢ ¬ y ∈ ⋃ x ∖ z ↔ ¬ ∃ v y ∈ v ∧ v ∈ x ∖ z
11 alnex ⊢ ∀ v ¬ y ∈ v ∧ v ∈ x ∖ z ↔ ¬ ∃ v y ∈ v ∧ v ∈ x ∖ z
12 con2b ⊢ y ∈ v → ¬ v ∈ x ∖ z ↔ v ∈ x ∖ z → ¬ y ∈ v
13 imnan ⊢ y ∈ v → ¬ v ∈ x ∖ z ↔ ¬ y ∈ v ∧ v ∈ x ∖ z
14 eldifsn ⊢ v ∈ x ∖ z ↔ v ∈ x ∧ v ≠ z
15 necom ⊢ v ≠ z ↔ z ≠ v
16 15 anbi2i ⊢ v ∈ x ∧ v ≠ z ↔ v ∈ x ∧ z ≠ v
17 14 16 bitri ⊢ v ∈ x ∖ z ↔ v ∈ x ∧ z ≠ v
18 17 imbi1i ⊢ v ∈ x ∖ z → ¬ y ∈ v ↔ v ∈ x ∧ z ≠ v → ¬ y ∈ v
19 12 13 18 3bitr3i ⊢ ¬ y ∈ v ∧ v ∈ x ∖ z ↔ v ∈ x ∧ z ≠ v → ¬ y ∈ v
20 19 albii ⊢ ∀ v ¬ y ∈ v ∧ v ∈ x ∖ z ↔ ∀ v v ∈ x ∧ z ≠ v → ¬ y ∈ v
21 10 11 20 3bitr2i ⊢ ¬ y ∈ ⋃ x ∖ z ↔ ∀ v v ∈ x ∧ z ≠ v → ¬ y ∈ v
22 21 bilani ⊢ y ∈ z ∧ ¬ y ∈ ⋃ x ∖ z → ∀ v v ∈ x ∧ z ≠ v → ¬ y ∈ v
23 8 22 sylbi ⊢ y ∈ z ∖ ⋃ x ∖ z → ∀ v v ∈ x ∧ z ≠ v → ¬ y ∈ v
24 7 23 syl11 ⊢ w ∈ x ∧ z ≠ w → y ∈ z ∖ ⋃ x ∖ z → ¬ y ∈ w
25 24 ralrimiv ⊢ w ∈ x ∧ z ≠ w → ∀ y ∈ z ∖ ⋃ x ∖ z ¬ y ∈ w
26 disj ⊢ z ∖ ⋃ x ∖ z ∩ w = ∅ ↔ ∀ y ∈ z ∖ ⋃ x ∖ z ¬ y ∈ w
27 25 26 sylibr ⊢ w ∈ x ∧ z ≠ w → z ∖ ⋃ x ∖ z ∩ w = ∅