This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝑤 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤 ) → ( ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ∩ 𝑤 ) = ∅ )

Proof

Step Hyp Ref Expression
1 elequ1 ⊢ ( 𝑣 = 𝑤 → ( 𝑣 ∈ 𝑥 ↔ 𝑤 ∈ 𝑥 ) )
2 neeq2 ⊢ ( 𝑣 = 𝑤 → ( 𝑧 ≠ 𝑣 ↔ 𝑧 ≠ 𝑤 ) )
3 1 2 anbi12d ⊢ ( 𝑣 = 𝑤 → ( ( 𝑣 ∈ 𝑥 ∧ 𝑧 ≠ 𝑣 ) ↔ ( 𝑤 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤 ) ) )
4 elequ2 ⊢ ( 𝑣 = 𝑤 → ( 𝑦 ∈ 𝑣 ↔ 𝑦 ∈ 𝑤 ) )
5 4 notbid ⊢ ( 𝑣 = 𝑤 → ( ¬ 𝑦 ∈ 𝑣 ↔ ¬ 𝑦 ∈ 𝑤 ) )
6 3 5 imbi12d ⊢ ( 𝑣 = 𝑤 → ( ( ( 𝑣 ∈ 𝑥 ∧ 𝑧 ≠ 𝑣 ) → ¬ 𝑦 ∈ 𝑣 ) ↔ ( ( 𝑤 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤 ) → ¬ 𝑦 ∈ 𝑤 ) ) )
7 6 spvv ⊢ ( ∀ 𝑣 ( ( 𝑣 ∈ 𝑥 ∧ 𝑧 ≠ 𝑣 ) → ¬ 𝑦 ∈ 𝑣 ) → ( ( 𝑤 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤 ) → ¬ 𝑦 ∈ 𝑤 ) )
8 eldif ⊢ ( 𝑦 ∈ ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ↔ ( 𝑦 ∈ 𝑧 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∖ { 𝑧 } ) ) )
9 simpr ⊢ ( ( 𝑦 ∈ 𝑧 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∖ { 𝑧 } ) ) → ¬ 𝑦 ∈ ∪ ( 𝑥 ∖ { 𝑧 } ) )
10 eluni ⊢ ( 𝑦 ∈ ∪ ( 𝑥 ∖ { 𝑧 } ) ↔ ∃ 𝑣 ( 𝑦 ∈ 𝑣 ∧ 𝑣 ∈ ( 𝑥 ∖ { 𝑧 } ) ) )
11 10 notbii ⊢ ( ¬ 𝑦 ∈ ∪ ( 𝑥 ∖ { 𝑧 } ) ↔ ¬ ∃ 𝑣 ( 𝑦 ∈ 𝑣 ∧ 𝑣 ∈ ( 𝑥 ∖ { 𝑧 } ) ) )
12 alnex ⊢ ( ∀ 𝑣 ¬ ( 𝑦 ∈ 𝑣 ∧ 𝑣 ∈ ( 𝑥 ∖ { 𝑧 } ) ) ↔ ¬ ∃ 𝑣 ( 𝑦 ∈ 𝑣 ∧ 𝑣 ∈ ( 𝑥 ∖ { 𝑧 } ) ) )
13 con2b ⊢ ( ( 𝑦 ∈ 𝑣 → ¬ 𝑣 ∈ ( 𝑥 ∖ { 𝑧 } ) ) ↔ ( 𝑣 ∈ ( 𝑥 ∖ { 𝑧 } ) → ¬ 𝑦 ∈ 𝑣 ) )
14 imnan ⊢ ( ( 𝑦 ∈ 𝑣 → ¬ 𝑣 ∈ ( 𝑥 ∖ { 𝑧 } ) ) ↔ ¬ ( 𝑦 ∈ 𝑣 ∧ 𝑣 ∈ ( 𝑥 ∖ { 𝑧 } ) ) )
15 eldifsn ⊢ ( 𝑣 ∈ ( 𝑥 ∖ { 𝑧 } ) ↔ ( 𝑣 ∈ 𝑥 ∧ 𝑣 ≠ 𝑧 ) )
16 necom ⊢ ( 𝑣 ≠ 𝑧 ↔ 𝑧 ≠ 𝑣 )
17 16 anbi2i ⊢ ( ( 𝑣 ∈ 𝑥 ∧ 𝑣 ≠ 𝑧 ) ↔ ( 𝑣 ∈ 𝑥 ∧ 𝑧 ≠ 𝑣 ) )
18 15 17 bitri ⊢ ( 𝑣 ∈ ( 𝑥 ∖ { 𝑧 } ) ↔ ( 𝑣 ∈ 𝑥 ∧ 𝑧 ≠ 𝑣 ) )
19 18 imbi1i ⊢ ( ( 𝑣 ∈ ( 𝑥 ∖ { 𝑧 } ) → ¬ 𝑦 ∈ 𝑣 ) ↔ ( ( 𝑣 ∈ 𝑥 ∧ 𝑧 ≠ 𝑣 ) → ¬ 𝑦 ∈ 𝑣 ) )
20 13 14 19 3bitr3i ⊢ ( ¬ ( 𝑦 ∈ 𝑣 ∧ 𝑣 ∈ ( 𝑥 ∖ { 𝑧 } ) ) ↔ ( ( 𝑣 ∈ 𝑥 ∧ 𝑧 ≠ 𝑣 ) → ¬ 𝑦 ∈ 𝑣 ) )
21 20 albii ⊢ ( ∀ 𝑣 ¬ ( 𝑦 ∈ 𝑣 ∧ 𝑣 ∈ ( 𝑥 ∖ { 𝑧 } ) ) ↔ ∀ 𝑣 ( ( 𝑣 ∈ 𝑥 ∧ 𝑧 ≠ 𝑣 ) → ¬ 𝑦 ∈ 𝑣 ) )
22 11 12 21 3bitr2i ⊢ ( ¬ 𝑦 ∈ ∪ ( 𝑥 ∖ { 𝑧 } ) ↔ ∀ 𝑣 ( ( 𝑣 ∈ 𝑥 ∧ 𝑧 ≠ 𝑣 ) → ¬ 𝑦 ∈ 𝑣 ) )
23 9 22 sylib ⊢ ( ( 𝑦 ∈ 𝑧 ∧ ¬ 𝑦 ∈ ∪ ( 𝑥 ∖ { 𝑧 } ) ) → ∀ 𝑣 ( ( 𝑣 ∈ 𝑥 ∧ 𝑧 ≠ 𝑣 ) → ¬ 𝑦 ∈ 𝑣 ) )
24 8 23 sylbi ⊢ ( 𝑦 ∈ ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) → ∀ 𝑣 ( ( 𝑣 ∈ 𝑥 ∧ 𝑧 ≠ 𝑣 ) → ¬ 𝑦 ∈ 𝑣 ) )
25 7 24 syl11 ⊢ ( ( 𝑤 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤 ) → ( 𝑦 ∈ ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) → ¬ 𝑦 ∈ 𝑤 ) )
26 25 ralrimiv ⊢ ( ( 𝑤 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤 ) → ∀ 𝑦 ∈ ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ¬ 𝑦 ∈ 𝑤 )
27 disj ⊢ ( ( ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ∩ 𝑤 ) = ∅ ↔ ∀ 𝑦 ∈ ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ¬ 𝑦 ∈ 𝑤 )
28 26 27 sylibr ⊢ ( ( 𝑤 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤 ) → ( ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ∩ 𝑤 ) = ∅ )