Theorem axprlem5 5370

Description: Lemma for axpr 5371. 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 5250	. 2 ⊢ ∃𝑠∀𝑛 ¬ 𝑛 ∈ 𝑠
2		nfa1 2147	. . . 4 ⊢ Ⅎ𝑠∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝)
3		nfv 1916	. . . 4 ⊢ Ⅎ𝑠 𝑤 = 𝑦
4	2, 3	nfan 1901	. . 3 ⊢ Ⅎ𝑠(∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) ∧ 𝑤 = 𝑦)
5		pm2.21 123	. . . . . . . . 9 ⊢ (¬ 𝑛 ∈ 𝑠 → (𝑛 ∈ 𝑠 → ∀𝑡 ¬ 𝑡 ∈ 𝑛))
6	5	alimi 1812	. . . . . . . 8 ⊢ (∀𝑛 ¬ 𝑛 ∈ 𝑠 → ∀𝑛(𝑛 ∈ 𝑠 → ∀𝑡 ¬ 𝑡 ∈ 𝑛))
7	6	adantr 481	. . . . . . 7 ⊢ ((∀𝑛 ¬ 𝑛 ∈ 𝑠 ∧ (∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) ∧ 𝑤 = 𝑦)) → ∀𝑛(𝑛 ∈ 𝑠 → ∀𝑡 ¬ 𝑡 ∈ 𝑛))
8		df-ral 3062	. . . . . . 7 ⊢ (∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 ↔ ∀𝑛(𝑛 ∈ 𝑠 → ∀𝑡 ¬ 𝑡 ∈ 𝑛))
9	7, 8	sylibr 233	. . . . . 6 ⊢ ((∀𝑛 ¬ 𝑛 ∈ 𝑠 ∧ (∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) ∧ 𝑤 = 𝑦)) → ∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛)
10		sp 2175	. . . . . . 7 ⊢ (∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) → (∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝))
11	10	ad2antrl 725	. . . . . 6 ⊢ ((∀𝑛 ¬ 𝑛 ∈ 𝑠 ∧ (∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) ∧ 𝑤 = 𝑦)) → (∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝))
12	9, 11	mpd 15	. . . . 5 ⊢ ((∀𝑛 ¬ 𝑛 ∈ 𝑠 ∧ (∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) ∧ 𝑤 = 𝑦)) → 𝑠 ∈ 𝑝)
13		simpl 483	. . . . . . 7 ⊢ ((∀𝑛 ¬ 𝑛 ∈ 𝑠 ∧ (∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) ∧ 𝑤 = 𝑦)) → ∀𝑛 ¬ 𝑛 ∈ 𝑠)
14		alnex 1782	. . . . . . 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 2208	. 2 ⊢ ((∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) ∧ 𝑤 = 𝑦) → (∃𝑠∀𝑛 ¬ 𝑛 ∈ 𝑠 → ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
23	1, 22	mpi 20	1 ⊢ ((∀𝑠(∀𝑛 ∈ 𝑠 ∀𝑡 ¬ 𝑡 ∈ 𝑛 → 𝑠 ∈ 𝑝) ∧ 𝑤 = 𝑦) → ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396  if-wif 1060  ∀wal 1538  ∃wex 1780  ∀wral 3061

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 1912  ax-6 1970  ax-7 2010  ax-10 2136  ax-12 2170  ax-nul 5250

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-ifp 1061  df-tru 1543  df-ex 1781  df-nf 1785  df-ral 3062

This theorem is referenced by:  axpr  5371