MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  axprlem3 Structured version   Visualization version   GIF version

Theorem axprlem3 5431
Description: Lemma for axpr 5433. Eliminate the antecedent of the relevant replacement instance. (Contributed by Rohan Ridenour, 10-Aug-2023.) (Proof shortened by Matthew House, 18-Sep-2025.)
Assertion
Ref Expression
axprlem3 𝑧𝑤(𝑤𝑧 ↔ ∃𝑠(𝑠𝑝 ∧ if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))
Distinct variable groups:   𝑥,𝑧,𝑤   𝑦,𝑧,𝑤   𝑧,𝑛,𝑤   𝑧,𝑠,𝑝,𝑤

Proof of Theorem axprlem3
StepHypRef Expression
1 axrep4v 5290 . 2 (∀𝑠𝑧𝑤(if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦) → 𝑤 = 𝑧) → ∃𝑧𝑤(𝑤𝑧 ↔ ∃𝑠(𝑠𝑝 ∧ if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
2 ifptru 1074 . . . . . . 7 (∃𝑛 𝑛𝑠 → (if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦) ↔ 𝑤 = 𝑥))
32biimpd 229 . . . . . 6 (∃𝑛 𝑛𝑠 → (if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦) → 𝑤 = 𝑥))
4 equeuclr 2020 . . . . . 6 (𝑧 = 𝑥 → (𝑤 = 𝑥𝑤 = 𝑧))
53, 4syl9r 78 . . . . 5 (𝑧 = 𝑥 → (∃𝑛 𝑛𝑠 → (if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦) → 𝑤 = 𝑧)))
65alrimdv 1927 . . . 4 (𝑧 = 𝑥 → (∃𝑛 𝑛𝑠 → ∀𝑤(if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦) → 𝑤 = 𝑧)))
76spimevw 1992 . . 3 (∃𝑛 𝑛𝑠 → ∃𝑧𝑤(if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦) → 𝑤 = 𝑧))
8 ifpfal 1075 . . . . . . 7 (¬ ∃𝑛 𝑛𝑠 → (if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦) ↔ 𝑤 = 𝑦))
98biimpd 229 . . . . . 6 (¬ ∃𝑛 𝑛𝑠 → (if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦) → 𝑤 = 𝑦))
10 equeuclr 2020 . . . . . 6 (𝑧 = 𝑦 → (𝑤 = 𝑦𝑤 = 𝑧))
119, 10syl9r 78 . . . . 5 (𝑧 = 𝑦 → (¬ ∃𝑛 𝑛𝑠 → (if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦) → 𝑤 = 𝑧)))
1211alrimdv 1927 . . . 4 (𝑧 = 𝑦 → (¬ ∃𝑛 𝑛𝑠 → ∀𝑤(if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦) → 𝑤 = 𝑧)))
1312spimevw 1992 . . 3 (¬ ∃𝑛 𝑛𝑠 → ∃𝑧𝑤(if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦) → 𝑤 = 𝑧))
147, 13pm2.61i 182 . 2 𝑧𝑤(if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦) → 𝑤 = 𝑧)
151, 14mpg 1794 1 𝑧𝑤(𝑤𝑧 ↔ ∃𝑠(𝑠𝑝 ∧ if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  if-wif 1062  wal 1535  wex 1776
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-rep 5285
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ifp 1063  df-ex 1777
This theorem is referenced by:  axpr  5433
  Copyright terms: Public domain W3C validator