Theorem axprlem4 5364

Description: Lemma for axpr 5365. 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

Step	Hyp	Ref	Expression
1		axprlem4.1	. . 3 ⊢ ∃𝑠∀𝑛𝜑
2		axprlem4.2	. . . . . . . 8 ⊢ (𝜑 → (𝑛 ∈ 𝑠 → ∀𝑡 ¬ 𝑡 ∈ 𝑛))
3	2	alimi 1812	. . . . . . 7 ⊢ (∀𝑛𝜑 → ∀𝑛(𝑛 ∈ 𝑠 → ∀𝑡 ¬ 𝑡 ∈ 𝑛))
4		df-ral 3048	. . . . . . 7 ⊢ (∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 ↔ ∀𝑛(𝑛 ∈ 𝑠 → ∀𝑡 ¬ 𝑡 ∈ 𝑛))
5	3, 4	sylibr 234	. . . . . 6 ⊢ (∀𝑛𝜑 → ∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛)
6	5	imim1i 63	. . . . 5 ⊢ ((∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) → (∀𝑛𝜑 → 𝑠 ∈ 𝑝))
7	6	ancrd 551	. . . 4 ⊢ ((∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) → (∀𝑛𝜑 → (𝑠 ∈ 𝑝 ∧ ∀𝑛𝜑)))
8	7	aleximi 1833	. . 3 ⊢ (∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) → (∃𝑠∀𝑛𝜑 → ∃𝑠(𝑠 ∈ 𝑝 ∧ ∀𝑛𝜑)))
9	1, 8	mpi 20	. 2 ⊢ (∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) → ∃𝑠(𝑠 ∈ 𝑝 ∧ ∀𝑛𝜑))
10		axprlem4.3	. . . . 5 ⊢ (∀𝑛𝜑 → (if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦) ↔ 𝑤 = 𝑣))
11	10	biimprcd 250	. . . 4 ⊢ (𝑤 = 𝑣 → (∀𝑛𝜑 → if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))
12	11	anim2d 612	. . 3 ⊢ (𝑤 = 𝑣 → ((𝑠 ∈ 𝑝 ∧ ∀𝑛𝜑) → (𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
13	12	eximdv 1918	. 2 ⊢ (𝑤 = 𝑣 → (∃𝑠(𝑠 ∈ 𝑝 ∧ ∀𝑛𝜑) → ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
14	9, 13	syl5com 31	1 ⊢ (∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) → (𝑤 = 𝑣 → ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395  if-wif 1062  ∀wal 1539  ∃wex 1780  ∀wral 3047

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-ral 3048

This theorem is referenced by:  axpr  5365