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

Theorem axprlem5 5425
Description: Lemma for axpr 5426. 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 5306 . 2 𝑠𝑛 ¬ 𝑛𝑠
2 nfa1 2148 . . . 4 𝑠𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝)
3 nfv 1917 . . . 4 𝑠 𝑤 = 𝑦
42, 3nfan 1902 . . 3 𝑠(∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦)
5 pm2.21 123 . . . . . . . . 9 𝑛𝑠 → (𝑛𝑠 → ∀𝑡 ¬ 𝑡𝑛))
65alimi 1813 . . . . . . . 8 (∀𝑛 ¬ 𝑛𝑠 → ∀𝑛(𝑛𝑠 → ∀𝑡 ¬ 𝑡𝑛))
76adantr 481 . . . . . . 7 ((∀𝑛 ¬ 𝑛𝑠 ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦)) → ∀𝑛(𝑛𝑠 → ∀𝑡 ¬ 𝑡𝑛))
8 df-ral 3062 . . . . . . 7 (∀𝑛𝑠𝑡 ¬ 𝑡𝑛 ↔ ∀𝑛(𝑛𝑠 → ∀𝑡 ¬ 𝑡𝑛))
97, 8sylibr 233 . . . . . 6 ((∀𝑛 ¬ 𝑛𝑠 ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦)) → ∀𝑛𝑠𝑡 ¬ 𝑡𝑛)
10 sp 2176 . . . . . . 7 (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) → (∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝))
1110ad2antrl 726 . . . . . 6 ((∀𝑛 ¬ 𝑛𝑠 ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦)) → (∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝))
129, 11mpd 15 . . . . 5 ((∀𝑛 ¬ 𝑛𝑠 ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦)) → 𝑠𝑝)
13 simpl 483 . . . . . . 7 ((∀𝑛 ¬ 𝑛𝑠 ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦)) → ∀𝑛 ¬ 𝑛𝑠)
14 alnex 1783 . . . . . . 7 (∀𝑛 ¬ 𝑛𝑠 ↔ ¬ ∃𝑛 𝑛𝑠)
1513, 14sylib 217 . . . . . 6 ((∀𝑛 ¬ 𝑛𝑠 ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦)) → ¬ ∃𝑛 𝑛𝑠)
16 simprr 771 . . . . . 6 ((∀𝑛 ¬ 𝑛𝑠 ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦)) → 𝑤 = 𝑦)
17 ifpfal 1075 . . . . . . 7 (¬ ∃𝑛 𝑛𝑠 → (if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦) ↔ 𝑤 = 𝑦))
1817biimpar 478 . . . . . 6 ((¬ ∃𝑛 𝑛𝑠𝑤 = 𝑦) → if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))
1915, 16, 18syl2anc 584 . . . . 5 ((∀𝑛 ¬ 𝑛𝑠 ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦)) → if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))
2012, 19jca 512 . . . 4 ((∀𝑛 ¬ 𝑛𝑠 ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦)) → (𝑠𝑝 ∧ if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))
2120expcom 414 . . 3 ((∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦) → (∀𝑛 ¬ 𝑛𝑠 → (𝑠𝑝 ∧ if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
224, 21eximd 2209 . 2 ((∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦) → (∃𝑠𝑛 ¬ 𝑛𝑠 → ∃𝑠(𝑠𝑝 ∧ if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
231, 22mpi 20 1 ((∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦) → ∃𝑠(𝑠𝑝 ∧ if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  if-wif 1061  wal 1539  wex 1781  wral 3061
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-10 2137  ax-12 2171  ax-nul 5306
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-ifp 1062  df-tru 1544  df-ex 1782  df-nf 1786  df-ral 3062
This theorem is referenced by:  axpr  5426
  Copyright terms: Public domain W3C validator