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

Theorem axprlem4 5218
Description: Lemma for axpr 5220. The first element of the pair is included in any superset of the set whose existence is asserted by the axiom of replacement. (Contributed by Rohan Ridenour, 10-Aug-2023.) (Revised by BJ, 13-Aug-2023.)
Assertion
Ref Expression
axprlem4 ((∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑥) → ∃𝑠(𝑠𝑝 ∧ if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))
Distinct variable groups:   𝑥,𝑠   𝑤,𝑠   𝑡,𝑛,𝑠

Proof of Theorem axprlem4
StepHypRef Expression
1 axprlem1 5215 . . 3 𝑠𝑛(∀𝑡 ¬ 𝑡𝑛𝑛𝑠)
21bm1.3ii 5097 . 2 𝑠𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛)
3 nfa1 2121 . . . 4 𝑠𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝)
4 nfv 1892 . . . 4 𝑠 𝑤 = 𝑥
53, 4nfan 1881 . . 3 𝑠(∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑥)
6 biimp 216 . . . . . . . . 9 ((𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) → (𝑛𝑠 → ∀𝑡 ¬ 𝑡𝑛))
76alimi 1793 . . . . . . . 8 (∀𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) → ∀𝑛(𝑛𝑠 → ∀𝑡 ¬ 𝑡𝑛))
8 df-ral 3110 . . . . . . . 8 (∀𝑛𝑠𝑡 ¬ 𝑡𝑛 ↔ ∀𝑛(𝑛𝑠 → ∀𝑡 ¬ 𝑡𝑛))
97, 8sylibr 235 . . . . . . 7 (∀𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) → ∀𝑛𝑠𝑡 ¬ 𝑡𝑛)
10 sp 2146 . . . . . . 7 (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) → (∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝))
119, 10mpan9 507 . . . . . 6 ((∀𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) ∧ ∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝)) → 𝑠𝑝)
1211adantrr 713 . . . . 5 ((∀𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑥)) → 𝑠𝑝)
13 ax-nul 5101 . . . . . . 7 𝑛𝑡 ¬ 𝑡𝑛
14 nfa1 2121 . . . . . . . 8 𝑛𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛)
15 sp 2146 . . . . . . . . 9 (∀𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) → (𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛))
1615biimprd 249 . . . . . . . 8 (∀𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) → (∀𝑡 ¬ 𝑡𝑛𝑛𝑠))
1714, 16eximd 2181 . . . . . . 7 (∀𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) → (∃𝑛𝑡 ¬ 𝑡𝑛 → ∃𝑛 𝑛𝑠))
1813, 17mpi 20 . . . . . 6 (∀𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) → ∃𝑛 𝑛𝑠)
19 simprr 769 . . . . . 6 ((∀𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑥)) → 𝑤 = 𝑥)
20 ifptru 1066 . . . . . . 7 (∃𝑛 𝑛𝑠 → (if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦) ↔ 𝑤 = 𝑥))
2120biimpar 478 . . . . . 6 ((∃𝑛 𝑛𝑠𝑤 = 𝑥) → if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))
2218, 19, 21syl2an2r 681 . . . . 5 ((∀𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑥)) → if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))
2312, 22jca 512 . . . 4 ((∀𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑥)) → (𝑠𝑝 ∧ if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))
2423expcom 414 . . 3 ((∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑥) → (∀𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) → (𝑠𝑝 ∧ if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
255, 24eximd 2181 . 2 ((∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑥) → (∃𝑠𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) → ∃𝑠(𝑠𝑝 ∧ if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
262, 25mpi 20 1 ((∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑥) → ∃𝑠(𝑠𝑝 ∧ if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  if-wif 1055  wal 1520  wex 1761  wral 3105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-9 2091  ax-10 2112  ax-12 2141  ax-sep 5094  ax-nul 5101  ax-pow 5157
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-ifp 1056  df-tru 1525  df-ex 1762  df-nf 1766  df-ral 3110
This theorem is referenced by:  axpr  5220
  Copyright terms: Public domain W3C validator