Theorem axprlem4 5344

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

Assertion

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

Distinct variable groups:   𝑥,𝑠   𝑤,𝑠   𝑡,𝑛,𝑠

Proof of Theorem axprlem4

Step	Hyp	Ref	Expression
1		axprlem1 5341	. . 3 ⊢ ∃𝑠∀𝑛(∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑛 ∈ 𝑠)
2	1	bm1.3ii 5221	. 2 ⊢ ∃𝑠∀𝑛(𝑛 ∈ 𝑠 ↔ ∀𝑡 ¬ 𝑡 ∈ 𝑛)
3		nfa1 2150	. . . 4 ⊢ Ⅎ𝑠∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝)
4		nfv 1918	. . . 4 ⊢ Ⅎ𝑠 𝑤 = 𝑥
5	3, 4	nfan 1903	. . 3 ⊢ Ⅎ𝑠(∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) ∧ 𝑤 = 𝑥)
6		biimp 214	. . . . . . . . 9 ⊢ ((𝑛 ∈ 𝑠 ↔ ∀𝑡 ¬ 𝑡 ∈ 𝑛) → (𝑛 ∈ 𝑠 → ∀𝑡 ¬ 𝑡 ∈ 𝑛))
7	6	alimi 1815	. . . . . . . 8 ⊢ (∀𝑛(𝑛 ∈ 𝑠 ↔ ∀𝑡 ¬ 𝑡 ∈ 𝑛) → ∀𝑛(𝑛 ∈ 𝑠 → ∀𝑡 ¬ 𝑡 ∈ 𝑛))
8		df-ral 3068	. . . . . . . 8 ⊢ (∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 ↔ ∀𝑛(𝑛 ∈ 𝑠 → ∀𝑡 ¬ 𝑡 ∈ 𝑛))
9	7, 8	sylibr 233	. . . . . . 7 ⊢ (∀𝑛(𝑛 ∈ 𝑠 ↔ ∀𝑡 ¬ 𝑡 ∈ 𝑛) → ∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛)
10		sp 2178	. . . . . . 7 ⊢ (∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) → (∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝))
11	9, 10	mpan9 506	. . . . . 6 ⊢ ((∀𝑛(𝑛 ∈ 𝑠 ↔ ∀𝑡 ¬ 𝑡 ∈ 𝑛) ∧ ∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝)) → 𝑠 ∈ 𝑝)
12	11	adantrr 713	. . . . 5 ⊢ ((∀𝑛(𝑛 ∈ 𝑠 ↔ ∀𝑡 ¬ 𝑡 ∈ 𝑛) ∧ (∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) ∧ 𝑤 = 𝑥)) → 𝑠 ∈ 𝑝)
13		ax-nul 5225	. . . . . . 7 ⊢ ∃𝑛∀𝑡 ¬ 𝑡 ∈ 𝑛
14		nfa1 2150	. . . . . . . 8 ⊢ Ⅎ𝑛∀𝑛(𝑛 ∈ 𝑠 ↔ ∀𝑡 ¬ 𝑡 ∈ 𝑛)
15		sp 2178	. . . . . . . . 9 ⊢ (∀𝑛(𝑛 ∈ 𝑠 ↔ ∀𝑡 ¬ 𝑡 ∈ 𝑛) → (𝑛 ∈ 𝑠 ↔ ∀𝑡 ¬ 𝑡 ∈ 𝑛))
16	15	biimprd 247	. . . . . . . 8 ⊢ (∀𝑛(𝑛 ∈ 𝑠 ↔ ∀𝑡 ¬ 𝑡 ∈ 𝑛) → (∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑛 ∈ 𝑠))
17	14, 16	eximd 2212	. . . . . . 7 ⊢ (∀𝑛(𝑛 ∈ 𝑠 ↔ ∀𝑡 ¬ 𝑡 ∈ 𝑛) → (∃𝑛∀𝑡 ¬ 𝑡 ∈ 𝑛 → ∃𝑛 𝑛 ∈ 𝑠))
18	13, 17	mpi 20	. . . . . 6 ⊢ (∀𝑛(𝑛 ∈ 𝑠 ↔ ∀𝑡 ¬ 𝑡 ∈ 𝑛) → ∃𝑛 𝑛 ∈ 𝑠)
19		simprr 769	. . . . . 6 ⊢ ((∀𝑛(𝑛 ∈ 𝑠 ↔ ∀𝑡 ¬ 𝑡 ∈ 𝑛) ∧ (∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) ∧ 𝑤 = 𝑥)) → 𝑤 = 𝑥)
20		ifptru 1072	. . . . . . 7 ⊢ (∃𝑛 𝑛 ∈ 𝑠 → (if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦) ↔ 𝑤 = 𝑥))
21	20	biimpar 477	. . . . . 6 ⊢ ((∃𝑛 𝑛 ∈ 𝑠 ∧ 𝑤 = 𝑥) → if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))
22	18, 19, 21	syl2an2r 681	. . . . 5 ⊢ ((∀𝑛(𝑛 ∈ 𝑠 ↔ ∀𝑡 ¬ 𝑡 ∈ 𝑛) ∧ (∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) ∧ 𝑤 = 𝑥)) → if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))
23	12, 22	jca 511	. . . 4 ⊢ ((∀𝑛(𝑛 ∈ 𝑠 ↔ ∀𝑡 ¬ 𝑡 ∈ 𝑛) ∧ (∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) ∧ 𝑤 = 𝑥)) → (𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))
24	23	expcom 413	. . 3 ⊢ ((∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) ∧ 𝑤 = 𝑥) → (∀𝑛(𝑛 ∈ 𝑠 ↔ ∀𝑡 ¬ 𝑡 ∈ 𝑛) → (𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
25	5, 24	eximd 2212	. 2 ⊢ ((∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) ∧ 𝑤 = 𝑥) → (∃𝑠∀𝑛(𝑛 ∈ 𝑠 ↔ ∀𝑡 ¬ 𝑡 ∈ 𝑛) → ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
26	2, 25	mpi 20	1 ⊢ ((∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) ∧ 𝑤 = 𝑥) → ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 395  if-wif 1059  ∀wal 1537  ∃wex 1783  ∀wral 3063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-10 2139  ax-12 2173  ax-sep 5218  ax-nul 5225  ax-pow 5283

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-ifp 1060  df-tru 1542  df-ex 1784  df-nf 1788  df-ral 3068

This theorem is referenced by:  axpr  5346