Metamath Proof Explorer

Theorem axprlem3

Description: Lemma for axpr . Eliminate the antecedent of the relevant replacement instance. (Contributed by Rohan Ridenour, 10-Aug-2023)

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 nfv ⊢ Ⅎ z if- ∃ n n ∈ s w = x w = y
2 1 axrep4 ⊢ ∀ 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
3 ax6evr ⊢ ∃ z x = z
4 ifptru ⊢ ∃ n n ∈ s → if- ∃ n n ∈ s w = x w = y ↔ w = x
5 4 biimpd ⊢ ∃ n n ∈ s → if- ∃ n n ∈ s w = x w = y → w = x
6 equtrr ⊢ x = z → w = x → w = z
7 5 6 sylan9r ⊢ x = z ∧ ∃ n n ∈ s → if- ∃ n n ∈ s w = x w = y → w = z
8 7 alrimiv ⊢ x = z ∧ ∃ n n ∈ s → ∀ w if- ∃ n n ∈ s w = x w = y → w = z
9 8 expcom ⊢ ∃ n n ∈ s → x = z → ∀ w if- ∃ n n ∈ s w = x w = y → w = z
10 9 eximdv ⊢ ∃ n n ∈ s → ∃ z x = z → ∃ z ∀ w if- ∃ n n ∈ s w = x w = y → w = z
11 3 10 mpi ⊢ ∃ n n ∈ s → ∃ z ∀ w if- ∃ n n ∈ s w = x w = y → w = z
12 ax6evr ⊢ ∃ z y = z
13 ifpfal ⊢ ¬ ∃ n n ∈ s → if- ∃ n n ∈ s w = x w = y ↔ w = y
14 13 biimpd ⊢ ¬ ∃ n n ∈ s → if- ∃ n n ∈ s w = x w = y → w = y
15 14 adantl ⊢ y = z ∧ ¬ ∃ n n ∈ s → if- ∃ n n ∈ s w = x w = y → w = y
16 simpl ⊢ y = z ∧ ¬ ∃ n n ∈ s → y = z
17 equtr ⊢ w = y → y = z → w = z
18 15 16 17 syl6ci ⊢ y = z ∧ ¬ ∃ n n ∈ s → if- ∃ n n ∈ s w = x w = y → w = z
19 18 alrimiv ⊢ y = z ∧ ¬ ∃ n n ∈ s → ∀ w if- ∃ n n ∈ s w = x w = y → w = z
20 19 expcom ⊢ ¬ ∃ n n ∈ s → y = z → ∀ w if- ∃ n n ∈ s w = x w = y → w = z
21 20 eximdv ⊢ ¬ ∃ n n ∈ s → ∃ z y = z → ∃ z ∀ w if- ∃ n n ∈ s w = x w = y → w = z
22 12 21 mpi ⊢ ¬ ∃ n n ∈ s → ∃ z ∀ w if- ∃ n n ∈ s w = x w = y → w = z
23 11 22 pm2.61i ⊢ ∃ z ∀ w if- ∃ n n ∈ s w = x w = y → w = z
24 2 23 mpg ⊢ ∃ z ∀ w w ∈ z ↔ ∃ s s ∈ p ∧ if- ∃ n n ∈ s w = x w = y