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

Proof

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