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 simpr ⊢ y ∈ z ∧ ¬ y ∈ ⋃ x ∖ z → ¬ y ∈ ⋃ x ∖ z
10 eluni ⊢ y ∈ ⋃ x ∖ z ↔ ∃ v y ∈ v ∧ v ∈ x ∖ z
11 10 notbii ⊢ ¬ y ∈ ⋃ x ∖ z ↔ ¬ ∃ v y ∈ v ∧ v ∈ x ∖ z
12 alnex ⊢ ∀ v ¬ y ∈ v ∧ v ∈ x ∖ z ↔ ¬ ∃ v y ∈ v ∧ v ∈ x ∖ z
13 con2b ⊢ y ∈ v → ¬ v ∈ x ∖ z ↔ v ∈ x ∖ z → ¬ y ∈ v
14 imnan ⊢ y ∈ v → ¬ v ∈ x ∖ z ↔ ¬ y ∈ v ∧ v ∈ x ∖ z
15 eldifsn ⊢ v ∈ x ∖ z ↔ v ∈ x ∧ v ≠ z
16 necom ⊢ v ≠ z ↔ z ≠ v
17 16 anbi2i ⊢ v ∈ x ∧ v ≠ z ↔ v ∈ x ∧ z ≠ v
18 15 17 bitri ⊢ v ∈ x ∖ z ↔ v ∈ x ∧ z ≠ v
19 18 imbi1i ⊢ v ∈ x ∖ z → ¬ y ∈ v ↔ v ∈ x ∧ z ≠ v → ¬ y ∈ v
20 13 14 19 3bitr3i ⊢ ¬ y ∈ v ∧ v ∈ x ∖ z ↔ v ∈ x ∧ z ≠ v → ¬ y ∈ v
21 20 albii ⊢ ∀ v ¬ y ∈ v ∧ v ∈ x ∖ z ↔ ∀ v v ∈ x ∧ z ≠ v → ¬ y ∈ v
22 11 12 21 3bitr2i ⊢ ¬ y ∈ ⋃ x ∖ z ↔ ∀ v v ∈ x ∧ z ≠ v → ¬ y ∈ v
23 9 22 sylib ⊢ y ∈ z ∧ ¬ y ∈ ⋃ x ∖ z → ∀ v v ∈ x ∧ z ≠ v → ¬ y ∈ v
24 8 23 sylbi ⊢ y ∈ z ∖ ⋃ x ∖ z → ∀ v v ∈ x ∧ z ≠ v → ¬ y ∈ v
25 7 24 syl11 ⊢ w ∈ x ∧ z ≠ w → y ∈ z ∖ ⋃ x ∖ z → ¬ y ∈ w
26 25 ralrimiv ⊢ w ∈ x ∧ z ≠ w → ∀ y ∈ z ∖ ⋃ x ∖ z ¬ y ∈ w
27 disj ⊢ z ∖ ⋃ x ∖ z ∩ w = ∅ ↔ ∀ y ∈ z ∖ ⋃ x ∖ z ¬ y ∈ w
28 26 27 sylibr ⊢ w ∈ x ∧ z ≠ w → z ∖ ⋃ x ∖ z ∩ w = ∅