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