Theorem axprlem4

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

	Ref	Expression
Hypotheses	axprlem4.1	⊢ ∃ 𝑠 ∀ 𝑛 𝜑
	axprlem4.2	⊢ ( 𝜑 → ( 𝑛 ∈ 𝑠 → ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 ) )
	axprlem4.3	⊢ ( ∀ 𝑛 𝜑 → ( if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ↔ 𝑤 = 𝑣 ) )
Assertion	axprlem4	⊢ ( ∀ 𝑠 ( ∀ 𝑛 ∈ 𝑠 ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝 ) → ( 𝑤 = 𝑣 → ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) ) )

Proof

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