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

Theorem axprlem5 5426
Description: Lemma for axpr 5427. 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 5307 . 2 𝑠𝑛 ¬ 𝑛𝑠
2 nfa1 2149 . . . 4 𝑠𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝)
3 nfv 1918 . . . 4 𝑠 𝑤 = 𝑦
42, 3nfan 1903 . . 3 𝑠(∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦)
5 pm2.21 123 . . . . . . . . 9 𝑛𝑠 → (𝑛𝑠 → ∀𝑡 ¬ 𝑡𝑛))
65alimi 1814 . . . . . . . 8 (∀𝑛 ¬ 𝑛𝑠 → ∀𝑛(𝑛𝑠 → ∀𝑡 ¬ 𝑡𝑛))
76adantr 482 . . . . . . 7 ((∀𝑛 ¬ 𝑛𝑠 ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦)) → ∀𝑛(𝑛𝑠 → ∀𝑡 ¬ 𝑡𝑛))
8 df-ral 3063 . . . . . . 7 (∀𝑛𝑠𝑡 ¬ 𝑡𝑛 ↔ ∀𝑛(𝑛𝑠 → ∀𝑡 ¬ 𝑡𝑛))
97, 8sylibr 233 . . . . . 6 ((∀𝑛 ¬ 𝑛𝑠 ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦)) → ∀𝑛𝑠𝑡 ¬ 𝑡𝑛)
10 sp 2177 . . . . . . 7 (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) → (∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝))
1110ad2antrl 727 . . . . . 6 ((∀𝑛 ¬ 𝑛𝑠 ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦)) → (∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝))
129, 11mpd 15 . . . . 5 ((∀𝑛 ¬ 𝑛𝑠 ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦)) → 𝑠𝑝)
13 simpl 484 . . . . . . 7 ((∀𝑛 ¬ 𝑛𝑠 ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦)) → ∀𝑛 ¬ 𝑛𝑠)
14 alnex 1784 . . . . . . 7 (∀𝑛 ¬ 𝑛𝑠 ↔ ¬ ∃𝑛 𝑛𝑠)
1513, 14sylib 217 . . . . . 6 ((∀𝑛 ¬ 𝑛𝑠 ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦)) → ¬ ∃𝑛 𝑛𝑠)
16 simprr 772 . . . . . 6 ((∀𝑛 ¬ 𝑛𝑠 ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦)) → 𝑤 = 𝑦)
17 ifpfal 1076 . . . . . . 7 (¬ ∃𝑛 𝑛𝑠 → (if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦) ↔ 𝑤 = 𝑦))
1817biimpar 479 . . . . . 6 ((¬ ∃𝑛 𝑛𝑠𝑤 = 𝑦) → if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))
1915, 16, 18syl2anc 585 . . . . 5 ((∀𝑛 ¬ 𝑛𝑠 ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦)) → if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))
2012, 19jca 513 . . . 4 ((∀𝑛 ¬ 𝑛𝑠 ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦)) → (𝑠𝑝 ∧ if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))
2120expcom 415 . . 3 ((∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦) → (∀𝑛 ¬ 𝑛𝑠 → (𝑠𝑝 ∧ if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
224, 21eximd 2210 . 2 ((∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦) → (∃𝑠𝑛 ¬ 𝑛𝑠 → ∃𝑠(𝑠𝑝 ∧ if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
231, 22mpi 20 1 ((∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦) → ∃𝑠(𝑠𝑝 ∧ if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 397  if-wif 1062  wal 1540  wex 1782  wral 3062
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-10 2138  ax-12 2172  ax-nul 5307
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-ifp 1063  df-tru 1545  df-ex 1783  df-nf 1787  df-ral 3063
This theorem is referenced by:  axpr  5427
  Copyright terms: Public domain W3C validator