Theorem axprlem4 5426

Description: Lemma for axpr 5427. 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 1811	. . . . . . 7 ⊢ (∀𝑛𝜑 → ∀𝑛(𝑛 ∈ 𝑠 → ∀𝑡 ¬ 𝑡 ∈ 𝑛))
4		df-ral 3062	. . . . . . 7 ⊢ (∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 ↔ ∀𝑛(𝑛 ∈ 𝑠 → ∀𝑡 ¬ 𝑡 ∈ 𝑛))
5	3, 4	sylibr 234	. . . . . 6 ⊢ (∀𝑛𝜑 → ∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛)
6	5	imim1i 63	. . . . 5 ⊢ ((∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) → (∀𝑛𝜑 → 𝑠 ∈ 𝑝))
7	6	ancrd 551	. . . 4 ⊢ ((∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) → (∀𝑛𝜑 → (𝑠 ∈ 𝑝 ∧ ∀𝑛𝜑)))
8	7	aleximi 1832	. . 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 1917	. 2 ⊢ (𝑤 = 𝑣 → (∃𝑠(𝑠 ∈ 𝑝 ∧ ∀𝑛𝜑) → ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
14	9, 13	syl5com 31	1 ⊢ (∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) → (𝑤 = 𝑣 → ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395  if-wif 1063  ∀wal 1538  ∃wex 1779  ∀wral 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-ral 3062

This theorem is referenced by:  axpr  5427