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

Theorem axprlem4 5373
Description: Lemma for axpr 5375. 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 5370 . . 3 𝑠𝑛(∀𝑡 ¬ 𝑡𝑛𝑛𝑠)
21bm1.3ii 5250 . 2 𝑠𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛)
3 nfa1 2148 . . . 4 𝑠𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝)
4 nfv 1917 . . . 4 𝑠 𝑤 = 𝑥
53, 4nfan 1902 . . 3 𝑠(∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑥)
6 biimp 214 . . . . . . . . 9 ((𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) → (𝑛𝑠 → ∀𝑡 ¬ 𝑡𝑛))
76alimi 1813 . . . . . . . 8 (∀𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) → ∀𝑛(𝑛𝑠 → ∀𝑡 ¬ 𝑡𝑛))
8 df-ral 3063 . . . . . . . 8 (∀𝑛𝑠𝑡 ¬ 𝑡𝑛 ↔ ∀𝑛(𝑛𝑠 → ∀𝑡 ¬ 𝑡𝑛))
97, 8sylibr 233 . . . . . . 7 (∀𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) → ∀𝑛𝑠𝑡 ¬ 𝑡𝑛)
10 sp 2176 . . . . . . 7 (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) → (∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝))
119, 10mpan9 508 . . . . . 6 ((∀𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) ∧ ∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝)) → 𝑠𝑝)
1211adantrr 715 . . . . 5 ((∀𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑥)) → 𝑠𝑝)
13 ax-nul 5254 . . . . . . 7 𝑛𝑡 ¬ 𝑡𝑛
14 nfa1 2148 . . . . . . . 8 𝑛𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛)
15 sp 2176 . . . . . . . . 9 (∀𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) → (𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛))
1615biimprd 248 . . . . . . . 8 (∀𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) → (∀𝑡 ¬ 𝑡𝑛𝑛𝑠))
1714, 16eximd 2209 . . . . . . 7 (∀𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) → (∃𝑛𝑡 ¬ 𝑡𝑛 → ∃𝑛 𝑛𝑠))
1813, 17mpi 20 . . . . . 6 (∀𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) → ∃𝑛 𝑛𝑠)
19 simprr 771 . . . . . 6 ((∀𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑥)) → 𝑤 = 𝑥)
20 ifptru 1074 . . . . . . 7 (∃𝑛 𝑛𝑠 → (if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦) ↔ 𝑤 = 𝑥))
2120biimpar 479 . . . . . 6 ((∃𝑛 𝑛𝑠𝑤 = 𝑥) → if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))
2218, 19, 21syl2an2r 683 . . . . 5 ((∀𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑥)) → if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))
2312, 22jca 513 . . . 4 ((∀𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑥)) → (𝑠𝑝 ∧ if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))
2423expcom 415 . . 3 ((∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑥) → (∀𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) → (𝑠𝑝 ∧ if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
255, 24eximd 2209 . 2 ((∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑥) → (∃𝑠𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) → ∃𝑠(𝑠𝑝 ∧ if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
262, 25mpi 20 1 ((∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑥) → ∃𝑠(𝑠𝑝 ∧ if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397  if-wif 1061  wal 1539  wex 1781  wral 3062
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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-10 2137  ax-12 2171  ax-sep 5247  ax-nul 5254  ax-pow 5312
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-ifp 1062  df-tru 1544  df-ex 1782  df-nf 1786  df-ral 3063
This theorem is referenced by:  axpr  5375
  Copyright terms: Public domain W3C validator