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∈xz≠∅∧∀z∈x∀w∈xφ→A=∅→∀z∈x∃v∈z∀w∈xφ→¬v∈A

Proof

Step Hyp Ref Expression
1 r19.26 ⊢∀z∈xz≠∅∧∀w∈xφ→A=∅↔∀z∈xz≠∅∧∀z∈x∀w∈xφ→A=∅
2 n0 ⊢z≠∅↔∃vv∈z
3 2 biimpi ⊢z≠∅→∃vv∈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 ⊢∃vv∈z∧∀v∀w∈xφ→¬v∈A→∃vv∈z∧∀w∈xφ→¬v∈A
10 df-rex ⊢∃v∈z∀w∈xφ→¬v∈A↔∃vv∈z∧∀w∈xφ→¬v∈A
11 9 10 sylibr ⊢∃vv∈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∈xz≠∅∧∀w∈xφ→A=∅→∀z∈x∃v∈z∀w∈xφ→¬v∈A
14 1 13 sylbir ⊢∀z∈xz≠∅∧∀z∈x∀w∈xφ→A=∅→∀z∈x∃v∈z∀w∈xφ→¬v∈A