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

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 ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝜑 → 𝐴 = ∅ ) ) → ∀ 𝑧 ∈ 𝑥 ∃ 𝑣 ∈ 𝑧 ∀ 𝑤 ∈ 𝑥 ( 𝜑 → ¬ 𝑣 ∈ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 r19.26 ⊢ ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ ∧ ∀ 𝑤 ∈ 𝑥 ( 𝜑 → 𝐴 = ∅ ) ) ↔ ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝜑 → 𝐴 = ∅ ) ) )
2 n0 ⊢ ( 𝑧 ≠ ∅ ↔ ∃ 𝑣 𝑣 ∈ 𝑧 )
3 2 biimpi ⊢ ( 𝑧 ≠ ∅ → ∃ 𝑣 𝑣 ∈ 𝑧 )
4 ne0i ⊢ ( 𝑣 ∈ 𝐴 → 𝐴 ≠ ∅ )
5 4 necon2bi ⊢ ( 𝐴 = ∅ → ¬ 𝑣 ∈ 𝐴 )
6 5 imim2i ⊢ ( ( 𝜑 → 𝐴 = ∅ ) → ( 𝜑 → ¬ 𝑣 ∈ 𝐴 ) )
7 6 ralimi ⊢ ( ∀ 𝑤 ∈ 𝑥 ( 𝜑 → 𝐴 = ∅ ) → ∀ 𝑤 ∈ 𝑥 ( 𝜑 → ¬ 𝑣 ∈ 𝐴 ) )
8 7 alrimiv ⊢ ( ∀ 𝑤 ∈ 𝑥 ( 𝜑 → 𝐴 = ∅ ) → ∀ 𝑣 ∀ 𝑤 ∈ 𝑥 ( 𝜑 → ¬ 𝑣 ∈ 𝐴 ) )
9 19.29r ⊢ ( ( ∃ 𝑣 𝑣 ∈ 𝑧 ∧ ∀ 𝑣 ∀ 𝑤 ∈ 𝑥 ( 𝜑 → ¬ 𝑣 ∈ 𝐴 ) ) → ∃ 𝑣 ( 𝑣 ∈ 𝑧 ∧ ∀ 𝑤 ∈ 𝑥 ( 𝜑 → ¬ 𝑣 ∈ 𝐴 ) ) )
10 df-rex ⊢ ( ∃ 𝑣 ∈ 𝑧 ∀ 𝑤 ∈ 𝑥 ( 𝜑 → ¬ 𝑣 ∈ 𝐴 ) ↔ ∃ 𝑣 ( 𝑣 ∈ 𝑧 ∧ ∀ 𝑤 ∈ 𝑥 ( 𝜑 → ¬ 𝑣 ∈ 𝐴 ) ) )
11 9 10 sylibr ⊢ ( ( ∃ 𝑣 𝑣 ∈ 𝑧 ∧ ∀ 𝑣 ∀ 𝑤 ∈ 𝑥 ( 𝜑 → ¬ 𝑣 ∈ 𝐴 ) ) → ∃ 𝑣 ∈ 𝑧 ∀ 𝑤 ∈ 𝑥 ( 𝜑 → ¬ 𝑣 ∈ 𝐴 ) )
12 3 8 11 syl2an ⊢ ( ( 𝑧 ≠ ∅ ∧ ∀ 𝑤 ∈ 𝑥 ( 𝜑 → 𝐴 = ∅ ) ) → ∃ 𝑣 ∈ 𝑧 ∀ 𝑤 ∈ 𝑥 ( 𝜑 → ¬ 𝑣 ∈ 𝐴 ) )
13 12 ralimi ⊢ ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ ∧ ∀ 𝑤 ∈ 𝑥 ( 𝜑 → 𝐴 = ∅ ) ) → ∀ 𝑧 ∈ 𝑥 ∃ 𝑣 ∈ 𝑧 ∀ 𝑤 ∈ 𝑥 ( 𝜑 → ¬ 𝑣 ∈ 𝐴 ) )
14 1 13 sylbir ⊢ ( ( ∀ 𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ( 𝜑 → 𝐴 = ∅ ) ) → ∀ 𝑧 ∈ 𝑥 ∃ 𝑣 ∈ 𝑧 ∀ 𝑤 ∈ 𝑥 ( 𝜑 → ¬ 𝑣 ∈ 𝐴 ) )