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

Theorem axprlem5 5431
Description: Lemma for axpr 5432. 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 5311 . 2 𝑠𝑛 ¬ 𝑛𝑠
2 nfa1 2141 . . . 4 𝑠𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝)
3 nfv 1910 . . . 4 𝑠 𝑤 = 𝑦
42, 3nfan 1895 . . 3 𝑠(∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦)
5 pm2.21 123 . . . . . . . . 9 𝑛𝑠 → (𝑛𝑠 → ∀𝑡 ¬ 𝑡𝑛))
65alimi 1806 . . . . . . . 8 (∀𝑛 ¬ 𝑛𝑠 → ∀𝑛(𝑛𝑠 → ∀𝑡 ¬ 𝑡𝑛))
76adantr 479 . . . . . . 7 ((∀𝑛 ¬ 𝑛𝑠 ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦)) → ∀𝑛(𝑛𝑠 → ∀𝑡 ¬ 𝑡𝑛))
8 df-ral 3052 . . . . . . 7 (∀𝑛𝑠𝑡 ¬ 𝑡𝑛 ↔ ∀𝑛(𝑛𝑠 → ∀𝑡 ¬ 𝑡𝑛))
97, 8sylibr 233 . . . . . 6 ((∀𝑛 ¬ 𝑛𝑠 ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦)) → ∀𝑛𝑠𝑡 ¬ 𝑡𝑛)
10 sp 2172 . . . . . . 7 (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) → (∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝))
1110ad2antrl 726 . . . . . 6 ((∀𝑛 ¬ 𝑛𝑠 ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦)) → (∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝))
129, 11mpd 15 . . . . 5 ((∀𝑛 ¬ 𝑛𝑠 ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦)) → 𝑠𝑝)
13 simpl 481 . . . . . . 7 ((∀𝑛 ¬ 𝑛𝑠 ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦)) → ∀𝑛 ¬ 𝑛𝑠)
14 alnex 1776 . . . . . . 7 (∀𝑛 ¬ 𝑛𝑠 ↔ ¬ ∃𝑛 𝑛𝑠)
1513, 14sylib 217 . . . . . 6 ((∀𝑛 ¬ 𝑛𝑠 ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦)) → ¬ ∃𝑛 𝑛𝑠)
16 simprr 771 . . . . . 6 ((∀𝑛 ¬ 𝑛𝑠 ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦)) → 𝑤 = 𝑦)
17 ifpfal 1073 . . . . . . 7 (¬ ∃𝑛 𝑛𝑠 → (if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦) ↔ 𝑤 = 𝑦))
1817biimpar 476 . . . . . 6 ((¬ ∃𝑛 𝑛𝑠𝑤 = 𝑦) → if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))
1915, 16, 18syl2anc 582 . . . . 5 ((∀𝑛 ¬ 𝑛𝑠 ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦)) → if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))
2012, 19jca 510 . . . 4 ((∀𝑛 ¬ 𝑛𝑠 ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦)) → (𝑠𝑝 ∧ if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))
2120expcom 412 . . 3 ((∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦) → (∀𝑛 ¬ 𝑛𝑠 → (𝑠𝑝 ∧ if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
224, 21eximd 2205 . 2 ((∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦) → (∃𝑠𝑛 ¬ 𝑛𝑠 → ∃𝑠(𝑠𝑝 ∧ if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
231, 22mpi 20 1 ((∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦) → ∃𝑠(𝑠𝑝 ∧ if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 394  if-wif 1060  wal 1532  wex 1774  wral 3051
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-10 2130  ax-12 2167  ax-nul 5311
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-ifp 1061  df-tru 1537  df-ex 1775  df-nf 1779  df-ral 3052
This theorem is referenced by:  axpr  5432
  Copyright terms: Public domain W3C validator