Metamath Proof Explorer

Theorem kmlem8

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

Ref Expression
Assertion kmlem8 ⊢ ¬ ∃ z ∈ u ∀ w ∈ z ψ → ∃ y ∀ z ∈ u z ≠ ∅ → ∃! w w ∈ z ∩ y ↔ ∃ z ∈ u ∀ w ∈ z ψ ∨ ∃ y ¬ y ∈ u ∧ ∀ z ∈ u ∃! w w ∈ z ∩ y

Proof

Step Hyp Ref Expression
1 ralnex ⊢ ∀ z ∈ u ¬ ∀ w ∈ z ψ ↔ ¬ ∃ z ∈ u ∀ w ∈ z ψ
2 df-rex ⊢ ∃ w ∈ z ¬ ψ ↔ ∃ w w ∈ z ∧ ¬ ψ
3 rexnal ⊢ ∃ w ∈ z ¬ ψ ↔ ¬ ∀ w ∈ z ψ
4 2 3 bitr3i ⊢ ∃ w w ∈ z ∧ ¬ ψ ↔ ¬ ∀ w ∈ z ψ
5 exsimpl ⊢ ∃ w w ∈ z ∧ ¬ ψ → ∃ w w ∈ z
6 n0 ⊢ z ≠ ∅ ↔ ∃ w w ∈ z
7 5 6 sylibr ⊢ ∃ w w ∈ z ∧ ¬ ψ → z ≠ ∅
8 4 7 sylbir ⊢ ¬ ∀ w ∈ z ψ → z ≠ ∅
9 8 ralimi ⊢ ∀ z ∈ u ¬ ∀ w ∈ z ψ → ∀ z ∈ u z ≠ ∅
10 1 9 sylbir ⊢ ¬ ∃ z ∈ u ∀ w ∈ z ψ → ∀ z ∈ u z ≠ ∅
11 kmlem2 ⊢ ∃ y ∀ z ∈ u z ≠ ∅ → ∃! w w ∈ z ∩ y ↔ ∃ y ¬ y ∈ u ∧ ∀ z ∈ u z ≠ ∅ → ∃! w w ∈ z ∩ y
12 biimt ⊢ z ≠ ∅ → ∃! w w ∈ z ∩ y ↔ z ≠ ∅ → ∃! w w ∈ z ∩ y
13 12 ralimi ⊢ ∀ z ∈ u z ≠ ∅ → ∀ z ∈ u ∃! w w ∈ z ∩ y ↔ z ≠ ∅ → ∃! w w ∈ z ∩ y
14 ralbi ⊢ ∀ z ∈ u ∃! w w ∈ z ∩ y ↔ z ≠ ∅ → ∃! w w ∈ z ∩ y → ∀ z ∈ u ∃! w w ∈ z ∩ y ↔ ∀ z ∈ u z ≠ ∅ → ∃! w w ∈ z ∩ y
15 13 14 syl ⊢ ∀ z ∈ u z ≠ ∅ → ∀ z ∈ u ∃! w w ∈ z ∩ y ↔ ∀ z ∈ u z ≠ ∅ → ∃! w w ∈ z ∩ y
16 15 anbi2d ⊢ ∀ z ∈ u z ≠ ∅ → ¬ y ∈ u ∧ ∀ z ∈ u ∃! w w ∈ z ∩ y ↔ ¬ y ∈ u ∧ ∀ z ∈ u z ≠ ∅ → ∃! w w ∈ z ∩ y
17 16 exbidv ⊢ ∀ z ∈ u z ≠ ∅ → ∃ y ¬ y ∈ u ∧ ∀ z ∈ u ∃! w w ∈ z ∩ y ↔ ∃ y ¬ y ∈ u ∧ ∀ z ∈ u z ≠ ∅ → ∃! w w ∈ z ∩ y
18 11 17 bitr4id ⊢ ∀ z ∈ u z ≠ ∅ → ∃ y ∀ z ∈ u z ≠ ∅ → ∃! w w ∈ z ∩ y ↔ ∃ y ¬ y ∈ u ∧ ∀ z ∈ u ∃! w w ∈ z ∩ y
19 10 18 syl ⊢ ¬ ∃ z ∈ u ∀ w ∈ z ψ → ∃ y ∀ z ∈ u z ≠ ∅ → ∃! w w ∈ z ∩ y ↔ ∃ y ¬ y ∈ u ∧ ∀ z ∈ u ∃! w w ∈ z ∩ y
20 19 pm5.74i ⊢ ¬ ∃ z ∈ u ∀ w ∈ z ψ → ∃ y ∀ z ∈ u z ≠ ∅ → ∃! w w ∈ z ∩ y ↔ ¬ ∃ z ∈ u ∀ w ∈ z ψ → ∃ y ¬ y ∈ u ∧ ∀ z ∈ u ∃! w w ∈ z ∩ y
21 pm4.64 ⊢ ¬ ∃ z ∈ u ∀ w ∈ z ψ → ∃ y ¬ y ∈ u ∧ ∀ z ∈ u ∃! w w ∈ z ∩ y ↔ ∃ z ∈ u ∀ w ∈ z ψ ∨ ∃ y ¬ y ∈ u ∧ ∀ z ∈ u ∃! w w ∈ z ∩ y
22 20 21 bitri ⊢ ¬ ∃ z ∈ u ∀ w ∈ z ψ → ∃ y ∀ z ∈ u z ≠ ∅ → ∃! w w ∈ z ∩ y ↔ ∃ z ∈ u ∀ w ∈ z ψ ∨ ∃ y ¬ y ∈ u ∧ ∀ z ∈ u ∃! w w ∈ z ∩ y