Metamath Proof Explorer

Theorem kmlem6

Description: Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 4 => 1. (Contributed by NM, 26-Mar-2004)

Ref Expression
Assertion kmlem6 ⊢ ∀ z ∈ x z ≠ ∅ ∧ ∀ z ∈ x ∀ w ∈ x φ → A = ∅ → ∀ z ∈ x ∃ v ∈ z ∀ w ∈ x φ → ¬ v ∈ A

Proof

Step Hyp Ref Expression
1 r19.26 ⊢ ∀ z ∈ x z ≠ ∅ ∧ ∀ w ∈ x φ → A = ∅ ↔ ∀ z ∈ x z ≠ ∅ ∧ ∀ z ∈ x ∀ w ∈ x φ → A = ∅
2 n0 ⊢ z ≠ ∅ ↔ ∃ v v ∈ z
3 2 biimpi ⊢ z ≠ ∅ → ∃ v v ∈ z
4 ne0i ⊢ v ∈ A → A ≠ ∅
5 4 necon2bi ⊢ A = ∅ → ¬ v ∈ A
6 5 imim2i ⊢ φ → A = ∅ → φ → ¬ v ∈ A
7 6 ralimi ⊢ ∀ w ∈ x φ → A = ∅ → ∀ w ∈ x φ → ¬ v ∈ A
8 7 alrimiv ⊢ ∀ w ∈ x φ → A = ∅ → ∀ v ∀ w ∈ x φ → ¬ v ∈ A
9 19.29r ⊢ ∃ v v ∈ z ∧ ∀ v ∀ w ∈ x φ → ¬ v ∈ A → ∃ v v ∈ z ∧ ∀ w ∈ x φ → ¬ v ∈ A
10 df-rex ⊢ ∃ v ∈ z ∀ w ∈ x φ → ¬ v ∈ A ↔ ∃ v v ∈ z ∧ ∀ w ∈ x φ → ¬ v ∈ A
11 9 10 sylibr ⊢ ∃ v v ∈ z ∧ ∀ v ∀ w ∈ x φ → ¬ v ∈ A → ∃ v ∈ z ∀ w ∈ x φ → ¬ v ∈ A
12 3 8 11 syl2an ⊢ z ≠ ∅ ∧ ∀ w ∈ x φ → A = ∅ → ∃ v ∈ z ∀ w ∈ x φ → ¬ v ∈ A
13 12 ralimi ⊢ ∀ z ∈ x z ≠ ∅ ∧ ∀ w ∈ x φ → A = ∅ → ∀ z ∈ x ∃ v ∈ z ∀ w ∈ x φ → ¬ v ∈ A
14 1 13 sylbir ⊢ ∀ z ∈ x z ≠ ∅ ∧ ∀ z ∈ x ∀ w ∈ x φ → A = ∅ → ∀ z ∈ x ∃ v ∈ z ∀ w ∈ x φ → ¬ v ∈ A