Theorem kmlem3

Description: Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. The right-hand side is part of the hypothesis of 4. (Contributed by NM, 25-Mar-2004)

	Ref	Expression
Assertion	kmlem3	⊢ ( ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ≠ ∅ ↔ ∃ 𝑣 ∈ 𝑧 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dfdif2	⊢ ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) = { 𝑣 ∈ 𝑧 ∣ ¬ 𝑣 ∈ ∪ ( 𝑥 ∖ { 𝑧 } ) }
2		dfnul3	⊢ ∅ = { 𝑣 ∈ 𝑧 ∣ ¬ 𝑣 ∈ 𝑧 }
3	2	uneq2i	⊢ ( { 𝑣 ∈ 𝑧 ∣ ¬ 𝑣 ∈ ∪ ( 𝑥 ∖ { 𝑧 } ) } ∪ ∅ ) = ( { 𝑣 ∈ 𝑧 ∣ ¬ 𝑣 ∈ ∪ ( 𝑥 ∖ { 𝑧 } ) } ∪ { 𝑣 ∈ 𝑧 ∣ ¬ 𝑣 ∈ 𝑧 } )
4		un0	⊢ ( { 𝑣 ∈ 𝑧 ∣ ¬ 𝑣 ∈ ∪ ( 𝑥 ∖ { 𝑧 } ) } ∪ ∅ ) = { 𝑣 ∈ 𝑧 ∣ ¬ 𝑣 ∈ ∪ ( 𝑥 ∖ { 𝑧 } ) }
5		unrab	⊢ ( { 𝑣 ∈ 𝑧 ∣ ¬ 𝑣 ∈ ∪ ( 𝑥 ∖ { 𝑧 } ) } ∪ { 𝑣 ∈ 𝑧 ∣ ¬ 𝑣 ∈ 𝑧 } ) = { 𝑣 ∈ 𝑧 ∣ ( ¬ 𝑣 ∈ ∪ ( 𝑥 ∖ { 𝑧 } ) ∨ ¬ 𝑣 ∈ 𝑧 ) }
6	3 4 5	3eqtr3i	⊢ { 𝑣 ∈ 𝑧 ∣ ¬ 𝑣 ∈ ∪ ( 𝑥 ∖ { 𝑧 } ) } = { 𝑣 ∈ 𝑧 ∣ ( ¬ 𝑣 ∈ ∪ ( 𝑥 ∖ { 𝑧 } ) ∨ ¬ 𝑣 ∈ 𝑧 ) }
7		ianor	⊢ ( ¬ ( 𝑣 ∈ ∪ ( 𝑥 ∖ { 𝑧 } ) ∧ 𝑣 ∈ 𝑧 ) ↔ ( ¬ 𝑣 ∈ ∪ ( 𝑥 ∖ { 𝑧 } ) ∨ ¬ 𝑣 ∈ 𝑧 ) )
8		eluni	⊢ ( 𝑣 ∈ ∪ ( 𝑥 ∖ { 𝑧 } ) ↔ ∃ 𝑤 ( 𝑣 ∈ 𝑤 ∧ 𝑤 ∈ ( 𝑥 ∖ { 𝑧 } ) ) )
9	8	anbi1i	⊢ ( ( 𝑣 ∈ ∪ ( 𝑥 ∖ { 𝑧 } ) ∧ 𝑣 ∈ 𝑧 ) ↔ ( ∃ 𝑤 ( 𝑣 ∈ 𝑤 ∧ 𝑤 ∈ ( 𝑥 ∖ { 𝑧 } ) ) ∧ 𝑣 ∈ 𝑧 ) )
10		df-rex	⊢ ( ∃ 𝑤 ∈ 𝑥 ¬ ( 𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) ↔ ∃ 𝑤 ( 𝑤 ∈ 𝑥 ∧ ¬ ( 𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) ) )
11		elin	⊢ ( 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ↔ ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑤 ) )
12	11	anbi2i	⊢ ( ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) ↔ ( 𝑧 ≠ 𝑤 ∧ ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑤 ) ) )
13		df-an	⊢ ( ( 𝑧 ≠ 𝑤 ∧ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) ↔ ¬ ( 𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) )
14	12 13	bitr3i	⊢ ( ( 𝑧 ≠ 𝑤 ∧ ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑤 ) ) ↔ ¬ ( 𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) )
15	14	anbi2i	⊢ ( ( 𝑤 ∈ 𝑥 ∧ ( 𝑧 ≠ 𝑤 ∧ ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑤 ) ) ) ↔ ( 𝑤 ∈ 𝑥 ∧ ¬ ( 𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) ) )
16		eldifsn	⊢ ( 𝑤 ∈ ( 𝑥 ∖ { 𝑧 } ) ↔ ( 𝑤 ∈ 𝑥 ∧ 𝑤 ≠ 𝑧 ) )
17		necom	⊢ ( 𝑤 ≠ 𝑧 ↔ 𝑧 ≠ 𝑤 )
18	17	anbi2i	⊢ ( ( 𝑤 ∈ 𝑥 ∧ 𝑤 ≠ 𝑧 ) ↔ ( 𝑤 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤 ) )
19	16 18	bitri	⊢ ( 𝑤 ∈ ( 𝑥 ∖ { 𝑧 } ) ↔ ( 𝑤 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤 ) )
20	19	anbi2i	⊢ ( ( ( 𝑣 ∈ 𝑤 ∧ 𝑣 ∈ 𝑧 ) ∧ 𝑤 ∈ ( 𝑥 ∖ { 𝑧 } ) ) ↔ ( ( 𝑣 ∈ 𝑤 ∧ 𝑣 ∈ 𝑧 ) ∧ ( 𝑤 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤 ) ) )
21		ancom	⊢ ( ( 𝑣 ∈ 𝑤 ∧ 𝑣 ∈ 𝑧 ) ↔ ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑤 ) )
22	21	anbi2ci	⊢ ( ( ( 𝑣 ∈ 𝑤 ∧ 𝑣 ∈ 𝑧 ) ∧ ( 𝑤 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤 ) ) ↔ ( ( 𝑤 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤 ) ∧ ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑤 ) ) )
23		anass	⊢ ( ( ( 𝑤 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤 ) ∧ ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑤 ) ) ↔ ( 𝑤 ∈ 𝑥 ∧ ( 𝑧 ≠ 𝑤 ∧ ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑤 ) ) ) )
24	20 22 23	3bitri	⊢ ( ( ( 𝑣 ∈ 𝑤 ∧ 𝑣 ∈ 𝑧 ) ∧ 𝑤 ∈ ( 𝑥 ∖ { 𝑧 } ) ) ↔ ( 𝑤 ∈ 𝑥 ∧ ( 𝑧 ≠ 𝑤 ∧ ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑤 ) ) ) )
25		an32	⊢ ( ( ( 𝑣 ∈ 𝑤 ∧ 𝑣 ∈ 𝑧 ) ∧ 𝑤 ∈ ( 𝑥 ∖ { 𝑧 } ) ) ↔ ( ( 𝑣 ∈ 𝑤 ∧ 𝑤 ∈ ( 𝑥 ∖ { 𝑧 } ) ) ∧ 𝑣 ∈ 𝑧 ) )
26	24 25	bitr3i	⊢ ( ( 𝑤 ∈ 𝑥 ∧ ( 𝑧 ≠ 𝑤 ∧ ( 𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑤 ) ) ) ↔ ( ( 𝑣 ∈ 𝑤 ∧ 𝑤 ∈ ( 𝑥 ∖ { 𝑧 } ) ) ∧ 𝑣 ∈ 𝑧 ) )
27	15 26	bitr3i	⊢ ( ( 𝑤 ∈ 𝑥 ∧ ¬ ( 𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) ) ↔ ( ( 𝑣 ∈ 𝑤 ∧ 𝑤 ∈ ( 𝑥 ∖ { 𝑧 } ) ) ∧ 𝑣 ∈ 𝑧 ) )
28	27	exbii	⊢ ( ∃ 𝑤 ( 𝑤 ∈ 𝑥 ∧ ¬ ( 𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) ) ↔ ∃ 𝑤 ( ( 𝑣 ∈ 𝑤 ∧ 𝑤 ∈ ( 𝑥 ∖ { 𝑧 } ) ) ∧ 𝑣 ∈ 𝑧 ) )
29		19.41v	⊢ ( ∃ 𝑤 ( ( 𝑣 ∈ 𝑤 ∧ 𝑤 ∈ ( 𝑥 ∖ { 𝑧 } ) ) ∧ 𝑣 ∈ 𝑧 ) ↔ ( ∃ 𝑤 ( 𝑣 ∈ 𝑤 ∧ 𝑤 ∈ ( 𝑥 ∖ { 𝑧 } ) ) ∧ 𝑣 ∈ 𝑧 ) )
30	10 28 29	3bitri	⊢ ( ∃ 𝑤 ∈ 𝑥 ¬ ( 𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) ↔ ( ∃ 𝑤 ( 𝑣 ∈ 𝑤 ∧ 𝑤 ∈ ( 𝑥 ∖ { 𝑧 } ) ) ∧ 𝑣 ∈ 𝑧 ) )
31		rexnal	⊢ ( ∃ 𝑤 ∈ 𝑥 ¬ ( 𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) ↔ ¬ ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) )
32	9 30 31	3bitr2ri	⊢ ( ¬ ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) ↔ ( 𝑣 ∈ ∪ ( 𝑥 ∖ { 𝑧 } ) ∧ 𝑣 ∈ 𝑧 ) )
33	32	con1bii	⊢ ( ¬ ( 𝑣 ∈ ∪ ( 𝑥 ∖ { 𝑧 } ) ∧ 𝑣 ∈ 𝑧 ) ↔ ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) )
34	7 33	bitr3i	⊢ ( ( ¬ 𝑣 ∈ ∪ ( 𝑥 ∖ { 𝑧 } ) ∨ ¬ 𝑣 ∈ 𝑧 ) ↔ ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) )
35	34	rabbii	⊢ { 𝑣 ∈ 𝑧 ∣ ( ¬ 𝑣 ∈ ∪ ( 𝑥 ∖ { 𝑧 } ) ∨ ¬ 𝑣 ∈ 𝑧 ) } = { 𝑣 ∈ 𝑧 ∣ ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) }
36	1 6 35	3eqtri	⊢ ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) = { 𝑣 ∈ 𝑧 ∣ ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) }
37	36	neeq1i	⊢ ( ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ≠ ∅ ↔ { 𝑣 ∈ 𝑧 ∣ ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) } ≠ ∅ )
38		rabn0	⊢ ( { 𝑣 ∈ 𝑧 ∣ ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) } ≠ ∅ ↔ ∃ 𝑣 ∈ 𝑧 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) )
39	37 38	bitri	⊢ ( ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ≠ ∅ ↔ ∃ 𝑣 ∈ 𝑧 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) )