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

Theorem axprlem4OLD 5434
Description: Obsolete version of axprlem4 5431 as of 18-Sep-2025. (Contributed by Rohan Ridenour, 10-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
axprlem4OLD ((∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑥) → ∃𝑠(𝑠𝑝 ∧ if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))
Distinct variable groups:   𝑥,𝑠   𝑤,𝑠   𝑡,𝑛,𝑠

Proof of Theorem axprlem4OLD
StepHypRef Expression
1 axprlem1 5428 . . 3 𝑠𝑛(∀𝑡 ¬ 𝑡𝑛𝑛𝑠)
21bm1.3iiOLD 5307 . 2 𝑠𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛)
3 nfa1 2148 . . . 4 𝑠𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝)
4 nfv 1911 . . . 4 𝑠 𝑤 = 𝑥
53, 4nfan 1896 . . 3 𝑠(∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑥)
6 biimp 215 . . . . . . . . 9 ((𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) → (𝑛𝑠 → ∀𝑡 ¬ 𝑡𝑛))
76alimi 1807 . . . . . . . 8 (∀𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) → ∀𝑛(𝑛𝑠 → ∀𝑡 ¬ 𝑡𝑛))
8 df-ral 3059 . . . . . . . 8 (∀𝑛𝑠𝑡 ¬ 𝑡𝑛 ↔ ∀𝑛(𝑛𝑠 → ∀𝑡 ¬ 𝑡𝑛))
97, 8sylibr 234 . . . . . . 7 (∀𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) → ∀𝑛𝑠𝑡 ¬ 𝑡𝑛)
10 sp 2180 . . . . . . 7 (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) → (∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝))
119, 10mpan9 506 . . . . . 6 ((∀𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) ∧ ∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝)) → 𝑠𝑝)
1211adantrr 717 . . . . 5 ((∀𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑥)) → 𝑠𝑝)
13 ax-nul 5311 . . . . . . 7 𝑛𝑡 ¬ 𝑡𝑛
14 nfa1 2148 . . . . . . . 8 𝑛𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛)
15 sp 2180 . . . . . . . . 9 (∀𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) → (𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛))
1615biimprd 248 . . . . . . . 8 (∀𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) → (∀𝑡 ¬ 𝑡𝑛𝑛𝑠))
1714, 16eximd 2213 . . . . . . 7 (∀𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) → (∃𝑛𝑡 ¬ 𝑡𝑛 → ∃𝑛 𝑛𝑠))
1813, 17mpi 20 . . . . . 6 (∀𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) → ∃𝑛 𝑛𝑠)
19 simprr 773 . . . . . 6 ((∀𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑥)) → 𝑤 = 𝑥)
20 ifptru 1074 . . . . . . 7 (∃𝑛 𝑛𝑠 → (if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦) ↔ 𝑤 = 𝑥))
2120biimpar 477 . . . . . 6 ((∃𝑛 𝑛𝑠𝑤 = 𝑥) → if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))
2218, 19, 21syl2an2r 685 . . . . 5 ((∀𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑥)) → if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))
2312, 22jca 511 . . . 4 ((∀𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑥)) → (𝑠𝑝 ∧ if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))
2423expcom 413 . . 3 ((∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑥) → (∀𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) → (𝑠𝑝 ∧ if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
255, 24eximd 2213 . 2 ((∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑥) → (∃𝑠𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) → ∃𝑠(𝑠𝑝 ∧ if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
262, 25mpi 20 1 ((∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑥) → ∃𝑠(𝑠𝑝 ∧ if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  if-wif 1062  wal 1534  wex 1775  wral 3058
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-10 2138  ax-12 2174  ax-sep 5301  ax-nul 5311  ax-pow 5370
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ifp 1063  df-tru 1539  df-ex 1776  df-nf 1780  df-ral 3059
This theorem is referenced by:  axprOLD  5436
  Copyright terms: Public domain W3C validator