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