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	$$⊢\left(w\in x\wedge z\ne w\right)\to \left(z\setminus \bigcup \left(x\setminus \left\{z\right\}\right)\right)\cap \left(w\setminus \bigcup \left(x\setminus \left\{w\right\}\right)\right)=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		difss	$$⊢w\setminus \bigcup \left(x\setminus \left\{w\right\}\right)\subseteq w$$
2		sslin	$$⊢w\setminus \bigcup \left(x\setminus \left\{w\right\}\right)\subseteq w\to \left(z\setminus \bigcup \left(x\setminus \left\{z\right\}\right)\right)\cap \left(w\setminus \bigcup \left(x\setminus \left\{w\right\}\right)\right)\subseteq \left(z\setminus \bigcup \left(x\setminus \left\{z\right\}\right)\right)\cap w$$
3	1 2	ax-mp	$$⊢\left(z\setminus \bigcup \left(x\setminus \left\{z\right\}\right)\right)\cap \left(w\setminus \bigcup \left(x\setminus \left\{w\right\}\right)\right)\subseteq \left(z\setminus \bigcup \left(x\setminus \left\{z\right\}\right)\right)\cap w$$
4		kmlem4	$$⊢\left(w\in x\wedge z\ne w\right)\to \left(z\setminus \bigcup \left(x\setminus \left\{z\right\}\right)\right)\cap w=\varnothing$$
5	3 4	sseqtrid	$$⊢\left(w\in x\wedge z\ne w\right)\to \left(z\setminus \bigcup \left(x\setminus \left\{z\right\}\right)\right)\cap \left(w\setminus \bigcup \left(x\setminus \left\{w\right\}\right)\right)\subseteq \varnothing$$
6		ss0b	$$⊢\left(z\setminus \bigcup \left(x\setminus \left\{z\right\}\right)\right)\cap \left(w\setminus \bigcup \left(x\setminus \left\{w\right\}\right)\right)\subseteq \varnothing \leftrightarrow \left(z\setminus \bigcup \left(x\setminus \left\{z\right\}\right)\right)\cap \left(w\setminus \bigcup \left(x\setminus \left\{w\right\}\right)\right)=\varnothing$$
7	5 6	sylib	$$⊢\left(w\in x\wedge z\ne w\right)\to \left(z\setminus \bigcup \left(x\setminus \left\{z\right\}\right)\right)\cap \left(w\setminus \bigcup \left(x\setminus \left\{w\right\}\right)\right)=\varnothing$$