Theorem axprlem4

Description: Lemma for axpr . The first element of the pair 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)

	Ref	Expression
Assertion	axprlem4	⊢ ( ( ∀ 𝑠 ( ∀ 𝑛 ∈ 𝑠 ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝 ) ∧ 𝑤 = 𝑥 ) → ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) )

Proof

Step	Hyp	Ref	Expression
1		axprlem1	⊢ ∃ 𝑠 ∀ 𝑛 ( ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑛 ∈ 𝑠 )
2	1	bm1.3ii	⊢ ∃ 𝑠 ∀ 𝑛 ( 𝑛 ∈ 𝑠 ↔ ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 )
3		nfa1	⊢ Ⅎ 𝑠 ∀ 𝑠 ( ∀ 𝑛 ∈ 𝑠 ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝 )
4		nfv	⊢ Ⅎ 𝑠 𝑤 = 𝑥
5	3 4	nfan	⊢ Ⅎ 𝑠 ( ∀ 𝑠 ( ∀ 𝑛 ∈ 𝑠 ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝 ) ∧ 𝑤 = 𝑥 )
6		biimp	⊢ ( ( 𝑛 ∈ 𝑠 ↔ ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 ) → ( 𝑛 ∈ 𝑠 → ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 ) )
7	6	alimi	⊢ ( ∀ 𝑛 ( 𝑛 ∈ 𝑠 ↔ ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 ) → ∀ 𝑛 ( 𝑛 ∈ 𝑠 → ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 ) )
8		df-ral	⊢ ( ∀ 𝑛 ∈ 𝑠 ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 ↔ ∀ 𝑛 ( 𝑛 ∈ 𝑠 → ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 ) )
9	7 8	sylibr	⊢ ( ∀ 𝑛 ( 𝑛 ∈ 𝑠 ↔ ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 ) → ∀ 𝑛 ∈ 𝑠 ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 )
10		sp	⊢ ( ∀ 𝑠 ( ∀ 𝑛 ∈ 𝑠 ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝 ) → ( ∀ 𝑛 ∈ 𝑠 ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝 ) )
11	9 10	mpan9	⊢ ( ( ∀ 𝑛 ( 𝑛 ∈ 𝑠 ↔ ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 ) ∧ ∀ 𝑠 ( ∀ 𝑛 ∈ 𝑠 ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝 ) ) → 𝑠 ∈ 𝑝 )
12	11	adantrr	⊢ ( ( ∀ 𝑛 ( 𝑛 ∈ 𝑠 ↔ ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 ) ∧ ( ∀ 𝑠 ( ∀ 𝑛 ∈ 𝑠 ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝 ) ∧ 𝑤 = 𝑥 ) ) → 𝑠 ∈ 𝑝 )
13		ax-nul	⊢ ∃ 𝑛 ∀ 𝑡 ¬ 𝑡 ∈ 𝑛
14		nfa1	⊢ Ⅎ 𝑛 ∀ 𝑛 ( 𝑛 ∈ 𝑠 ↔ ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 )
15		sp	⊢ ( ∀ 𝑛 ( 𝑛 ∈ 𝑠 ↔ ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 ) → ( 𝑛 ∈ 𝑠 ↔ ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 ) )
16	15	biimprd	⊢ ( ∀ 𝑛 ( 𝑛 ∈ 𝑠 ↔ ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 ) → ( ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑛 ∈ 𝑠 ) )
17	14 16	eximd	⊢ ( ∀ 𝑛 ( 𝑛 ∈ 𝑠 ↔ ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 ) → ( ∃ 𝑛 ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 → ∃ 𝑛 𝑛 ∈ 𝑠 ) )
18	13 17	mpi	⊢ ( ∀ 𝑛 ( 𝑛 ∈ 𝑠 ↔ ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 ) → ∃ 𝑛 𝑛 ∈ 𝑠 )
19		simprr	⊢ ( ( ∀ 𝑛 ( 𝑛 ∈ 𝑠 ↔ ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 ) ∧ ( ∀ 𝑠 ( ∀ 𝑛 ∈ 𝑠 ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝 ) ∧ 𝑤 = 𝑥 ) ) → 𝑤 = 𝑥 )
20		ifptru	⊢ ( ∃ 𝑛 𝑛 ∈ 𝑠 → ( if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ↔ 𝑤 = 𝑥 ) )
21	20	biimpar	⊢ ( ( ∃ 𝑛 𝑛 ∈ 𝑠 ∧ 𝑤 = 𝑥 ) → if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) )
22	18 19 21	syl2an2r	⊢ ( ( ∀ 𝑛 ( 𝑛 ∈ 𝑠 ↔ ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 ) ∧ ( ∀ 𝑠 ( ∀ 𝑛 ∈ 𝑠 ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝 ) ∧ 𝑤 = 𝑥 ) ) → if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) )
23	12 22	jca	⊢ ( ( ∀ 𝑛 ( 𝑛 ∈ 𝑠 ↔ ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 ) ∧ ( ∀ 𝑠 ( ∀ 𝑛 ∈ 𝑠 ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝 ) ∧ 𝑤 = 𝑥 ) ) → ( 𝑠 ∈ 𝑝 ∧ if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) )
24	23	expcom	⊢ ( ( ∀ 𝑠 ( ∀ 𝑛 ∈ 𝑠 ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝 ) ∧ 𝑤 = 𝑥 ) → ( ∀ 𝑛 ( 𝑛 ∈ 𝑠 ↔ ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 ) → ( 𝑠 ∈ 𝑝 ∧ if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) ) )
25	5 24	eximd	⊢ ( ( ∀ 𝑠 ( ∀ 𝑛 ∈ 𝑠 ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝 ) ∧ 𝑤 = 𝑥 ) → ( ∃ 𝑠 ∀ 𝑛 ( 𝑛 ∈ 𝑠 ↔ ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 ) → ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) ) )
26	2 25	mpi	⊢ ( ( ∀ 𝑠 ( ∀ 𝑛 ∈ 𝑠 ∀ 𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝 ) ∧ 𝑤 = 𝑥 ) → ∃ 𝑠 ( 𝑠 ∈ 𝑝 ∧ if- ( ∃ 𝑛 𝑛 ∈ 𝑠 , 𝑤 = 𝑥 , 𝑤 = 𝑦 ) ) )