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∃!vv∈z∩y
Assertion kmlem16 ⊢∃z∈x∀v∈z∃w∈xz≠w∧v∈z∩w∨∃y¬y∈x∧χ↔∃y∀z∃v∀uy∈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∃!vv∈z∩y
4 1 2 3 kmlem14 ⊢∃z∈x∀v∈z∃w∈xz≠w∧v∈z∩w↔∃y∀z∃v∀uy∈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∈xz≠w∧v∈z∩w∨∃y¬y∈x∧χ↔∃y∀z∃v∀uy∈x∧φ∨∃y∀z∃v∀u¬y∈x∧ψ
8 19.43 ⊢∃y∀z∃v∀uy∈x∧φ∨∀z∃v∀u¬y∈x∧ψ↔∃y∀z∃v∀uy∈x∧φ∨∃y∀z∃v∀u¬y∈x∧ψ
9 pm3.24 ⊢¬y∈x∧¬y∈x
10 simpl ⊢y∈x∧φ→y∈x
11 10 sps ⊢∀uy∈x∧φ→y∈x
12 11 exlimivv ⊢∃z∃v∀uy∈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∀uy∈x∧φ∧∃z∃v∀u¬y∈x∧ψ→y∈x∧¬y∈x
17 9 16 mto ⊢¬∃z∃v∀uy∈x∧φ∧∃z∃v∀u¬y∈x∧ψ
18 19.33b ⊢¬∃z∃v∀uy∈x∧φ∧∃z∃v∀u¬y∈x∧ψ→∀z∃v∀uy∈x∧φ∨∃v∀u¬y∈x∧ψ↔∀z∃v∀uy∈x∧φ∨∀z∃v∀u¬y∈x∧ψ
19 17 18 ax-mp ⊢∀z∃v∀uy∈x∧φ∨∃v∀u¬y∈x∧ψ↔∀z∃v∀uy∈x∧φ∨∀z∃v∀u¬y∈x∧ψ
20 10 exlimiv ⊢∃uy∈x∧φ→y∈x
21 13 exlimiv ⊢∃u¬y∈x∧ψ→¬y∈x
22 20 21 anim12i ⊢∃uy∈x∧φ∧∃u¬y∈x∧ψ→y∈x∧¬y∈x
23 9 22 mto ⊢¬∃uy∈x∧φ∧∃u¬y∈x∧ψ
24 19.33b ⊢¬∃uy∈x∧φ∧∃u¬y∈x∧ψ→∀uy∈x∧φ∨¬y∈x∧ψ↔∀uy∈x∧φ∨∀u¬y∈x∧ψ
25 23 24 ax-mp ⊢∀uy∈x∧φ∨¬y∈x∧ψ↔∀uy∈x∧φ∨∀u¬y∈x∧ψ
26 25 exbii ⊢∃v∀uy∈x∧φ∨¬y∈x∧ψ↔∃v∀uy∈x∧φ∨∀u¬y∈x∧ψ
27 19.43 ⊢∃v∀uy∈x∧φ∨∀u¬y∈x∧ψ↔∃v∀uy∈x∧φ∨∃v∀u¬y∈x∧ψ
28 26 27 bitr2i ⊢∃v∀uy∈x∧φ∨∃v∀u¬y∈x∧ψ↔∃v∀uy∈x∧φ∨¬y∈x∧ψ
29 28 albii ⊢∀z∃v∀uy∈x∧φ∨∃v∀u¬y∈x∧ψ↔∀z∃v∀uy∈x∧φ∨¬y∈x∧ψ
30 19 29 bitr3i ⊢∀z∃v∀uy∈x∧φ∨∀z∃v∀u¬y∈x∧ψ↔∀z∃v∀uy∈x∧φ∨¬y∈x∧ψ
31 30 exbii ⊢∃y∀z∃v∀uy∈x∧φ∨∀z∃v∀u¬y∈x∧ψ↔∃y∀z∃v∀uy∈x∧φ∨¬y∈x∧ψ
32 7 8 31 3bitr2i ⊢∃z∈x∀v∈z∃w∈xz≠w∧v∈z∩w∨∃y¬y∈x∧χ↔∃y∀z∃v∀uy∈x∧φ∨¬y∈x∧ψ