Theorem axprlem5 5328

Description: Lemma for axpr 5329. The second 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
axprlem5	⊢ ((∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) ∧ 𝑤 = 𝑦) → ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))

Distinct variable groups:   𝑦,𝑠   𝑤,𝑠   𝑛,𝑠

Proof of Theorem axprlem5

Step	Hyp	Ref	Expression
1		ax-nul 5210	. 2 ⊢ ∃𝑠∀𝑛 ¬ 𝑛 ∈ 𝑠
2		nfa1 2155	. . . 4 ⊢ Ⅎ𝑠∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝)
3		nfv 1915	. . . 4 ⊢ Ⅎ𝑠 𝑤 = 𝑦
4	2, 3	nfan 1900	. . 3 ⊢ Ⅎ𝑠(∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) ∧ 𝑤 = 𝑦)
5		pm2.21 123	. . . . . . . . 9 ⊢ (¬ 𝑛 ∈ 𝑠 → (𝑛 ∈ 𝑠 → ∀𝑡 ¬ 𝑡 ∈ 𝑛))
6	5	alimi 1812	. . . . . . . 8 ⊢ (∀𝑛 ¬ 𝑛 ∈ 𝑠 → ∀𝑛(𝑛 ∈ 𝑠 → ∀𝑡 ¬ 𝑡 ∈ 𝑛))
7	6	adantr 483	. . . . . . 7 ⊢ ((∀𝑛 ¬ 𝑛 ∈ 𝑠 ∧ (∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) ∧ 𝑤 = 𝑦)) → ∀𝑛(𝑛 ∈ 𝑠 → ∀𝑡 ¬ 𝑡 ∈ 𝑛))
8		df-ral 3143	. . . . . . 7 ⊢ (∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 ↔ ∀𝑛(𝑛 ∈ 𝑠 → ∀𝑡 ¬ 𝑡 ∈ 𝑛))
9	7, 8	sylibr 236	. . . . . 6 ⊢ ((∀𝑛 ¬ 𝑛 ∈ 𝑠 ∧ (∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) ∧ 𝑤 = 𝑦)) → ∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛)
10		sp 2182	. . . . . . 7 ⊢ (∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) → (∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝))
11	10	ad2antrl 726	. . . . . 6 ⊢ ((∀𝑛 ¬ 𝑛 ∈ 𝑠 ∧ (∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) ∧ 𝑤 = 𝑦)) → (∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝))
12	9, 11	mpd 15	. . . . 5 ⊢ ((∀𝑛 ¬ 𝑛 ∈ 𝑠 ∧ (∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) ∧ 𝑤 = 𝑦)) → 𝑠 ∈ 𝑝)
13		simpl 485	. . . . . . 7 ⊢ ((∀𝑛 ¬ 𝑛 ∈ 𝑠 ∧ (∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) ∧ 𝑤 = 𝑦)) → ∀𝑛 ¬ 𝑛 ∈ 𝑠)
14		alnex 1782	. . . . . . 7 ⊢ (∀𝑛 ¬ 𝑛 ∈ 𝑠 ↔ ¬ ∃𝑛 𝑛 ∈ 𝑠)
15	13, 14	sylib 220	. . . . . 6 ⊢ ((∀𝑛 ¬ 𝑛 ∈ 𝑠 ∧ (∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) ∧ 𝑤 = 𝑦)) → ¬ ∃𝑛 𝑛 ∈ 𝑠)
16		simprr 771	. . . . . 6 ⊢ ((∀𝑛 ¬ 𝑛 ∈ 𝑠 ∧ (∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) ∧ 𝑤 = 𝑦)) → 𝑤 = 𝑦)
17		ifpfal 1069	. . . . . . 7 ⊢ (¬ ∃𝑛 𝑛 ∈ 𝑠 → (if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦) ↔ 𝑤 = 𝑦))
18	17	biimpar 480	. . . . . 6 ⊢ ((¬ ∃𝑛 𝑛 ∈ 𝑠 ∧ 𝑤 = 𝑦) → if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))
19	15, 16, 18	syl2anc 586	. . . . 5 ⊢ ((∀𝑛 ¬ 𝑛 ∈ 𝑠 ∧ (∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) ∧ 𝑤 = 𝑦)) → if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))
20	12, 19	jca 514	. . . 4 ⊢ ((∀𝑛 ¬ 𝑛 ∈ 𝑠 ∧ (∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) ∧ 𝑤 = 𝑦)) → (𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))
21	20	expcom 416	. . 3 ⊢ ((∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) ∧ 𝑤 = 𝑦) → (∀𝑛 ¬ 𝑛 ∈ 𝑠 → (𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
22	4, 21	eximd 2216	. 2 ⊢ ((∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) ∧ 𝑤 = 𝑦) → (∃𝑠∀𝑛 ¬ 𝑛 ∈ 𝑠 → ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
23	1, 22	mpi 20	1 ⊢ ((∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) ∧ 𝑤 = 𝑦) → ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 398  if-wif 1057  ∀wal 1535  ∃wex 1780  ∀wral 3138

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-10 2145  ax-12 2177  ax-nul 5210

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-ifp 1058  df-tru 1540  df-ex 1781  df-nf 1785  df-ral 3143

This theorem is referenced by:  axpr  5329