Theorem axprlem4 5382

Description: Lemma for axpr 5383. 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 1830	. . . . . . 7 ⊢ (∀𝑛𝜑 → ∀𝑛(𝑛 ∈ 𝑠 → ∀𝑡 ¬ 𝑡 ∈ 𝑛))
4	3	ralrid 3083	. . . . . 6 ⊢ (∀𝑛𝜑 → ∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛)
5	4	imim1i 63	. . . . 5 ⊢ ((∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) → (∀𝑛𝜑 → 𝑠 ∈ 𝑝))
6	5	ancrd 559	. . . 4 ⊢ ((∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) → (∀𝑛𝜑 → (𝑠 ∈ 𝑝 ∧ ∀𝑛𝜑)))
7	6	aleximi 1851	. . 3 ⊢ (∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) → (∃𝑠∀𝑛𝜑 → ∃𝑠(𝑠 ∈ 𝑝 ∧ ∀𝑛𝜑)))
8	1, 7	mpi 20	. 2 ⊢ (∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) → ∃𝑠(𝑠 ∈ 𝑝 ∧ ∀𝑛𝜑))
9		axprlem4.3	. . . . 5 ⊢ (∀𝑛𝜑 → (if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦) ↔ 𝑤 = 𝑣))
10	9	biimprcd 252	. . . 4 ⊢ (𝑤 = 𝑣 → (∀𝑛𝜑 → if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))
11	10	anim2d 621	. . 3 ⊢ (𝑤 = 𝑣 → ((𝑠 ∈ 𝑝 ∧ ∀𝑛𝜑) → (𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
12	11	eximdv 1936	. 2 ⊢ (𝑤 = 𝑣 → (∃𝑠(𝑠 ∈ 𝑝 ∧ ∀𝑛𝜑) → ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
13	8, 12	syl5com 31	1 ⊢ (∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) → (𝑤 = 𝑣 → ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 399  if-wif 1073  ∀wal 1557  ∃wex 1798  ∀wral 3075

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-ral 3076

This theorem is referenced by:  axpr  5383