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

Theorem axprlem4 5295
Description: Lemma for axpr 5297. 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 5292 . . 3 𝑠𝑛(∀𝑡 ¬ 𝑡𝑛𝑛𝑠)
21bm1.3ii 5173 . 2 𝑠𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛)
3 nfa1 2153 . . . 4 𝑠𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝)
4 nfv 1915 . . . 4 𝑠 𝑤 = 𝑥
53, 4nfan 1900 . . 3 𝑠(∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑥)
6 biimp 218 . . . . . . . . 9 ((𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) → (𝑛𝑠 → ∀𝑡 ¬ 𝑡𝑛))
76alimi 1813 . . . . . . . 8 (∀𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) → ∀𝑛(𝑛𝑠 → ∀𝑡 ¬ 𝑡𝑛))
8 df-ral 3114 . . . . . . . 8 (∀𝑛𝑠𝑡 ¬ 𝑡𝑛 ↔ ∀𝑛(𝑛𝑠 → ∀𝑡 ¬ 𝑡𝑛))
97, 8sylibr 237 . . . . . . 7 (∀𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) → ∀𝑛𝑠𝑡 ¬ 𝑡𝑛)
10 sp 2181 . . . . . . 7 (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) → (∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝))
119, 10mpan9 510 . . . . . 6 ((∀𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) ∧ ∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝)) → 𝑠𝑝)
1211adantrr 716 . . . . 5 ((∀𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑥)) → 𝑠𝑝)
13 ax-nul 5177 . . . . . . 7 𝑛𝑡 ¬ 𝑡𝑛
14 nfa1 2153 . . . . . . . 8 𝑛𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛)
15 sp 2181 . . . . . . . . 9 (∀𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) → (𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛))
1615biimprd 251 . . . . . . . 8 (∀𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) → (∀𝑡 ¬ 𝑡𝑛𝑛𝑠))
1714, 16eximd 2215 . . . . . . 7 (∀𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) → (∃𝑛𝑡 ¬ 𝑡𝑛 → ∃𝑛 𝑛𝑠))
1813, 17mpi 20 . . . . . 6 (∀𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) → ∃𝑛 𝑛𝑠)
19 simprr 772 . . . . . 6 ((∀𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑥)) → 𝑤 = 𝑥)
20 ifptru 1071 . . . . . . 7 (∃𝑛 𝑛𝑠 → (if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦) ↔ 𝑤 = 𝑥))
2120biimpar 481 . . . . . 6 ((∃𝑛 𝑛𝑠𝑤 = 𝑥) → if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))
2218, 19, 21syl2an2r 684 . . . . 5 ((∀𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑥)) → if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))
2312, 22jca 515 . . . 4 ((∀𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑥)) → (𝑠𝑝 ∧ if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))
2423expcom 417 . . 3 ((∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑥) → (∀𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) → (𝑠𝑝 ∧ if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
255, 24eximd 2215 . 2 ((∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑥) → (∃𝑠𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) → ∃𝑠(𝑠𝑝 ∧ if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
262, 25mpi 20 1 ((∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑥) → ∃𝑠(𝑠𝑝 ∧ if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  if-wif 1058  wal 1536  wex 1781  wral 3109
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2122  ax-10 2143  ax-12 2176  ax-sep 5170  ax-nul 5177  ax-pow 5234
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ifp 1059  df-tru 1541  df-ex 1782  df-nf 1786  df-ral 3114
This theorem is referenced by:  axpr  5297
  Copyright terms: Public domain W3C validator