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