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

Theorem axprlem4 5432
Description: Lemma for axpr 5433. If an existing set of empty sets corresponds to one element of the pair, then the element 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.) (Revised by Matthew House, 18-Sep-2025.)
Hypotheses
Ref Expression
axprlem4.1 𝑠𝑛𝜑
axprlem4.2 (𝜑 → (𝑛𝑠 → ∀𝑡 ¬ 𝑡𝑛))
axprlem4.3 (∀𝑛𝜑 → (if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦) ↔ 𝑤 = 𝑣))
Assertion
Ref Expression
axprlem4 (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) → (𝑤 = 𝑣 → ∃𝑠(𝑠𝑝 ∧ if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
Distinct variable groups:   𝑤,𝑠   𝑣,𝑠
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑤,𝑣,𝑡,𝑛,𝑠,𝑝)

Proof of Theorem axprlem4
StepHypRef Expression
1 axprlem4.1 . . 3 𝑠𝑛𝜑
2 axprlem4.2 . . . . . . . 8 (𝜑 → (𝑛𝑠 → ∀𝑡 ¬ 𝑡𝑛))
32alimi 1808 . . . . . . 7 (∀𝑛𝜑 → ∀𝑛(𝑛𝑠 → ∀𝑡 ¬ 𝑡𝑛))
4 df-ral 3060 . . . . . . 7 (∀𝑛𝑠𝑡 ¬ 𝑡𝑛 ↔ ∀𝑛(𝑛𝑠 → ∀𝑡 ¬ 𝑡𝑛))
53, 4sylibr 234 . . . . . 6 (∀𝑛𝜑 → ∀𝑛𝑠𝑡 ¬ 𝑡𝑛)
65imim1i 63 . . . . 5 ((∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) → (∀𝑛𝜑𝑠𝑝))
76ancrd 551 . . . 4 ((∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) → (∀𝑛𝜑 → (𝑠𝑝 ∧ ∀𝑛𝜑)))
87aleximi 1829 . . 3 (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) → (∃𝑠𝑛𝜑 → ∃𝑠(𝑠𝑝 ∧ ∀𝑛𝜑)))
91, 8mpi 20 . 2 (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) → ∃𝑠(𝑠𝑝 ∧ ∀𝑛𝜑))
10 axprlem4.3 . . . . 5 (∀𝑛𝜑 → (if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦) ↔ 𝑤 = 𝑣))
1110biimprcd 250 . . . 4 (𝑤 = 𝑣 → (∀𝑛𝜑 → if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))
1211anim2d 612 . . 3 (𝑤 = 𝑣 → ((𝑠𝑝 ∧ ∀𝑛𝜑) → (𝑠𝑝 ∧ if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
1312eximdv 1915 . 2 (𝑤 = 𝑣 → (∃𝑠(𝑠𝑝 ∧ ∀𝑛𝜑) → ∃𝑠(𝑠𝑝 ∧ if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
149, 13syl5com 31 1 (∀𝑠(∀𝑛𝑠𝑡 ¬ 𝑡𝑛𝑠𝑝) → (𝑤 = 𝑣 → ∃𝑠(𝑠𝑝 ∧ if-(∃𝑛 𝑛𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  if-wif 1062  wal 1535  wex 1776  wral 3059
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-ral 3060
This theorem is referenced by:  axpr  5433
  Copyright terms: Public domain W3C validator