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

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

Proof of Theorem axprlem4
StepHypRef Expression
1 axprlem1 5419 . . 3 𝑠𝑛(∀𝑡 ¬ 𝑡𝑛𝑛𝑠)
21bm1.3ii 5299 . 2 𝑠𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛)
3 nfa1 2141 . . . 4 𝑠𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝)
4 nfv 1910 . . . 4 𝑠 𝑤 = 𝑥
53, 4nfan 1895 . . 3 𝑠(∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑥)
6 biimp 214 . . . . . . . . 9 ((𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) → (𝑛𝑠 → ∀𝑡 ¬ 𝑡𝑛))
76alimi 1806 . . . . . . . 8 (∀𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) → ∀𝑛(𝑛𝑠 → ∀𝑡 ¬ 𝑡𝑛))
8 df-ral 3052 . . . . . . . 8 (∀𝑛𝑠𝑡 ¬ 𝑡𝑛 ↔ ∀𝑛(𝑛𝑠 → ∀𝑡 ¬ 𝑡𝑛))
97, 8sylibr 233 . . . . . . 7 (∀𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) → ∀𝑛𝑠𝑡 ¬ 𝑡𝑛)
10 sp 2172 . . . . . . 7 (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) → (∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝))
119, 10mpan9 505 . . . . . 6 ((∀𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) ∧ ∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝)) → 𝑠𝑝)
1211adantrr 715 . . . . 5 ((∀𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑥)) → 𝑠𝑝)
13 ax-nul 5303 . . . . . . 7 𝑛𝑡 ¬ 𝑡𝑛
14 nfa1 2141 . . . . . . . 8 𝑛𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛)
15 sp 2172 . . . . . . . . 9 (∀𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) → (𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛))
1615biimprd 247 . . . . . . . 8 (∀𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) → (∀𝑡 ¬ 𝑡𝑛𝑛𝑠))
1714, 16eximd 2205 . . . . . . 7 (∀𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) → (∃𝑛𝑡 ¬ 𝑡𝑛 → ∃𝑛 𝑛𝑠))
1813, 17mpi 20 . . . . . 6 (∀𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) → ∃𝑛 𝑛𝑠)
19 simprr 771 . . . . . 6 ((∀𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑥)) → 𝑤 = 𝑥)
20 ifptru 1072 . . . . . . 7 (∃𝑛 𝑛𝑠 → (if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦) ↔ 𝑤 = 𝑥))
2120biimpar 476 . . . . . 6 ((∃𝑛 𝑛𝑠𝑤 = 𝑥) → if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))
2218, 19, 21syl2an2r 683 . . . . 5 ((∀𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑥)) → if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))
2312, 22jca 510 . . . 4 ((∀𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) ∧ (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑥)) → (𝑠𝑝 ∧ if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))
2423expcom 412 . . 3 ((∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑥) → (∀𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) → (𝑠𝑝 ∧ if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
255, 24eximd 2205 . 2 ((∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑥) → (∃𝑠𝑛(𝑛𝑠 ↔ ∀𝑡 ¬ 𝑡𝑛) → ∃𝑠(𝑠𝑝 ∧ if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
262, 25mpi 20 1 ((∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) ∧ 𝑤 = 𝑥) → ∃𝑠(𝑠𝑝 ∧ if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  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-9 2109  ax-10 2130  ax-12 2167  ax-sep 5296  ax-nul 5303  ax-pow 5361
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  5424
  Copyright terms: Public domain W3C validator