This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( 𝑧 ∖ ∪ ( 𝑥 ∖ { 𝑧 } ) ) ≠ ∅ ↔ ∃ 𝑣 ∈ 𝑧 ∀ 𝑤 ∈ 𝑥 ( 𝑧 ≠ 𝑤 → ¬ 𝑣 ∈ ( 𝑧 ∩ 𝑤 ) ) )