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	$⊢ (w \in x \land z \neq w) \to (z ∖ ⋃ (x ∖ \{z\})) \cap (w ∖ ⋃ (x ∖ \{w\})) = \emptyset$

Step	Hyp	Ref	Expression
1		difss	$⊢ w ∖ ⋃ (x ∖ \{w\}) \subseteq w$
2		sslin	$⊢ w ∖ ⋃ (x ∖ \{w\}) \subseteq w \to (z ∖ ⋃ (x ∖ \{z\})) \cap (w ∖ ⋃ (x ∖ \{w\})) \subseteq (z ∖ ⋃ (x ∖ \{z\})) \cap w$
3	1 2	ax-mp	$⊢ (z ∖ ⋃ (x ∖ \{z\})) \cap (w ∖ ⋃ (x ∖ \{w\})) \subseteq (z ∖ ⋃ (x ∖ \{z\})) \cap w$
4		kmlem4	$⊢ (w \in x \land z \neq w) \to (z ∖ ⋃ (x ∖ \{z\})) \cap w = \emptyset$
5	3 4	sseqtrid	$⊢ (w \in x \land z \neq w) \to (z ∖ ⋃ (x ∖ \{z\})) \cap (w ∖ ⋃ (x ∖ \{w\})) \subseteq \emptyset$
6		ss0b	$⊢ (z ∖ ⋃ (x ∖ \{z\})) \cap (w ∖ ⋃ (x ∖ \{w\})) \subseteq \emptyset \leftrightarrow (z ∖ ⋃ (x ∖ \{z\})) \cap (w ∖ ⋃ (x ∖ \{w\})) = \emptyset$
7	5 6	sylib	$⊢ (w \in x \land z \neq w) \to (z ∖ ⋃ (x ∖ \{z\})) \cap (w ∖ ⋃ (x ∖ \{w\})) = \emptyset$

Metamath Proof Explorer