Theorem axprALT2 35723

Description: Alternate proof of axpr 5389, proved from predicate calculus, ax-rep 5232, and ax-inf2 9635. (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 5387	. . 3 ⊢ ∃𝑧∀𝑤(𝑤 ∈ 𝑧 ↔ ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))
2		elequ1 2152	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑠 → (𝑡 ∈ 𝑝 ↔ 𝑠 ∈ 𝑝))
3		elequ2 2160	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑠 → (𝑢 ∈ 𝑡 ↔ 𝑢 ∈ 𝑠))
4	2, 3	anbi12d 644	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑠 → ((𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡) ↔ (𝑠 ∈ 𝑝 ∧ 𝑢 ∈ 𝑠)))
5	4	cbvexvw 2070	. . . . . . . . . . 11 ⊢ (∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡) ↔ ∃𝑠(𝑠 ∈ 𝑝 ∧ 𝑢 ∈ 𝑠))
6		elex2 2838	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ 𝑠 → ∃𝑛 𝑛 ∈ 𝑠)
7	6	anim2i 629	. . . . . . . . . . . 12 ⊢ ((𝑠 ∈ 𝑝 ∧ 𝑢 ∈ 𝑠) → (𝑠 ∈ 𝑝 ∧ ∃𝑛 𝑛 ∈ 𝑠))
8	7	eximi 1868	. . . . . . . . . . 11 ⊢ (∃𝑠(𝑠 ∈ 𝑝 ∧ 𝑢 ∈ 𝑠) → ∃𝑠(𝑠 ∈ 𝑝 ∧ ∃𝑛 𝑛 ∈ 𝑠))
9	5, 8	sylbi 220	. . . . . . . . . 10 ⊢ (∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡) → ∃𝑠(𝑠 ∈ 𝑝 ∧ ∃𝑛 𝑛 ∈ 𝑠))
10	9	3ad2ant3 1153	. . . . . . . . 9 ⊢ ((𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → ∃𝑠(𝑠 ∈ 𝑝 ∧ ∃𝑛 𝑛 ∈ 𝑠))
11	10	exlimiv 1963	. . . . . . . 8 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → ∃𝑠(𝑠 ∈ 𝑝 ∧ ∃𝑛 𝑛 ∈ 𝑠))
12		ax-1 6	. . . . . . . . . 10 ⊢ (𝑠 ∈ 𝑝 → (𝑤 = 𝑥 → 𝑠 ∈ 𝑝))
13		ifptru 1091	. . . . . . . . . . 11 ⊢ (∃𝑛 𝑛 ∈ 𝑠 → (if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦) ↔ 𝑤 = 𝑥))
14	13	biimprd 251	. . . . . . . . . 10 ⊢ (∃𝑛 𝑛 ∈ 𝑠 → (𝑤 = 𝑥 → if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))
15	12, 14	anim12ii 630	. . . . . . . . 9 ⊢ ((𝑠 ∈ 𝑝 ∧ ∃𝑛 𝑛 ∈ 𝑠) → (𝑤 = 𝑥 → (𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
16	15	eximi 1868	. . . . . . . 8 ⊢ (∃𝑠(𝑠 ∈ 𝑝 ∧ ∃𝑛 𝑛 ∈ 𝑠) → ∃𝑠(𝑤 = 𝑥 → (𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
17		19.37imv 1980	. . . . . . . 8 ⊢ (∃𝑠(𝑤 = 𝑥 → (𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))) → (𝑤 = 𝑥 → ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
18	11, 16, 17	3syl 19	. . . . . . 7 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → (𝑤 = 𝑥 → ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
19		3simpa 1166	. . . . . . . . . 10 ⊢ ((𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → (𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢))
20	19	eximi 1868	. . . . . . . . 9 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → ∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢))
21		elequ1 2152	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑠 → (𝑢 ∈ 𝑝 ↔ 𝑠 ∈ 𝑝))
22		elequ2 2160	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑠 → (𝑡 ∈ 𝑢 ↔ 𝑡 ∈ 𝑠))
23	22	notbid 321	. . . . . . . . . . . . . 14 ⊢ (𝑢 = 𝑠 → (¬ 𝑡 ∈ 𝑢 ↔ ¬ 𝑡 ∈ 𝑠))
24	23	albidv 1953	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑠 → (∀𝑡 ¬ 𝑡 ∈ 𝑢 ↔ ∀𝑡 ¬ 𝑡 ∈ 𝑠))
25		elequ1 2152	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 𝑛 → (𝑡 ∈ 𝑠 ↔ 𝑛 ∈ 𝑠))
26	25	notbid 321	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑛 → (¬ 𝑡 ∈ 𝑠 ↔ ¬ 𝑛 ∈ 𝑠))
27	26	cbvalvw 2069	. . . . . . . . . . . . 13 ⊢ (∀𝑡 ¬ 𝑡 ∈ 𝑠 ↔ ∀𝑛 ¬ 𝑛 ∈ 𝑠)
28	24, 27	bitrdi 290	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑠 → (∀𝑡 ¬ 𝑡 ∈ 𝑢 ↔ ∀𝑛 ¬ 𝑛 ∈ 𝑠))
29	21, 28	anbi12d 644	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑠 → ((𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢) ↔ (𝑠 ∈ 𝑝 ∧ ∀𝑛 ¬ 𝑛 ∈ 𝑠)))
30	29	cbvexvw 2070	. . . . . . . . . 10 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢) ↔ ∃𝑠(𝑠 ∈ 𝑝 ∧ ∀𝑛 ¬ 𝑛 ∈ 𝑠))
31		alnex 1814	. . . . . . . . . . . . 13 ⊢ (∀𝑛 ¬ 𝑛 ∈ 𝑠 ↔ ¬ ∃𝑛 𝑛 ∈ 𝑠)
32	31	anbi2i 635	. . . . . . . . . . . 12 ⊢ ((𝑠 ∈ 𝑝 ∧ ∀𝑛 ¬ 𝑛 ∈ 𝑠) ↔ (𝑠 ∈ 𝑝 ∧ ¬ ∃𝑛 𝑛 ∈ 𝑠))
33	32	biimpi 219	. . . . . . . . . . 11 ⊢ ((𝑠 ∈ 𝑝 ∧ ∀𝑛 ¬ 𝑛 ∈ 𝑠) → (𝑠 ∈ 𝑝 ∧ ¬ ∃𝑛 𝑛 ∈ 𝑠))
34	33	eximi 1868	. . . . . . . . . 10 ⊢ (∃𝑠(𝑠 ∈ 𝑝 ∧ ∀𝑛 ¬ 𝑛 ∈ 𝑠) → ∃𝑠(𝑠 ∈ 𝑝 ∧ ¬ ∃𝑛 𝑛 ∈ 𝑠))
35	30, 34	sylbi 220	. . . . . . . . 9 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢) → ∃𝑠(𝑠 ∈ 𝑝 ∧ ¬ ∃𝑛 𝑛 ∈ 𝑠))
36	20, 35	syl 18	. . . . . . . 8 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → ∃𝑠(𝑠 ∈ 𝑝 ∧ ¬ ∃𝑛 𝑛 ∈ 𝑠))
37		ax-1 6	. . . . . . . . . 10 ⊢ (𝑠 ∈ 𝑝 → (𝑤 = 𝑦 → 𝑠 ∈ 𝑝))
38		ifpfal 1092	. . . . . . . . . . 11 ⊢ (¬ ∃𝑛 𝑛 ∈ 𝑠 → (if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦) ↔ 𝑤 = 𝑦))
39	38	biimprd 251	. . . . . . . . . 10 ⊢ (¬ ∃𝑛 𝑛 ∈ 𝑠 → (𝑤 = 𝑦 → if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))
40	37, 39	anim12ii 630	. . . . . . . . 9 ⊢ ((𝑠 ∈ 𝑝 ∧ ¬ ∃𝑛 𝑛 ∈ 𝑠) → (𝑤 = 𝑦 → (𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
41	40	eximi 1868	. . . . . . . 8 ⊢ (∃𝑠(𝑠 ∈ 𝑝 ∧ ¬ ∃𝑛 𝑛 ∈ 𝑠) → ∃𝑠(𝑤 = 𝑦 → (𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
42		19.37imv 1980	. . . . . . . 8 ⊢ (∃𝑠(𝑤 = 𝑦 → (𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))) → (𝑤 = 𝑦 → ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
43	36, 41, 42	3syl 19	. . . . . . 7 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → (𝑤 = 𝑦 → ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
44	18, 43	jaod 873	. . . . . 6 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → ((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
45		imbi2 351	. . . . . 6 ⊢ ((𝑤 ∈ 𝑧 ↔ ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))) → (((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧) ↔ ((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))))
46	44, 45	syl5ibrcom 250	. . . . 5 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → ((𝑤 ∈ 𝑧 ↔ ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))) → ((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧)))
47	46	alimdv 1949	. . . 4 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → (∀𝑤(𝑤 ∈ 𝑧 ↔ ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))) → ∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧)))
48	47	eximdv 1950	. . 3 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → (∃𝑧∀𝑤(𝑤 ∈ 𝑧 ↔ ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))) → ∃𝑧∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧)))
49	1, 48	mpi 21	. 2 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → ∃𝑧∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧))
50		ax-inf2 9635	. . . . 5 ⊢ ∃𝑝(∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢) ∧ ∀𝑢(𝑢 ∈ 𝑝 → ∃𝑡(𝑡 ∈ 𝑝 ∧ ∀𝑣(𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢)))))
51		df-rex 3088	. . . . . 6 ⊢ (∃𝑢 ∈ 𝑝 ∀𝑡 ¬ 𝑡 ∈ 𝑢 ↔ ∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢))
52		df-ral 3078	. . . . . . . 8 ⊢ (∀𝑢 ∈ 𝑝 ∃𝑡(𝑡 ∈ 𝑝 ∧ ∀𝑣(𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢))) ↔ ∀𝑢(𝑢 ∈ 𝑝 → ∃𝑡(𝑡 ∈ 𝑝 ∧ ∀𝑣(𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢)))))
53		olc 882	. . . . . . . . . . . . . 14 ⊢ (𝑣 = 𝑢 → (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢))
54		biimpr 223	. . . . . . . . . . . . . 14 ⊢ ((𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢)) → ((𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢) → 𝑣 ∈ 𝑡))
55	53, 54	syl5 35	. . . . . . . . . . . . 13 ⊢ ((𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢)) → (𝑣 = 𝑢 → 𝑣 ∈ 𝑡))
56	55	alimi 1844	. . . . . . . . . . . 12 ⊢ (∀𝑣(𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢)) → ∀𝑣(𝑣 = 𝑢 → 𝑣 ∈ 𝑡))
57		elequ1 2152	. . . . . . . . . . . . 13 ⊢ (𝑣 = 𝑢 → (𝑣 ∈ 𝑡 ↔ 𝑢 ∈ 𝑡))
58	57	equsalvw 2037	. . . . . . . . . . . 12 ⊢ (∀𝑣(𝑣 = 𝑢 → 𝑣 ∈ 𝑡) ↔ 𝑢 ∈ 𝑡)
59	56, 58	sylib 221	. . . . . . . . . . 11 ⊢ (∀𝑣(𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢)) → 𝑢 ∈ 𝑡)
60	59	anim2i 629	. . . . . . . . . 10 ⊢ ((𝑡 ∈ 𝑝 ∧ ∀𝑣(𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢))) → (𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡))
61	60	eximi 1868	. . . . . . . . 9 ⊢ (∃𝑡(𝑡 ∈ 𝑝 ∧ ∀𝑣(𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢))) → ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡))
62	61	ralimi 3100	. . . . . . . 8 ⊢ (∀𝑢 ∈ 𝑝 ∃𝑡(𝑡 ∈ 𝑝 ∧ ∀𝑣(𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢))) → ∀𝑢 ∈ 𝑝 ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡))
63	52, 62	sylbir 238	. . . . . . 7 ⊢ (∀𝑢(𝑢 ∈ 𝑝 → ∃𝑡(𝑡 ∈ 𝑝 ∧ ∀𝑣(𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢)))) → ∀𝑢 ∈ 𝑝 ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡))
64	63	anim2i 629	. . . . . 6 ⊢ ((∃𝑢 ∈ 𝑝 ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∀𝑢(𝑢 ∈ 𝑝 → ∃𝑡(𝑡 ∈ 𝑝 ∧ ∀𝑣(𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢))))) → (∃𝑢 ∈ 𝑝 ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∀𝑢 ∈ 𝑝 ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)))
65	51, 64	sylanbr 594	. . . . 5 ⊢ ((∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢) ∧ ∀𝑢(𝑢 ∈ 𝑝 → ∃𝑡(𝑡 ∈ 𝑝 ∧ ∀𝑣(𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢))))) → (∃𝑢 ∈ 𝑝 ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∀𝑢 ∈ 𝑝 ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)))
66	50, 65	eximii 1870	. . . 4 ⊢ ∃𝑝(∃𝑢 ∈ 𝑝 ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∀𝑢 ∈ 𝑝 ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡))
67		r19.29r 3127	. . . 4 ⊢ ((∃𝑢 ∈ 𝑝 ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∀𝑢 ∈ 𝑝 ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → ∃𝑢 ∈ 𝑝 (∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)))
68	66, 67	eximii 1870	. . 3 ⊢ ∃𝑝∃𝑢 ∈ 𝑝 (∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡))
69		df-rex 3088	. . . 4 ⊢ (∃𝑢 ∈ 𝑝 (∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) ↔ ∃𝑢(𝑢 ∈ 𝑝 ∧ (∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡))))
70		3anass 1111	. . . . 5 ⊢ ((𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) ↔ (𝑢 ∈ 𝑝 ∧ (∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡))))
71	70	exbii 1881	. . . 4 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) ↔ ∃𝑢(𝑢 ∈ 𝑝 ∧ (∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡))))
72	69, 71	sylbb2 241	. . 3 ⊢ (∃𝑢 ∈ 𝑝 (∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → ∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)))
73	68, 72	eximii 1870	. 2 ⊢ ∃𝑝∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡))
74	49, 73	exlimiiv 1964	1 ⊢ ∃𝑧∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861  if-wif 1078   ∧ w3a 1103  ∀wal 1568  ∃wex 1812  ∀wral 3077  ∃wrex 3087

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-rep 5232  ax-inf2 9635

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ifp 1079  df-3an 1105  df-ex 1813  df-clel 2836  df-ral 3078  df-rex 3088

This theorem is used by: (None)