Metamath Proof Explorer

Theorem kmlem16

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

Ref Expression
Hypotheses kmlem14.1 ⊢ φ ↔ z ∈ y → v ∈ x ∧ y ≠ v ∧ z ∈ v
kmlem14.2 ⊢ ψ ↔ z ∈ x → v ∈ z ∧ v ∈ y ∧ u ∈ z ∧ u ∈ y → u = v
kmlem14.3 ⊢ χ ↔ ∀ z ∈ x ∃! v v ∈ z ∩ y
Assertion kmlem16 ⊢ ∃ z ∈ x ∀ v ∈ z ∃ w ∈ x z ≠ w ∧ v ∈ z ∩ w ∨ ∃ y ¬ y ∈ x ∧ χ ↔ ∃ y ∀ z ∃ v ∀ u y ∈ x ∧ φ ∨ ¬ y ∈ x ∧ ψ

Proof

Step Hyp Ref Expression
1 kmlem14.1 ⊢ φ ↔ z ∈ y → v ∈ x ∧ y ≠ v ∧ z ∈ v
2 kmlem14.2 ⊢ ψ ↔ z ∈ x → v ∈ z ∧ v ∈ y ∧ u ∈ z ∧ u ∈ y → u = v
3 kmlem14.3 ⊢ χ ↔ ∀ z ∈ x ∃! v v ∈ z ∩ y
4 1 2 3 kmlem14 ⊢ ∃ z ∈ x ∀ v ∈ z ∃ w ∈ x z ≠ w ∧ v ∈ z ∩ w ↔ ∃ y ∀ z ∃ v ∀ u y ∈ x ∧ φ
5 1 2 3 kmlem15 ⊢ ¬ y ∈ x ∧ χ ↔ ∀ z ∃ v ∀ u ¬ y ∈ x ∧ ψ
6 5 exbii ⊢ ∃ y ¬ y ∈ x ∧ χ ↔ ∃ y ∀ z ∃ v ∀ u ¬ y ∈ x ∧ ψ
7 4 6 orbi12i ⊢ ∃ z ∈ x ∀ v ∈ z ∃ w ∈ x z ≠ w ∧ v ∈ z ∩ w ∨ ∃ y ¬ y ∈ x ∧ χ ↔ ∃ y ∀ z ∃ v ∀ u y ∈ x ∧ φ ∨ ∃ y ∀ z ∃ v ∀ u ¬ y ∈ x ∧ ψ
8 19.43 ⊢ ∃ y ∀ z ∃ v ∀ u y ∈ x ∧ φ ∨ ∀ z ∃ v ∀ u ¬ y ∈ x ∧ ψ ↔ ∃ y ∀ z ∃ v ∀ u y ∈ x ∧ φ ∨ ∃ y ∀ z ∃ v ∀ u ¬ y ∈ x ∧ ψ
9 pm3.24 ⊢ ¬ y ∈ x ∧ ¬ y ∈ x
10 simpl ⊢ y ∈ x ∧ φ → y ∈ x
11 10 sps ⊢ ∀ u y ∈ x ∧ φ → y ∈ x
12 11 exlimivv ⊢ ∃ z ∃ v ∀ u y ∈ x ∧ φ → y ∈ x
13 simpl ⊢ ¬ y ∈ x ∧ ψ → ¬ y ∈ x
14 13 sps ⊢ ∀ u ¬ y ∈ x ∧ ψ → ¬ y ∈ x
15 14 exlimivv ⊢ ∃ z ∃ v ∀ u ¬ y ∈ x ∧ ψ → ¬ y ∈ x
16 12 15 anim12i ⊢ ∃ z ∃ v ∀ u y ∈ x ∧ φ ∧ ∃ z ∃ v ∀ u ¬ y ∈ x ∧ ψ → y ∈ x ∧ ¬ y ∈ x
17 9 16 mto ⊢ ¬ ∃ z ∃ v ∀ u y ∈ x ∧ φ ∧ ∃ z ∃ v ∀ u ¬ y ∈ x ∧ ψ
18 19.33b ⊢ ¬ ∃ z ∃ v ∀ u y ∈ x ∧ φ ∧ ∃ z ∃ v ∀ u ¬ y ∈ x ∧ ψ → ∀ z ∃ v ∀ u y ∈ x ∧ φ ∨ ∃ v ∀ u ¬ y ∈ x ∧ ψ ↔ ∀ z ∃ v ∀ u y ∈ x ∧ φ ∨ ∀ z ∃ v ∀ u ¬ y ∈ x ∧ ψ
19 17 18 ax-mp ⊢ ∀ z ∃ v ∀ u y ∈ x ∧ φ ∨ ∃ v ∀ u ¬ y ∈ x ∧ ψ ↔ ∀ z ∃ v ∀ u y ∈ x ∧ φ ∨ ∀ z ∃ v ∀ u ¬ y ∈ x ∧ ψ
20 10 exlimiv ⊢ ∃ u y ∈ x ∧ φ → y ∈ x
21 13 exlimiv ⊢ ∃ u ¬ y ∈ x ∧ ψ → ¬ y ∈ x
22 20 21 anim12i ⊢ ∃ u y ∈ x ∧ φ ∧ ∃ u ¬ y ∈ x ∧ ψ → y ∈ x ∧ ¬ y ∈ x
23 9 22 mto ⊢ ¬ ∃ u y ∈ x ∧ φ ∧ ∃ u ¬ y ∈ x ∧ ψ
24 19.33b ⊢ ¬ ∃ u y ∈ x ∧ φ ∧ ∃ u ¬ y ∈ x ∧ ψ → ∀ u y ∈ x ∧ φ ∨ ¬ y ∈ x ∧ ψ ↔ ∀ u y ∈ x ∧ φ ∨ ∀ u ¬ y ∈ x ∧ ψ
25 23 24 ax-mp ⊢ ∀ u y ∈ x ∧ φ ∨ ¬ y ∈ x ∧ ψ ↔ ∀ u y ∈ x ∧ φ ∨ ∀ u ¬ y ∈ x ∧ ψ
26 25 exbii ⊢ ∃ v ∀ u y ∈ x ∧ φ ∨ ¬ y ∈ x ∧ ψ ↔ ∃ v ∀ u y ∈ x ∧ φ ∨ ∀ u ¬ y ∈ x ∧ ψ
27 19.43 ⊢ ∃ v ∀ u y ∈ x ∧ φ ∨ ∀ u ¬ y ∈ x ∧ ψ ↔ ∃ v ∀ u y ∈ x ∧ φ ∨ ∃ v ∀ u ¬ y ∈ x ∧ ψ
28 26 27 bitr2i ⊢ ∃ v ∀ u y ∈ x ∧ φ ∨ ∃ v ∀ u ¬ y ∈ x ∧ ψ ↔ ∃ v ∀ u y ∈ x ∧ φ ∨ ¬ y ∈ x ∧ ψ
29 28 albii ⊢ ∀ z ∃ v ∀ u y ∈ x ∧ φ ∨ ∃ v ∀ u ¬ y ∈ x ∧ ψ ↔ ∀ z ∃ v ∀ u y ∈ x ∧ φ ∨ ¬ y ∈ x ∧ ψ
30 19 29 bitr3i ⊢ ∀ z ∃ v ∀ u y ∈ x ∧ φ ∨ ∀ z ∃ v ∀ u ¬ y ∈ x ∧ ψ ↔ ∀ z ∃ v ∀ u y ∈ x ∧ φ ∨ ¬ y ∈ x ∧ ψ
31 30 exbii ⊢ ∃ y ∀ z ∃ v ∀ u y ∈ x ∧ φ ∨ ∀ z ∃ v ∀ u ¬ y ∈ x ∧ ψ ↔ ∃ y ∀ z ∃ v ∀ u y ∈ x ∧ φ ∨ ¬ y ∈ x ∧ ψ
32 7 8 31 3bitr2i ⊢ ∃ z ∈ x ∀ v ∈ z ∃ w ∈ x z ≠ w ∧ v ∈ z ∩ w ∨ ∃ y ¬ y ∈ x ∧ χ ↔ ∃ y ∀ z ∃ v ∀ u y ∈ x ∧ φ ∨ ¬ y ∈ x ∧ ψ