Theorem axprALT2 35441

Description: Alternate proof of axpr 5396, proved from predicate calculus, ax-rep 5239, and ax-inf2 9606. (Contributed by BTernaryTau, 26-Mar-2026.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
axprALT2	⊢ ∃𝑧∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧)

Distinct variable groups:   𝑥,𝑤,𝑧   𝑦,𝑤,𝑧

Proof of Theorem axprALT2

Dummy variables 𝑡 𝑝 𝑢 𝑣 𝑠 𝑛 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		axprlem3 5394	. . 3 ⊢ ∃𝑧∀𝑤(𝑤 ∈ 𝑧 ↔ ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))
2		elequ1 2156	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑠 → (𝑡 ∈ 𝑝 ↔ 𝑠 ∈ 𝑝))
3		elequ2 2164	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑠 → (𝑢 ∈ 𝑡 ↔ 𝑢 ∈ 𝑠))
4	2, 3	anbi12d 643	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑠 → ((𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡) ↔ (𝑠 ∈ 𝑝 ∧ 𝑢 ∈ 𝑠)))
5	4	cbvexvw 2064	. . . . . . . . . . 11 ⊢ (∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡) ↔ ∃𝑠(𝑠 ∈ 𝑝 ∧ 𝑢 ∈ 𝑠))
6		elex2 2846	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ 𝑠 → ∃𝑛 𝑛 ∈ 𝑠)
7	6	anim2i 628	. . . . . . . . . . . 12 ⊢ ((𝑠 ∈ 𝑝 ∧ 𝑢 ∈ 𝑠) → (𝑠 ∈ 𝑝 ∧ ∃𝑛 𝑛 ∈ 𝑠))
8	7	eximi 1862	. . . . . . . . . . 11 ⊢ (∃𝑠(𝑠 ∈ 𝑝 ∧ 𝑢 ∈ 𝑠) → ∃𝑠(𝑠 ∈ 𝑝 ∧ ∃𝑛 𝑛 ∈ 𝑠))
9	5, 8	sylbi 220	. . . . . . . . . 10 ⊢ (∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡) → ∃𝑠(𝑠 ∈ 𝑝 ∧ ∃𝑛 𝑛 ∈ 𝑠))
10	9	3ad2ant3 1151	. . . . . . . . 9 ⊢ ((𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → ∃𝑠(𝑠 ∈ 𝑝 ∧ ∃𝑛 𝑛 ∈ 𝑠))
11	10	exlimiv 1957	. . . . . . . 8 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → ∃𝑠(𝑠 ∈ 𝑝 ∧ ∃𝑛 𝑛 ∈ 𝑠))
12		ax-1 6	. . . . . . . . . 10 ⊢ (𝑠 ∈ 𝑝 → (𝑤 = 𝑥 → 𝑠 ∈ 𝑝))
13		ifptru 1089	. . . . . . . . . . 11 ⊢ (∃𝑛 𝑛 ∈ 𝑠 → (if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦) ↔ 𝑤 = 𝑥))
14	13	biimprd 251	. . . . . . . . . 10 ⊢ (∃𝑛 𝑛 ∈ 𝑠 → (𝑤 = 𝑥 → if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))
15	12, 14	anim12ii 629	. . . . . . . . 9 ⊢ ((𝑠 ∈ 𝑝 ∧ ∃𝑛 𝑛 ∈ 𝑠) → (𝑤 = 𝑥 → (𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
16	15	eximi 1862	. . . . . . . 8 ⊢ (∃𝑠(𝑠 ∈ 𝑝 ∧ ∃𝑛 𝑛 ∈ 𝑠) → ∃𝑠(𝑤 = 𝑥 → (𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
17		19.37imv 1974	. . . . . . . 8 ⊢ (∃𝑠(𝑤 = 𝑥 → (𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))) → (𝑤 = 𝑥 → ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
18	11, 16, 17	3syl 19	. . . . . . 7 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → (𝑤 = 𝑥 → ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
19		3simpa 1164	. . . . . . . . . 10 ⊢ ((𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → (𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢))
20	19	eximi 1862	. . . . . . . . 9 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → ∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢))
21		elequ1 2156	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑠 → (𝑢 ∈ 𝑝 ↔ 𝑠 ∈ 𝑝))
22		elequ2 2164	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑠 → (𝑡 ∈ 𝑢 ↔ 𝑡 ∈ 𝑠))
23	22	notbid 321	. . . . . . . . . . . . . 14 ⊢ (𝑢 = 𝑠 → (¬ 𝑡 ∈ 𝑢 ↔ ¬ 𝑡 ∈ 𝑠))
24	23	albidv 1947	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑠 → (∀𝑡 ¬ 𝑡 ∈ 𝑢 ↔ ∀𝑡 ¬ 𝑡 ∈ 𝑠))
25		elequ1 2156	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 𝑛 → (𝑡 ∈ 𝑠 ↔ 𝑛 ∈ 𝑠))
26	25	notbid 321	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑛 → (¬ 𝑡 ∈ 𝑠 ↔ ¬ 𝑛 ∈ 𝑠))
27	26	cbvalvw 2063	. . . . . . . . . . . . 13 ⊢ (∀𝑡 ¬ 𝑡 ∈ 𝑠 ↔ ∀𝑛 ¬ 𝑛 ∈ 𝑠)
28	24, 27	bitrdi 290	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑠 → (∀𝑡 ¬ 𝑡 ∈ 𝑢 ↔ ∀𝑛 ¬ 𝑛 ∈ 𝑠))
29	21, 28	anbi12d 643	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑠 → ((𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢) ↔ (𝑠 ∈ 𝑝 ∧ ∀𝑛 ¬ 𝑛 ∈ 𝑠)))
30	29	cbvexvw 2064	. . . . . . . . . 10 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢) ↔ ∃𝑠(𝑠 ∈ 𝑝 ∧ ∀𝑛 ¬ 𝑛 ∈ 𝑠))
31		alnex 1808	. . . . . . . . . . . . 13 ⊢ (∀𝑛 ¬ 𝑛 ∈ 𝑠 ↔ ¬ ∃𝑛 𝑛 ∈ 𝑠)
32	31	anbi2i 634	. . . . . . . . . . . 12 ⊢ ((𝑠 ∈ 𝑝 ∧ ∀𝑛 ¬ 𝑛 ∈ 𝑠) ↔ (𝑠 ∈ 𝑝 ∧ ¬ ∃𝑛 𝑛 ∈ 𝑠))
33	32	biimpi 219	. . . . . . . . . . 11 ⊢ ((𝑠 ∈ 𝑝 ∧ ∀𝑛 ¬ 𝑛 ∈ 𝑠) → (𝑠 ∈ 𝑝 ∧ ¬ ∃𝑛 𝑛 ∈ 𝑠))
34	33	eximi 1862	. . . . . . . . . 10 ⊢ (∃𝑠(𝑠 ∈ 𝑝 ∧ ∀𝑛 ¬ 𝑛 ∈ 𝑠) → ∃𝑠(𝑠 ∈ 𝑝 ∧ ¬ ∃𝑛 𝑛 ∈ 𝑠))
35	30, 34	sylbi 220	. . . . . . . . 9 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢) → ∃𝑠(𝑠 ∈ 𝑝 ∧ ¬ ∃𝑛 𝑛 ∈ 𝑠))
36	20, 35	syl 18	. . . . . . . 8 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → ∃𝑠(𝑠 ∈ 𝑝 ∧ ¬ ∃𝑛 𝑛 ∈ 𝑠))
37		ax-1 6	. . . . . . . . . 10 ⊢ (𝑠 ∈ 𝑝 → (𝑤 = 𝑦 → 𝑠 ∈ 𝑝))
38		ifpfal 1090	. . . . . . . . . . 11 ⊢ (¬ ∃𝑛 𝑛 ∈ 𝑠 → (if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦) ↔ 𝑤 = 𝑦))
39	38	biimprd 251	. . . . . . . . . 10 ⊢ (¬ ∃𝑛 𝑛 ∈ 𝑠 → (𝑤 = 𝑦 → if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))
40	37, 39	anim12ii 629	. . . . . . . . 9 ⊢ ((𝑠 ∈ 𝑝 ∧ ¬ ∃𝑛 𝑛 ∈ 𝑠) → (𝑤 = 𝑦 → (𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
41	40	eximi 1862	. . . . . . . 8 ⊢ (∃𝑠(𝑠 ∈ 𝑝 ∧ ¬ ∃𝑛 𝑛 ∈ 𝑠) → ∃𝑠(𝑤 = 𝑦 → (𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
42		19.37imv 1974	. . . . . . . 8 ⊢ (∃𝑠(𝑤 = 𝑦 → (𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))) → (𝑤 = 𝑦 → ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
43	36, 41, 42	3syl 19	. . . . . . 7 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → (𝑤 = 𝑦 → ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
44	18, 43	jaod 872	. . . . . 6 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → ((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
45		imbi2 351	. . . . . 6 ⊢ ((𝑤 ∈ 𝑧 ↔ ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))) → (((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧) ↔ ((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))))
46	44, 45	syl5ibrcom 250	. . . . 5 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → ((𝑤 ∈ 𝑧 ↔ ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))) → ((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧)))
47	46	alimdv 1943	. . . 4 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → (∀𝑤(𝑤 ∈ 𝑧 ↔ ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))) → ∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧)))
48	47	eximdv 1944	. . 3 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → (∃𝑧∀𝑤(𝑤 ∈ 𝑧 ↔ ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))) → ∃𝑧∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧)))
49	1, 48	mpi 21	. 2 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → ∃𝑧∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧))
50		ax-inf2 9606	. . . . 5 ⊢ ∃𝑝(∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢) ∧ ∀𝑢(𝑢 ∈ 𝑝 → ∃𝑡(𝑡 ∈ 𝑝 ∧ ∀𝑣(𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢)))))
51		df-rex 3096	. . . . . 6 ⊢ (∃𝑢 ∈ 𝑝 ∀𝑡 ¬ 𝑡 ∈ 𝑢 ↔ ∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢))
52		df-ral 3086	. . . . . . . 8 ⊢ (∀𝑢 ∈ 𝑝 ∃𝑡(𝑡 ∈ 𝑝 ∧ ∀𝑣(𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢))) ↔ ∀𝑢(𝑢 ∈ 𝑝 → ∃𝑡(𝑡 ∈ 𝑝 ∧ ∀𝑣(𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢)))))
53		olc 881	. . . . . . . . . . . . . 14 ⊢ (𝑣 = 𝑢 → (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢))
54		biimpr 223	. . . . . . . . . . . . . 14 ⊢ ((𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢)) → ((𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢) → 𝑣 ∈ 𝑡))
55	53, 54	syl5 35	. . . . . . . . . . . . 13 ⊢ ((𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢)) → (𝑣 = 𝑢 → 𝑣 ∈ 𝑡))
56	55	alimi 1838	. . . . . . . . . . . 12 ⊢ (∀𝑣(𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢)) → ∀𝑣(𝑣 = 𝑢 → 𝑣 ∈ 𝑡))
57		elequ1 2156	. . . . . . . . . . . . 13 ⊢ (𝑣 = 𝑢 → (𝑣 ∈ 𝑡 ↔ 𝑢 ∈ 𝑡))
58	57	equsalvw 2031	. . . . . . . . . . . 12 ⊢ (∀𝑣(𝑣 = 𝑢 → 𝑣 ∈ 𝑡) ↔ 𝑢 ∈ 𝑡)
59	56, 58	sylib 221	. . . . . . . . . . 11 ⊢ (∀𝑣(𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢)) → 𝑢 ∈ 𝑡)
60	59	anim2i 628	. . . . . . . . . 10 ⊢ ((𝑡 ∈ 𝑝 ∧ ∀𝑣(𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢))) → (𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡))
61	60	eximi 1862	. . . . . . . . 9 ⊢ (∃𝑡(𝑡 ∈ 𝑝 ∧ ∀𝑣(𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢))) → ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡))
62	61	ralimi 3108	. . . . . . . 8 ⊢ (∀𝑢 ∈ 𝑝 ∃𝑡(𝑡 ∈ 𝑝 ∧ ∀𝑣(𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢))) → ∀𝑢 ∈ 𝑝 ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡))
63	52, 62	sylbir 238	. . . . . . 7 ⊢ (∀𝑢(𝑢 ∈ 𝑝 → ∃𝑡(𝑡 ∈ 𝑝 ∧ ∀𝑣(𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢)))) → ∀𝑢 ∈ 𝑝 ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡))
64	63	anim2i 628	. . . . . 6 ⊢ ((∃𝑢 ∈ 𝑝 ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∀𝑢(𝑢 ∈ 𝑝 → ∃𝑡(𝑡 ∈ 𝑝 ∧ ∀𝑣(𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢))))) → (∃𝑢 ∈ 𝑝 ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∀𝑢 ∈ 𝑝 ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)))
65	51, 64	sylanbr 593	. . . . 5 ⊢ ((∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢) ∧ ∀𝑢(𝑢 ∈ 𝑝 → ∃𝑡(𝑡 ∈ 𝑝 ∧ ∀𝑣(𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢))))) → (∃𝑢 ∈ 𝑝 ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∀𝑢 ∈ 𝑝 ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)))
66	50, 65	eximii 1864	. . . 4 ⊢ ∃𝑝(∃𝑢 ∈ 𝑝 ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∀𝑢 ∈ 𝑝 ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡))
67		r19.29r 3135	. . . 4 ⊢ ((∃𝑢 ∈ 𝑝 ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∀𝑢 ∈ 𝑝 ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → ∃𝑢 ∈ 𝑝 (∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)))
68	66, 67	eximii 1864	. . 3 ⊢ ∃𝑝∃𝑢 ∈ 𝑝 (∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡))
69		df-rex 3096	. . . 4 ⊢ (∃𝑢 ∈ 𝑝 (∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) ↔ ∃𝑢(𝑢 ∈ 𝑝 ∧ (∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡))))
70		3anass 1109	. . . . 5 ⊢ ((𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) ↔ (𝑢 ∈ 𝑝 ∧ (∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡))))
71	70	exbii 1875	. . . 4 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) ↔ ∃𝑢(𝑢 ∈ 𝑝 ∧ (∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡))))
72	69, 71	sylbb2 241	. . 3 ⊢ (∃𝑢 ∈ 𝑝 (∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → ∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)))
73	68, 72	eximii 1864	. 2 ⊢ ∃𝑝∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡))
74	49, 73	exlimiiv 1958	1 ⊢ ∃𝑧∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∨ wo 860  if-wif 1076   ∧ w3a 1101  ∀wal 1565  ∃wex 1806  ∀wral 3085  ∃wrex 3095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-rep 5239  ax-inf2 9606

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ifp 1077  df-3an 1103  df-ex 1807  df-clel 2844  df-ral 3086  df-rex 3096

This theorem is referenced by: (None)