This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem axprOLD

Description: Obsolete version of axpr as of 18-Sep-2025. (Contributed by NM, 14-Nov-2006) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion axprOLD ⊢ ∃ z ∀ w w = x ∨ w = y → w ∈ z

Proof

Step Hyp Ref Expression
1 axprlem3OLD ⊢ ∃ z ∀ w w ∈ z ↔ ∃ s s ∈ p ∧ if- ∃ n n ∈ s w = x w = y
2 biimpr ⊢ w ∈ z ↔ ∃ s s ∈ p ∧ if- ∃ n n ∈ s w = x w = y → ∃ s s ∈ p ∧ if- ∃ n n ∈ s w = x w = y → w ∈ z
3 2 alimi ⊢ ∀ w w ∈ z ↔ ∃ s s ∈ p ∧ if- ∃ n n ∈ s w = x w = y → ∀ w ∃ s s ∈ p ∧ if- ∃ n n ∈ s w = x w = y → w ∈ z
4 1 3 eximii ⊢ ∃ z ∀ w ∃ s s ∈ p ∧ if- ∃ n n ∈ s w = x w = y → w ∈ z
5 axprlem4OLD ⊢ ∀ s ∀ n ∈ s ∀ t ¬ t ∈ n → s ∈ p ∧ w = x → ∃ s s ∈ p ∧ if- ∃ n n ∈ s w = x w = y
6 axprlem5OLD ⊢ ∀ s ∀ n ∈ s ∀ t ¬ t ∈ n → s ∈ p ∧ w = y → ∃ s s ∈ p ∧ if- ∃ n n ∈ s w = x w = y
7 5 6 jaodan ⊢ ∀ s ∀ n ∈ s ∀ t ¬ t ∈ n → s ∈ p ∧ w = x ∨ w = y → ∃ s s ∈ p ∧ if- ∃ n n ∈ s w = x w = y
8 7 ex ⊢ ∀ s ∀ n ∈ s ∀ t ¬ t ∈ n → s ∈ p → w = x ∨ w = y → ∃ s s ∈ p ∧ if- ∃ n n ∈ s w = x w = y
9 8 imim1d ⊢ ∀ s ∀ n ∈ s ∀ t ¬ t ∈ n → s ∈ p → ∃ s s ∈ p ∧ if- ∃ n n ∈ s w = x w = y → w ∈ z → w = x ∨ w = y → w ∈ z
10 9 alimdv ⊢ ∀ s ∀ n ∈ s ∀ t ¬ t ∈ n → s ∈ p → ∀ w ∃ s s ∈ p ∧ if- ∃ n n ∈ s w = x w = y → w ∈ z → ∀ w w = x ∨ w = y → w ∈ z
11 10 eximdv ⊢ ∀ s ∀ n ∈ s ∀ t ¬ t ∈ n → s ∈ p → ∃ z ∀ w ∃ s s ∈ p ∧ if- ∃ n n ∈ s w = x w = y → w ∈ z → ∃ z ∀ w w = x ∨ w = y → w ∈ z
12 4 11 mpi ⊢ ∀ s ∀ n ∈ s ∀ t ¬ t ∈ n → s ∈ p → ∃ z ∀ w w = x ∨ w = y → w ∈ z
13 axprlem2 ⊢ ∃ p ∀ s ∀ n ∈ s ∀ t ¬ t ∈ n → s ∈ p
14 12 13 exlimiiv ⊢ ∃ z ∀ w w = x ∨ w = y → w ∈ z