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∀ww∈z↔∃ss∈p∧if-∃nn∈sw=xw=y

Proof

Step Hyp Ref Expression
1 nfv ⊢Ⅎzif-∃nn∈sw=xw=y
2 1 axrep4 ⊢∀s∃z∀wif-∃nn∈sw=xw=y→w=z→∃z∀ww∈z↔∃ss∈p∧if-∃nn∈sw=xw=y
3 ax6evr ⊢∃zx=z
4 ifptru ⊢∃nn∈s→if-∃nn∈sw=xw=y↔w=x
5 4 biimpd ⊢∃nn∈s→if-∃nn∈sw=xw=y→w=x
6 equtrr ⊢x=z→w=x→w=z
7 5 6 sylan9r ⊢x=z∧∃nn∈s→if-∃nn∈sw=xw=y→w=z
8 7 alrimiv ⊢x=z∧∃nn∈s→∀wif-∃nn∈sw=xw=y→w=z
9 8 expcom ⊢∃nn∈s→x=z→∀wif-∃nn∈sw=xw=y→w=z
10 9 eximdv ⊢∃nn∈s→∃zx=z→∃z∀wif-∃nn∈sw=xw=y→w=z
11 3 10 mpi ⊢∃nn∈s→∃z∀wif-∃nn∈sw=xw=y→w=z
12 ax6evr ⊢∃zy=z
13 ifpfal ⊢¬∃nn∈s→if-∃nn∈sw=xw=y↔w=y
14 13 biimpd ⊢¬∃nn∈s→if-∃nn∈sw=xw=y→w=y
15 14 adantl ⊢y=z∧¬∃nn∈s→if-∃nn∈sw=xw=y→w=y
16 simpl ⊢y=z∧¬∃nn∈s→y=z
17 equtr ⊢w=y→y=z→w=z
18 15 16 17 syl6ci ⊢y=z∧¬∃nn∈s→if-∃nn∈sw=xw=y→w=z
19 18 alrimiv ⊢y=z∧¬∃nn∈s→∀wif-∃nn∈sw=xw=y→w=z
20 19 expcom ⊢¬∃nn∈s→y=z→∀wif-∃nn∈sw=xw=y→w=z
21 20 eximdv ⊢¬∃nn∈s→∃zy=z→∃z∀wif-∃nn∈sw=xw=y→w=z
22 12 21 mpi ⊢¬∃nn∈s→∃z∀wif-∃nn∈sw=xw=y→w=z
23 11 22 pm2.61i ⊢∃z∀wif-∃nn∈sw=xw=y→w=z
24 2 23 mpg ⊢∃z∀ww∈z↔∃ss∈p∧if-∃nn∈sw=xw=y