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 ⊢∀vv∈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↔∃vy∈v∧v∈x∖z
11 10 notbii ⊢¬y∈⋃x∖z↔¬∃vy∈v∧v∈x∖z
12 alnex ⊢∀v¬y∈v∧v∈x∖z↔¬∃vy∈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↔∀vv∈x∧z≠v→¬y∈v
22 11 12 21 3bitr2i ⊢¬y∈⋃x∖z↔∀vv∈x∧z≠v→¬y∈v
23 9 22 sylib ⊢y∈z∧¬y∈⋃x∖z→∀vv∈x∧z≠v→¬y∈v
24 8 23 sylbi ⊢y∈z∖⋃x∖z→∀vv∈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=∅