Theorem axprALT2 35290

Description: Alternate proof of axpr 5356, proved from predicate calculus, ax-rep 5199, and ax-inf2 9553. (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 5354	. . 3 ⊢ ∃𝑧∀𝑤(𝑤 ∈ 𝑧 ↔ ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))
2		elequ1 2126	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑠 → (𝑡 ∈ 𝑝 ↔ 𝑠 ∈ 𝑝))
3		elequ2 2134	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑠 → (𝑢 ∈ 𝑡 ↔ 𝑢 ∈ 𝑠))
4	2, 3	anbi12d 638	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑠 → ((𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡) ↔ (𝑠 ∈ 𝑝 ∧ 𝑢 ∈ 𝑠)))
5	4	cbvexvw 2044	. . . . . . . . . . 11 ⊢ (∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡) ↔ ∃𝑠(𝑠 ∈ 𝑝 ∧ 𝑢 ∈ 𝑠))
6		elex2 2816	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ 𝑠 → ∃𝑛 𝑛 ∈ 𝑠)
7	6	anim2i 623	. . . . . . . . . . . 12 ⊢ ((𝑠 ∈ 𝑝 ∧ 𝑢 ∈ 𝑠) → (𝑠 ∈ 𝑝 ∧ ∃𝑛 𝑛 ∈ 𝑠))
8	7	eximi 1842	. . . . . . . . . . 11 ⊢ (∃𝑠(𝑠 ∈ 𝑝 ∧ 𝑢 ∈ 𝑠) → ∃𝑠(𝑠 ∈ 𝑝 ∧ ∃𝑛 𝑛 ∈ 𝑠))
9	5, 8	sylbi 218	. . . . . . . . . 10 ⊢ (∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡) → ∃𝑠(𝑠 ∈ 𝑝 ∧ ∃𝑛 𝑛 ∈ 𝑠))
10	9	3ad2ant3 1141	. . . . . . . . 9 ⊢ ((𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → ∃𝑠(𝑠 ∈ 𝑝 ∧ ∃𝑛 𝑛 ∈ 𝑠))
11	10	exlimiv 1937	. . . . . . . 8 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → ∃𝑠(𝑠 ∈ 𝑝 ∧ ∃𝑛 𝑛 ∈ 𝑠))
12		ax-1 6	. . . . . . . . . 10 ⊢ (𝑠 ∈ 𝑝 → (𝑤 = 𝑥 → 𝑠 ∈ 𝑝))
13		ifptru 1080	. . . . . . . . . . 11 ⊢ (∃𝑛 𝑛 ∈ 𝑠 → (if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦) ↔ 𝑤 = 𝑥))
14	13	biimprd 249	. . . . . . . . . 10 ⊢ (∃𝑛 𝑛 ∈ 𝑠 → (𝑤 = 𝑥 → if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))
15	12, 14	anim12ii 624	. . . . . . . . 9 ⊢ ((𝑠 ∈ 𝑝 ∧ ∃𝑛 𝑛 ∈ 𝑠) → (𝑤 = 𝑥 → (𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
16	15	eximi 1842	. . . . . . . 8 ⊢ (∃𝑠(𝑠 ∈ 𝑝 ∧ ∃𝑛 𝑛 ∈ 𝑠) → ∃𝑠(𝑤 = 𝑥 → (𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
17		19.37imv 1954	. . . . . . . 8 ⊢ (∃𝑠(𝑤 = 𝑥 → (𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))) → (𝑤 = 𝑥 → ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
18	11, 16, 17	3syl 18	. . . . . . 7 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → (𝑤 = 𝑥 → ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
19		3simpa 1154	. . . . . . . . . 10 ⊢ ((𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → (𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢))
20	19	eximi 1842	. . . . . . . . 9 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → ∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢))
21		elequ1 2126	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑠 → (𝑢 ∈ 𝑝 ↔ 𝑠 ∈ 𝑝))
22		elequ2 2134	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑠 → (𝑡 ∈ 𝑢 ↔ 𝑡 ∈ 𝑠))
23	22	notbid 319	. . . . . . . . . . . . . 14 ⊢ (𝑢 = 𝑠 → (¬ 𝑡 ∈ 𝑢 ↔ ¬ 𝑡 ∈ 𝑠))
24	23	albidv 1927	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑠 → (∀𝑡 ¬ 𝑡 ∈ 𝑢 ↔ ∀𝑡 ¬ 𝑡 ∈ 𝑠))
25		elequ1 2126	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 𝑛 → (𝑡 ∈ 𝑠 ↔ 𝑛 ∈ 𝑠))
26	25	notbid 319	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑛 → (¬ 𝑡 ∈ 𝑠 ↔ ¬ 𝑛 ∈ 𝑠))
27	26	cbvalvw 2043	. . . . . . . . . . . . 13 ⊢ (∀𝑡 ¬ 𝑡 ∈ 𝑠 ↔ ∀𝑛 ¬ 𝑛 ∈ 𝑠)
28	24, 27	bitrdi 288	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑠 → (∀𝑡 ¬ 𝑡 ∈ 𝑢 ↔ ∀𝑛 ¬ 𝑛 ∈ 𝑠))
29	21, 28	anbi12d 638	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑠 → ((𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢) ↔ (𝑠 ∈ 𝑝 ∧ ∀𝑛 ¬ 𝑛 ∈ 𝑠)))
30	29	cbvexvw 2044	. . . . . . . . . 10 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢) ↔ ∃𝑠(𝑠 ∈ 𝑝 ∧ ∀𝑛 ¬ 𝑛 ∈ 𝑠))
31		alnex 1788	. . . . . . . . . . . . 13 ⊢ (∀𝑛 ¬ 𝑛 ∈ 𝑠 ↔ ¬ ∃𝑛 𝑛 ∈ 𝑠)
32	31	anbi2i 629	. . . . . . . . . . . 12 ⊢ ((𝑠 ∈ 𝑝 ∧ ∀𝑛 ¬ 𝑛 ∈ 𝑠) ↔ (𝑠 ∈ 𝑝 ∧ ¬ ∃𝑛 𝑛 ∈ 𝑠))
33	32	biimpi 217	. . . . . . . . . . 11 ⊢ ((𝑠 ∈ 𝑝 ∧ ∀𝑛 ¬ 𝑛 ∈ 𝑠) → (𝑠 ∈ 𝑝 ∧ ¬ ∃𝑛 𝑛 ∈ 𝑠))
34	33	eximi 1842	. . . . . . . . . 10 ⊢ (∃𝑠(𝑠 ∈ 𝑝 ∧ ∀𝑛 ¬ 𝑛 ∈ 𝑠) → ∃𝑠(𝑠 ∈ 𝑝 ∧ ¬ ∃𝑛 𝑛 ∈ 𝑠))
35	30, 34	sylbi 218	. . . . . . . . 9 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢) → ∃𝑠(𝑠 ∈ 𝑝 ∧ ¬ ∃𝑛 𝑛 ∈ 𝑠))
36	20, 35	syl 17	. . . . . . . 8 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → ∃𝑠(𝑠 ∈ 𝑝 ∧ ¬ ∃𝑛 𝑛 ∈ 𝑠))
37		ax-1 6	. . . . . . . . . 10 ⊢ (𝑠 ∈ 𝑝 → (𝑤 = 𝑦 → 𝑠 ∈ 𝑝))
38		ifpfal 1081	. . . . . . . . . . 11 ⊢ (¬ ∃𝑛 𝑛 ∈ 𝑠 → (if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦) ↔ 𝑤 = 𝑦))
39	38	biimprd 249	. . . . . . . . . 10 ⊢ (¬ ∃𝑛 𝑛 ∈ 𝑠 → (𝑤 = 𝑦 → if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))
40	37, 39	anim12ii 624	. . . . . . . . 9 ⊢ ((𝑠 ∈ 𝑝 ∧ ¬ ∃𝑛 𝑛 ∈ 𝑠) → (𝑤 = 𝑦 → (𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
41	40	eximi 1842	. . . . . . . 8 ⊢ (∃𝑠(𝑠 ∈ 𝑝 ∧ ¬ ∃𝑛 𝑛 ∈ 𝑠) → ∃𝑠(𝑤 = 𝑦 → (𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
42		19.37imv 1954	. . . . . . . 8 ⊢ (∃𝑠(𝑤 = 𝑦 → (𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))) → (𝑤 = 𝑦 → ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
43	36, 41, 42	3syl 18	. . . . . . 7 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → (𝑤 = 𝑦 → ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
44	18, 43	jaod 865	. . . . . 6 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → ((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
45		imbi2 349	. . . . . 6 ⊢ ((𝑤 ∈ 𝑧 ↔ ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))) → (((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧) ↔ ((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))))
46	44, 45	syl5ibrcom 248	. . . . 5 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → ((𝑤 ∈ 𝑧 ↔ ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))) → ((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧)))
47	46	alimdv 1923	. . . 4 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → (∀𝑤(𝑤 ∈ 𝑧 ↔ ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))) → ∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧)))
48	47	eximdv 1924	. . 3 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → (∃𝑧∀𝑤(𝑤 ∈ 𝑧 ↔ ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))) → ∃𝑧∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧)))
49	1, 48	mpi 20	. 2 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → ∃𝑧∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧))
50		ax-inf2 9553	. . . . 5 ⊢ ∃𝑝(∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢) ∧ ∀𝑢(𝑢 ∈ 𝑝 → ∃𝑡(𝑡 ∈ 𝑝 ∧ ∀𝑣(𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢)))))
51		df-rex 3064	. . . . . 6 ⊢ (∃𝑢 ∈ 𝑝 ∀𝑡 ¬ 𝑡 ∈ 𝑢 ↔ ∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢))
52		df-ral 3054	. . . . . . . 8 ⊢ (∀𝑢 ∈ 𝑝 ∃𝑡(𝑡 ∈ 𝑝 ∧ ∀𝑣(𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢))) ↔ ∀𝑢(𝑢 ∈ 𝑝 → ∃𝑡(𝑡 ∈ 𝑝 ∧ ∀𝑣(𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢)))))
53		olc 874	. . . . . . . . . . . . . 14 ⊢ (𝑣 = 𝑢 → (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢))
54		biimpr 221	. . . . . . . . . . . . . 14 ⊢ ((𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢)) → ((𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢) → 𝑣 ∈ 𝑡))
55	53, 54	syl5 34	. . . . . . . . . . . . 13 ⊢ ((𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢)) → (𝑣 = 𝑢 → 𝑣 ∈ 𝑡))
56	55	alimi 1818	. . . . . . . . . . . 12 ⊢ (∀𝑣(𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢)) → ∀𝑣(𝑣 = 𝑢 → 𝑣 ∈ 𝑡))
57		elequ1 2126	. . . . . . . . . . . . 13 ⊢ (𝑣 = 𝑢 → (𝑣 ∈ 𝑡 ↔ 𝑢 ∈ 𝑡))
58	57	equsalvw 2011	. . . . . . . . . . . 12 ⊢ (∀𝑣(𝑣 = 𝑢 → 𝑣 ∈ 𝑡) ↔ 𝑢 ∈ 𝑡)
59	56, 58	sylib 219	. . . . . . . . . . 11 ⊢ (∀𝑣(𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢)) → 𝑢 ∈ 𝑡)
60	59	anim2i 623	. . . . . . . . . 10 ⊢ ((𝑡 ∈ 𝑝 ∧ ∀𝑣(𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢))) → (𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡))
61	60	eximi 1842	. . . . . . . . 9 ⊢ (∃𝑡(𝑡 ∈ 𝑝 ∧ ∀𝑣(𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢))) → ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡))
62	61	ralimi 3076	. . . . . . . 8 ⊢ (∀𝑢 ∈ 𝑝 ∃𝑡(𝑡 ∈ 𝑝 ∧ ∀𝑣(𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢))) → ∀𝑢 ∈ 𝑝 ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡))
63	52, 62	sylbir 236	. . . . . . 7 ⊢ (∀𝑢(𝑢 ∈ 𝑝 → ∃𝑡(𝑡 ∈ 𝑝 ∧ ∀𝑣(𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢)))) → ∀𝑢 ∈ 𝑝 ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡))
64	63	anim2i 623	. . . . . 6 ⊢ ((∃𝑢 ∈ 𝑝 ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∀𝑢(𝑢 ∈ 𝑝 → ∃𝑡(𝑡 ∈ 𝑝 ∧ ∀𝑣(𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢))))) → (∃𝑢 ∈ 𝑝 ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∀𝑢 ∈ 𝑝 ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)))
65	51, 64	sylanbr 588	. . . . 5 ⊢ ((∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢) ∧ ∀𝑢(𝑢 ∈ 𝑝 → ∃𝑡(𝑡 ∈ 𝑝 ∧ ∀𝑣(𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢))))) → (∃𝑢 ∈ 𝑝 ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∀𝑢 ∈ 𝑝 ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)))
66	50, 65	eximii 1844	. . . 4 ⊢ ∃𝑝(∃𝑢 ∈ 𝑝 ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∀𝑢 ∈ 𝑝 ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡))
67		r19.29r 3103	. . . 4 ⊢ ((∃𝑢 ∈ 𝑝 ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∀𝑢 ∈ 𝑝 ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → ∃𝑢 ∈ 𝑝 (∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)))
68	66, 67	eximii 1844	. . 3 ⊢ ∃𝑝∃𝑢 ∈ 𝑝 (∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡))
69		df-rex 3064	. . . 4 ⊢ (∃𝑢 ∈ 𝑝 (∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) ↔ ∃𝑢(𝑢 ∈ 𝑝 ∧ (∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡))))
70		3anass 1100	. . . . 5 ⊢ ((𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) ↔ (𝑢 ∈ 𝑝 ∧ (∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡))))
71	70	exbii 1855	. . . 4 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) ↔ ∃𝑢(𝑢 ∈ 𝑝 ∧ (∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡))))
72	69, 71	sylbb2 239	. . 3 ⊢ (∃𝑢 ∈ 𝑝 (∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → ∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)))
73	68, 72	eximii 1844	. 2 ⊢ ∃𝑝∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡))
74	49, 73	exlimiiv 1938	1 ⊢ ∃𝑧∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∧ wa 396   ∨ wo 853  if-wif 1068   ∧ w3a 1092  ∀wal 1545  ∃wex 1786  ∀wral 3053  ∃wrex 3063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-rep 5199  ax-inf2 9553

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-ifp 1069  df-3an 1094  df-ex 1787  df-clel 2814  df-ral 3054  df-rex 3064

This theorem is referenced by: (None)