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

Theorem axprlem5 5293
Description: Lemma for axpr 5294. The second 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
axprlem5 ((∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦) → ∃𝑠(𝑠𝑝 ∧ if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))
Distinct variable groups:   𝑦,𝑠   𝑤,𝑠   𝑛,𝑠

Proof of Theorem axprlem5
StepHypRef Expression
1 ax-nul 5174 . 2 𝑠𝑛 ¬ 𝑛𝑠
2 nfa1 2152 . . . 4 𝑠𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝)
3 nfv 1915 . . . 4 𝑠 𝑤 = 𝑦
42, 3nfan 1900 . . 3 𝑠(∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦)
5 pm2.21 123 . . . . . . . . 9 𝑛𝑠 → (𝑛𝑠 → ∀𝑡 ¬ 𝑡𝑛))
65alimi 1813 . . . . . . . 8 (∀𝑛 ¬ 𝑛𝑠 → ∀𝑛(𝑛𝑠 → ∀𝑡 ¬ 𝑡𝑛))
76adantr 484 . . . . . . 7 ((∀𝑛 ¬ 𝑛𝑠 ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦)) → ∀𝑛(𝑛𝑠 → ∀𝑡 ¬ 𝑡𝑛))
8 df-ral 3111 . . . . . . 7 (∀𝑛𝑠𝑡 ¬ 𝑡𝑛 ↔ ∀𝑛(𝑛𝑠 → ∀𝑡 ¬ 𝑡𝑛))
97, 8sylibr 237 . . . . . 6 ((∀𝑛 ¬ 𝑛𝑠 ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦)) → ∀𝑛𝑠𝑡 ¬ 𝑡𝑛)
10 sp 2180 . . . . . . 7 (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) → (∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝))
1110ad2antrl 727 . . . . . 6 ((∀𝑛 ¬ 𝑛𝑠 ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦)) → (∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝))
129, 11mpd 15 . . . . 5 ((∀𝑛 ¬ 𝑛𝑠 ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦)) → 𝑠𝑝)
13 simpl 486 . . . . . . 7 ((∀𝑛 ¬ 𝑛𝑠 ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦)) → ∀𝑛 ¬ 𝑛𝑠)
14 alnex 1783 . . . . . . 7 (∀𝑛 ¬ 𝑛𝑠 ↔ ¬ ∃𝑛 𝑛𝑠)
1513, 14sylib 221 . . . . . 6 ((∀𝑛 ¬ 𝑛𝑠 ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦)) → ¬ ∃𝑛 𝑛𝑠)
16 simprr 772 . . . . . 6 ((∀𝑛 ¬ 𝑛𝑠 ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦)) → 𝑤 = 𝑦)
17 ifpfal 1072 . . . . . . 7 (¬ ∃𝑛 𝑛𝑠 → (if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦) ↔ 𝑤 = 𝑦))
1817biimpar 481 . . . . . 6 ((¬ ∃𝑛 𝑛𝑠𝑤 = 𝑦) → if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))
1915, 16, 18syl2anc 587 . . . . 5 ((∀𝑛 ¬ 𝑛𝑠 ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦)) → if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))
2012, 19jca 515 . . . 4 ((∀𝑛 ¬ 𝑛𝑠 ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦)) → (𝑠𝑝 ∧ if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))
2120expcom 417 . . 3 ((∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦) → (∀𝑛 ¬ 𝑛𝑠 → (𝑠𝑝 ∧ if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
224, 21eximd 2214 . 2 ((∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦) → (∃𝑠𝑛 ¬ 𝑛𝑠 → ∃𝑠(𝑠𝑝 ∧ if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
231, 22mpi 20 1 ((∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦) → ∃𝑠(𝑠𝑝 ∧ if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 399  if-wif 1058  wal 1536  wex 1781  wral 3106
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-10 2142  ax-12 2175  ax-nul 5174
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 3111
This theorem is referenced by:  axpr  5294
  Copyright terms: Public domain W3C validator