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

Metamath Proof Explorer

Theorem kmlem5

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

Ref Expression
Assertion kmlem5 ( ( 𝑤 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤 ) → ( ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ∩ ( 𝑤 ∖ ∪ ( 𝑥 ∖ { 𝑤 } ) ) ) = ∅ )

Proof

Step Hyp Ref Expression
1 difss ⊢ ( 𝑤 ∖ ∪ ( 𝑥 ∖ { 𝑤 } ) ) ⊆ 𝑤
2 sslin ⊢ ( ( 𝑤 ∖ ∪ ( 𝑥 ∖ { 𝑤 } ) ) ⊆ 𝑤 → ( ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ∩ ( 𝑤 ∖ ∪ ( 𝑥 ∖ { 𝑤 } ) ) ) ⊆ ( ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ∩ 𝑤 ) )
3 1 2 ax-mp ⊢ ( ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ∩ ( 𝑤 ∖ ∪ ( 𝑥 ∖ { 𝑤 } ) ) ) ⊆ ( ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ∩ 𝑤 )
4 kmlem4 ⊢ ( ( 𝑤 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤 ) → ( ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ∩ 𝑤 ) = ∅ )
5 3 4 sseqtrid ⊢ ( ( 𝑤 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤 ) → ( ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ∩ ( 𝑤 ∖ ∪ ( 𝑥 ∖ { 𝑤 } ) ) ) ⊆ ∅ )
6 ss0b ⊢ ( ( ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ∩ ( 𝑤 ∖ ∪ ( 𝑥 ∖ { 𝑤 } ) ) ) ⊆ ∅ ↔ ( ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ∩ ( 𝑤 ∖ ∪ ( 𝑥 ∖ { 𝑤 } ) ) ) = ∅ )
7 5 6 sylib ⊢ ( ( 𝑤 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤 ) → ( ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ∩ ( 𝑤 ∖ ∪ ( 𝑥 ∖ { 𝑤 } ) ) ) = ∅ )