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

Metamath Proof Explorer

Theorem axprlem3

Description: Lemma for axpr . Eliminate the antecedent of the relevant replacement instance. (Contributed by Rohan Ridenour, 10-Aug-2023) (Proof shortened by Matthew House, 18-Sep-2025)

Ref Expression
Assertion axprlem3 ⊢ ∃ z ∀ w w ∈ z ↔ ∃ s s ∈ p ∧ if- ∃ n n ∈ s w = x w = y

Proof

Step Hyp Ref Expression
1 axrep4v ⊢ ∀ s ∃ z ∀ w if- ∃ n n ∈ s w = x w = y → w = z → ∃ z ∀ w w ∈ z ↔ ∃ s s ∈ p ∧ if- ∃ n n ∈ s w = x w = y
2 ifptru ⊢ ∃ n n ∈ s → if- ∃ n n ∈ s w = x w = y ↔ w = x
3 2 biimpd ⊢ ∃ n n ∈ s → if- ∃ n n ∈ s w = x w = y → w = x
4 equeuclr ⊢ z = x → w = x → w = z
5 3 4 syl9r ⊢ z = x → ∃ n n ∈ s → if- ∃ n n ∈ s w = x w = y → w = z
6 5 alrimdv ⊢ z = x → ∃ n n ∈ s → ∀ w if- ∃ n n ∈ s w = x w = y → w = z
7 6 spimevw ⊢ ∃ n n ∈ s → ∃ z ∀ w if- ∃ n n ∈ s w = x w = y → w = z
8 ifpfal ⊢ ¬ ∃ n n ∈ s → if- ∃ n n ∈ s w = x w = y ↔ w = y
9 8 biimpd ⊢ ¬ ∃ n n ∈ s → if- ∃ n n ∈ s w = x w = y → w = y
10 equeuclr ⊢ z = y → w = y → w = z
11 9 10 syl9r ⊢ z = y → ¬ ∃ n n ∈ s → if- ∃ n n ∈ s w = x w = y → w = z
12 11 alrimdv ⊢ z = y → ¬ ∃ n n ∈ s → ∀ w if- ∃ n n ∈ s w = x w = y → w = z
13 12 spimevw ⊢ ¬ ∃ n n ∈ s → ∃ z ∀ w if- ∃ n n ∈ s w = x w = y → w = z
14 7 13 pm2.61i ⊢ ∃ z ∀ w if- ∃ n n ∈ s w = x w = y → w = z
15 1 14 mpg ⊢ ∃ z ∀ w w ∈ z ↔ ∃ s s ∈ p ∧ if- ∃ n n ∈ s w = x w = y