Theorem axprlem5 5350

Description: Lemma for axpr 5351. 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 5230	. 2 ⊢ ∃𝑠∀𝑛 ¬ 𝑛 ∈ 𝑠
2		nfa1 2148	. . . 4 ⊢ Ⅎ𝑠∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝)
3		nfv 1917	. . . 4 ⊢ Ⅎ𝑠 𝑤 = 𝑦
4	2, 3	nfan 1902	. . 3 ⊢ Ⅎ𝑠(∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) ∧ 𝑤 = 𝑦)
5		pm2.21 123	. . . . . . . . 9 ⊢ (¬ 𝑛 ∈ 𝑠 → (𝑛 ∈ 𝑠 → ∀𝑡 ¬ 𝑡 ∈ 𝑛))
6	5	alimi 1814	. . . . . . . 8 ⊢ (∀𝑛 ¬ 𝑛 ∈ 𝑠 → ∀𝑛(𝑛 ∈ 𝑠 → ∀𝑡 ¬ 𝑡 ∈ 𝑛))
7	6	adantr 481	. . . . . . 7 ⊢ ((∀𝑛 ¬ 𝑛 ∈ 𝑠 ∧ (∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) ∧ 𝑤 = 𝑦)) → ∀𝑛(𝑛 ∈ 𝑠 → ∀𝑡 ¬ 𝑡 ∈ 𝑛))
8		df-ral 3069	. . . . . . 7 ⊢ (∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 ↔ ∀𝑛(𝑛 ∈ 𝑠 → ∀𝑡 ¬ 𝑡 ∈ 𝑛))
9	7, 8	sylibr 233	. . . . . 6 ⊢ ((∀𝑛 ¬ 𝑛 ∈ 𝑠 ∧ (∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) ∧ 𝑤 = 𝑦)) → ∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛)
10		sp 2176	. . . . . . 7 ⊢ (∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) → (∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝))
11	10	ad2antrl 725	. . . . . 6 ⊢ ((∀𝑛 ¬ 𝑛 ∈ 𝑠 ∧ (∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) ∧ 𝑤 = 𝑦)) → (∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝))
12	9, 11	mpd 15	. . . . 5 ⊢ ((∀𝑛 ¬ 𝑛 ∈ 𝑠 ∧ (∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) ∧ 𝑤 = 𝑦)) → 𝑠 ∈ 𝑝)
13		simpl 483	. . . . . . 7 ⊢ ((∀𝑛 ¬ 𝑛 ∈ 𝑠 ∧ (∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) ∧ 𝑤 = 𝑦)) → ∀𝑛 ¬ 𝑛 ∈ 𝑠)
14		alnex 1784	. . . . . . 7 ⊢ (∀𝑛 ¬ 𝑛 ∈ 𝑠 ↔ ¬ ∃𝑛 𝑛 ∈ 𝑠)
15	13, 14	sylib 217	. . . . . 6 ⊢ ((∀𝑛 ¬ 𝑛 ∈ 𝑠 ∧ (∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) ∧ 𝑤 = 𝑦)) → ¬ ∃𝑛 𝑛 ∈ 𝑠)
16		simprr 770	. . . . . 6 ⊢ ((∀𝑛 ¬ 𝑛 ∈ 𝑠 ∧ (∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) ∧ 𝑤 = 𝑦)) → 𝑤 = 𝑦)
17		ifpfal 1074	. . . . . . 7 ⊢ (¬ ∃𝑛 𝑛 ∈ 𝑠 → (if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦) ↔ 𝑤 = 𝑦))
18	17	biimpar 478	. . . . . 6 ⊢ ((¬ ∃𝑛 𝑛 ∈ 𝑠 ∧ 𝑤 = 𝑦) → if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))
19	15, 16, 18	syl2anc 584	. . . . 5 ⊢ ((∀𝑛 ¬ 𝑛 ∈ 𝑠 ∧ (∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) ∧ 𝑤 = 𝑦)) → if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))
20	12, 19	jca 512	. . . 4 ⊢ ((∀𝑛 ¬ 𝑛 ∈ 𝑠 ∧ (∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) ∧ 𝑤 = 𝑦)) → (𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))
21	20	expcom 414	. . 3 ⊢ ((∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) ∧ 𝑤 = 𝑦) → (∀𝑛 ¬ 𝑛 ∈ 𝑠 → (𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
22	4, 21	eximd 2209	. 2 ⊢ ((∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) ∧ 𝑤 = 𝑦) → (∃𝑠∀𝑛 ¬ 𝑛 ∈ 𝑠 → ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
23	1, 22	mpi 20	1 ⊢ ((∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) ∧ 𝑤 = 𝑦) → ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396  if-wif 1060  ∀wal 1537  ∃wex 1782  ∀wral 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-10 2137  ax-12 2171  ax-nul 5230

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-ifp 1061  df-tru 1542  df-ex 1783  df-nf 1787  df-ral 3069

This theorem is referenced by:  axpr  5351