Metamath Proof Explorer

Theorem kmlem7

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

Ref Expression
Assertion kmlem7 ⊢∀z∈xz≠∅∧∀z∈x∀w∈xz≠w→z∩w=∅→¬∃z∈x∀v∈z∃w∈xz≠w∧v∈z∩w

Proof

Step Hyp Ref Expression
1 kmlem6 ⊢∀z∈xz≠∅∧∀z∈x∀w∈xz≠w→z∩w=∅→∀z∈x∃v∈z∀w∈xz≠w→¬v∈z∩w
2 ralinexa ⊢∀w∈xz≠w→¬v∈z∩w↔¬∃w∈xz≠w∧v∈z∩w
3 2 rexbii ⊢∃v∈z∀w∈xz≠w→¬v∈z∩w↔∃v∈z¬∃w∈xz≠w∧v∈z∩w
4 rexnal ⊢∃v∈z¬∃w∈xz≠w∧v∈z∩w↔¬∀v∈z∃w∈xz≠w∧v∈z∩w
5 3 4 bitri ⊢∃v∈z∀w∈xz≠w→¬v∈z∩w↔¬∀v∈z∃w∈xz≠w∧v∈z∩w
6 5 ralbii ⊢∀z∈x∃v∈z∀w∈xz≠w→¬v∈z∩w↔∀z∈x¬∀v∈z∃w∈xz≠w∧v∈z∩w
7 ralnex ⊢∀z∈x¬∀v∈z∃w∈xz≠w∧v∈z∩w↔¬∃z∈x∀v∈z∃w∈xz≠w∧v∈z∩w
8 6 7 bitri ⊢∀z∈x∃v∈z∀w∈xz≠w→¬v∈z∩w↔¬∃z∈x∀v∈z∃w∈xz≠w∧v∈z∩w
9 1 8 sylib ⊢∀z∈xz≠∅∧∀z∈x∀w∈xz≠w→z∩w=∅→¬∃z∈x∀v∈z∃w∈xz≠w∧v∈z∩w