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

Theorem axprlem5 5219
Description: Lemma for axpr 5220. 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 5101 . 2 𝑠𝑛 ¬ 𝑛𝑠
2 nfa1 2121 . . . 4 𝑠𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝)
3 nfv 1892 . . . 4 𝑠 𝑤 = 𝑦
42, 3nfan 1881 . . 3 𝑠(∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦)
5 pm2.21 123 . . . . . . . . 9 𝑛𝑠 → (𝑛𝑠 → ∀𝑡 ¬ 𝑡𝑛))
65alimi 1793 . . . . . . . 8 (∀𝑛 ¬ 𝑛𝑠 → ∀𝑛(𝑛𝑠 → ∀𝑡 ¬ 𝑡𝑛))
76adantr 481 . . . . . . 7 ((∀𝑛 ¬ 𝑛𝑠 ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦)) → ∀𝑛(𝑛𝑠 → ∀𝑡 ¬ 𝑡𝑛))
8 df-ral 3110 . . . . . . 7 (∀𝑛𝑠𝑡 ¬ 𝑡𝑛 ↔ ∀𝑛(𝑛𝑠 → ∀𝑡 ¬ 𝑡𝑛))
97, 8sylibr 235 . . . . . 6 ((∀𝑛 ¬ 𝑛𝑠 ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦)) → ∀𝑛𝑠𝑡 ¬ 𝑡𝑛)
10 sp 2146 . . . . . . 7 (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) → (∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝))
1110ad2antrl 724 . . . . . 6 ((∀𝑛 ¬ 𝑛𝑠 ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦)) → (∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝))
129, 11mpd 15 . . . . 5 ((∀𝑛 ¬ 𝑛𝑠 ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦)) → 𝑠𝑝)
13 simpl 483 . . . . . . 7 ((∀𝑛 ¬ 𝑛𝑠 ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦)) → ∀𝑛 ¬ 𝑛𝑠)
14 alnex 1763 . . . . . . 7 (∀𝑛 ¬ 𝑛𝑠 ↔ ¬ ∃𝑛 𝑛𝑠)
1513, 14sylib 219 . . . . . 6 ((∀𝑛 ¬ 𝑛𝑠 ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦)) → ¬ ∃𝑛 𝑛𝑠)
16 simprr 769 . . . . . 6 ((∀𝑛 ¬ 𝑛𝑠 ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦)) → 𝑤 = 𝑦)
17 ifpfal 1067 . . . . . . 7 (¬ ∃𝑛 𝑛𝑠 → (if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦) ↔ 𝑤 = 𝑦))
1817biimpar 478 . . . . . 6 ((¬ ∃𝑛 𝑛𝑠𝑤 = 𝑦) → if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))
1915, 16, 18syl2anc 584 . . . . 5 ((∀𝑛 ¬ 𝑛𝑠 ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦)) → if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))
2012, 19jca 512 . . . 4 ((∀𝑛 ¬ 𝑛𝑠 ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦)) → (𝑠𝑝 ∧ if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))
2120expcom 414 . . 3 ((∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦) → (∀𝑛 ¬ 𝑛𝑠 → (𝑠𝑝 ∧ if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
224, 21eximd 2181 . 2 ((∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦) → (∃𝑠𝑛 ¬ 𝑛𝑠 → ∃𝑠(𝑠𝑝 ∧ if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
231, 22mpi 20 1 ((∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑦) → ∃𝑠(𝑠𝑝 ∧ if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  if-wif 1055  wal 1520  wex 1761  wral 3105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-10 2112  ax-12 2141  ax-nul 5101
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-ifp 1056  df-tru 1525  df-ex 1762  df-nf 1766  df-ral 3110
This theorem is referenced by:  axpr  5220
  Copyright terms: Public domain W3C validator