Theorem axprALT2 35366

Description: Alternate proof of axpr 5381, proved from predicate calculus, ax-rep 5224, and ax-inf2 9590. (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 5379	. . 3 ⊢ ∃𝑧∀𝑤(𝑤 ∈ 𝑧 ↔ ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))
2		elequ1 2148	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑠 → (𝑡 ∈ 𝑝 ↔ 𝑠 ∈ 𝑝))
3		elequ2 2156	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑠 → (𝑢 ∈ 𝑡 ↔ 𝑢 ∈ 𝑠))
4	2, 3	anbi12d 641	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑠 → ((𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡) ↔ (𝑠 ∈ 𝑝 ∧ 𝑢 ∈ 𝑠)))
5	4	cbvexvw 2056	. . . . . . . . . . 11 ⊢ (∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡) ↔ ∃𝑠(𝑠 ∈ 𝑝 ∧ 𝑢 ∈ 𝑠))
6		elex2 2838	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ 𝑠 → ∃𝑛 𝑛 ∈ 𝑠)
7	6	anim2i 626	. . . . . . . . . . . 12 ⊢ ((𝑠 ∈ 𝑝 ∧ 𝑢 ∈ 𝑠) → (𝑠 ∈ 𝑝 ∧ ∃𝑛 𝑛 ∈ 𝑠))
8	7	eximi 1854	. . . . . . . . . . 11 ⊢ (∃𝑠(𝑠 ∈ 𝑝 ∧ 𝑢 ∈ 𝑠) → ∃𝑠(𝑠 ∈ 𝑝 ∧ ∃𝑛 𝑛 ∈ 𝑠))
9	5, 8	sylbi 219	. . . . . . . . . 10 ⊢ (∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡) → ∃𝑠(𝑠 ∈ 𝑝 ∧ ∃𝑛 𝑛 ∈ 𝑠))
10	9	3ad2ant3 1147	. . . . . . . . 9 ⊢ ((𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → ∃𝑠(𝑠 ∈ 𝑝 ∧ ∃𝑛 𝑛 ∈ 𝑠))
11	10	exlimiv 1949	. . . . . . . 8 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → ∃𝑠(𝑠 ∈ 𝑝 ∧ ∃𝑛 𝑛 ∈ 𝑠))
12		ax-1 6	. . . . . . . . . 10 ⊢ (𝑠 ∈ 𝑝 → (𝑤 = 𝑥 → 𝑠 ∈ 𝑝))
13		ifptru 1085	. . . . . . . . . . 11 ⊢ (∃𝑛 𝑛 ∈ 𝑠 → (if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦) ↔ 𝑤 = 𝑥))
14	13	biimprd 250	. . . . . . . . . 10 ⊢ (∃𝑛 𝑛 ∈ 𝑠 → (𝑤 = 𝑥 → if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))
15	12, 14	anim12ii 627	. . . . . . . . 9 ⊢ ((𝑠 ∈ 𝑝 ∧ ∃𝑛 𝑛 ∈ 𝑠) → (𝑤 = 𝑥 → (𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
16	15	eximi 1854	. . . . . . . 8 ⊢ (∃𝑠(𝑠 ∈ 𝑝 ∧ ∃𝑛 𝑛 ∈ 𝑠) → ∃𝑠(𝑤 = 𝑥 → (𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
17		19.37imv 1966	. . . . . . . 8 ⊢ (∃𝑠(𝑤 = 𝑥 → (𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))) → (𝑤 = 𝑥 → ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
18	11, 16, 17	3syl 18	. . . . . . 7 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → (𝑤 = 𝑥 → ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
19		3simpa 1160	. . . . . . . . . 10 ⊢ ((𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → (𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢))
20	19	eximi 1854	. . . . . . . . 9 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → ∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢))
21		elequ1 2148	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑠 → (𝑢 ∈ 𝑝 ↔ 𝑠 ∈ 𝑝))
22		elequ2 2156	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑠 → (𝑡 ∈ 𝑢 ↔ 𝑡 ∈ 𝑠))
23	22	notbid 320	. . . . . . . . . . . . . 14 ⊢ (𝑢 = 𝑠 → (¬ 𝑡 ∈ 𝑢 ↔ ¬ 𝑡 ∈ 𝑠))
24	23	albidv 1939	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑠 → (∀𝑡 ¬ 𝑡 ∈ 𝑢 ↔ ∀𝑡 ¬ 𝑡 ∈ 𝑠))
25		elequ1 2148	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 𝑛 → (𝑡 ∈ 𝑠 ↔ 𝑛 ∈ 𝑠))
26	25	notbid 320	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑛 → (¬ 𝑡 ∈ 𝑠 ↔ ¬ 𝑛 ∈ 𝑠))
27	26	cbvalvw 2055	. . . . . . . . . . . . 13 ⊢ (∀𝑡 ¬ 𝑡 ∈ 𝑠 ↔ ∀𝑛 ¬ 𝑛 ∈ 𝑠)
28	24, 27	bitrdi 289	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑠 → (∀𝑡 ¬ 𝑡 ∈ 𝑢 ↔ ∀𝑛 ¬ 𝑛 ∈ 𝑠))
29	21, 28	anbi12d 641	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑠 → ((𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢) ↔ (𝑠 ∈ 𝑝 ∧ ∀𝑛 ¬ 𝑛 ∈ 𝑠)))
30	29	cbvexvw 2056	. . . . . . . . . 10 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢) ↔ ∃𝑠(𝑠 ∈ 𝑝 ∧ ∀𝑛 ¬ 𝑛 ∈ 𝑠))
31		alnex 1800	. . . . . . . . . . . . 13 ⊢ (∀𝑛 ¬ 𝑛 ∈ 𝑠 ↔ ¬ ∃𝑛 𝑛 ∈ 𝑠)
32	31	anbi2i 632	. . . . . . . . . . . 12 ⊢ ((𝑠 ∈ 𝑝 ∧ ∀𝑛 ¬ 𝑛 ∈ 𝑠) ↔ (𝑠 ∈ 𝑝 ∧ ¬ ∃𝑛 𝑛 ∈ 𝑠))
33	32	biimpi 218	. . . . . . . . . . 11 ⊢ ((𝑠 ∈ 𝑝 ∧ ∀𝑛 ¬ 𝑛 ∈ 𝑠) → (𝑠 ∈ 𝑝 ∧ ¬ ∃𝑛 𝑛 ∈ 𝑠))
34	33	eximi 1854	. . . . . . . . . 10 ⊢ (∃𝑠(𝑠 ∈ 𝑝 ∧ ∀𝑛 ¬ 𝑛 ∈ 𝑠) → ∃𝑠(𝑠 ∈ 𝑝 ∧ ¬ ∃𝑛 𝑛 ∈ 𝑠))
35	30, 34	sylbi 219	. . . . . . . . 9 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢) → ∃𝑠(𝑠 ∈ 𝑝 ∧ ¬ ∃𝑛 𝑛 ∈ 𝑠))
36	20, 35	syl 17	. . . . . . . 8 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → ∃𝑠(𝑠 ∈ 𝑝 ∧ ¬ ∃𝑛 𝑛 ∈ 𝑠))
37		ax-1 6	. . . . . . . . . 10 ⊢ (𝑠 ∈ 𝑝 → (𝑤 = 𝑦 → 𝑠 ∈ 𝑝))
38		ifpfal 1086	. . . . . . . . . . 11 ⊢ (¬ ∃𝑛 𝑛 ∈ 𝑠 → (if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦) ↔ 𝑤 = 𝑦))
39	38	biimprd 250	. . . . . . . . . 10 ⊢ (¬ ∃𝑛 𝑛 ∈ 𝑠 → (𝑤 = 𝑦 → if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))
40	37, 39	anim12ii 627	. . . . . . . . 9 ⊢ ((𝑠 ∈ 𝑝 ∧ ¬ ∃𝑛 𝑛 ∈ 𝑠) → (𝑤 = 𝑦 → (𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
41	40	eximi 1854	. . . . . . . 8 ⊢ (∃𝑠(𝑠 ∈ 𝑝 ∧ ¬ ∃𝑛 𝑛 ∈ 𝑠) → ∃𝑠(𝑤 = 𝑦 → (𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
42		19.37imv 1966	. . . . . . . 8 ⊢ (∃𝑠(𝑤 = 𝑦 → (𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))) → (𝑤 = 𝑦 → ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
43	36, 41, 42	3syl 18	. . . . . . 7 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → (𝑤 = 𝑦 → ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
44	18, 43	jaod 870	. . . . . 6 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → ((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
45		imbi2 350	. . . . . 6 ⊢ ((𝑤 ∈ 𝑧 ↔ ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))) → (((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧) ↔ ((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))))
46	44, 45	syl5ibrcom 249	. . . . 5 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → ((𝑤 ∈ 𝑧 ↔ ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))) → ((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧)))
47	46	alimdv 1935	. . . 4 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → (∀𝑤(𝑤 ∈ 𝑧 ↔ ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))) → ∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧)))
48	47	eximdv 1936	. . 3 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → (∃𝑧∀𝑤(𝑤 ∈ 𝑧 ↔ ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))) → ∃𝑧∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧)))
49	1, 48	mpi 20	. 2 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → ∃𝑧∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧))
50		ax-inf2 9590	. . . . 5 ⊢ ∃𝑝(∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢) ∧ ∀𝑢(𝑢 ∈ 𝑝 → ∃𝑡(𝑡 ∈ 𝑝 ∧ ∀𝑣(𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢)))))
51		df-rex 3086	. . . . . 6 ⊢ (∃𝑢 ∈ 𝑝 ∀𝑡 ¬ 𝑡 ∈ 𝑢 ↔ ∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢))
52		df-ral 3076	. . . . . . . 8 ⊢ (∀𝑢 ∈ 𝑝 ∃𝑡(𝑡 ∈ 𝑝 ∧ ∀𝑣(𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢))) ↔ ∀𝑢(𝑢 ∈ 𝑝 → ∃𝑡(𝑡 ∈ 𝑝 ∧ ∀𝑣(𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢)))))
53		olc 879	. . . . . . . . . . . . . 14 ⊢ (𝑣 = 𝑢 → (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢))
54		biimpr 222	. . . . . . . . . . . . . 14 ⊢ ((𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢)) → ((𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢) → 𝑣 ∈ 𝑡))
55	53, 54	syl5 34	. . . . . . . . . . . . 13 ⊢ ((𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢)) → (𝑣 = 𝑢 → 𝑣 ∈ 𝑡))
56	55	alimi 1830	. . . . . . . . . . . 12 ⊢ (∀𝑣(𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢)) → ∀𝑣(𝑣 = 𝑢 → 𝑣 ∈ 𝑡))
57		elequ1 2148	. . . . . . . . . . . . 13 ⊢ (𝑣 = 𝑢 → (𝑣 ∈ 𝑡 ↔ 𝑢 ∈ 𝑡))
58	57	equsalvw 2023	. . . . . . . . . . . 12 ⊢ (∀𝑣(𝑣 = 𝑢 → 𝑣 ∈ 𝑡) ↔ 𝑢 ∈ 𝑡)
59	56, 58	sylib 220	. . . . . . . . . . 11 ⊢ (∀𝑣(𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢)) → 𝑢 ∈ 𝑡)
60	59	anim2i 626	. . . . . . . . . 10 ⊢ ((𝑡 ∈ 𝑝 ∧ ∀𝑣(𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢))) → (𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡))
61	60	eximi 1854	. . . . . . . . 9 ⊢ (∃𝑡(𝑡 ∈ 𝑝 ∧ ∀𝑣(𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢))) → ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡))
62	61	ralimi 3098	. . . . . . . 8 ⊢ (∀𝑢 ∈ 𝑝 ∃𝑡(𝑡 ∈ 𝑝 ∧ ∀𝑣(𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢))) → ∀𝑢 ∈ 𝑝 ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡))
63	52, 62	sylbir 237	. . . . . . 7 ⊢ (∀𝑢(𝑢 ∈ 𝑝 → ∃𝑡(𝑡 ∈ 𝑝 ∧ ∀𝑣(𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢)))) → ∀𝑢 ∈ 𝑝 ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡))
64	63	anim2i 626	. . . . . 6 ⊢ ((∃𝑢 ∈ 𝑝 ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∀𝑢(𝑢 ∈ 𝑝 → ∃𝑡(𝑡 ∈ 𝑝 ∧ ∀𝑣(𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢))))) → (∃𝑢 ∈ 𝑝 ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∀𝑢 ∈ 𝑝 ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)))
65	51, 64	sylanbr 591	. . . . 5 ⊢ ((∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢) ∧ ∀𝑢(𝑢 ∈ 𝑝 → ∃𝑡(𝑡 ∈ 𝑝 ∧ ∀𝑣(𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢))))) → (∃𝑢 ∈ 𝑝 ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∀𝑢 ∈ 𝑝 ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)))
66	50, 65	eximii 1856	. . . 4 ⊢ ∃𝑝(∃𝑢 ∈ 𝑝 ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∀𝑢 ∈ 𝑝 ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡))
67		r19.29r 3125	. . . 4 ⊢ ((∃𝑢 ∈ 𝑝 ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∀𝑢 ∈ 𝑝 ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → ∃𝑢 ∈ 𝑝 (∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)))
68	66, 67	eximii 1856	. . 3 ⊢ ∃𝑝∃𝑢 ∈ 𝑝 (∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡))
69		df-rex 3086	. . . 4 ⊢ (∃𝑢 ∈ 𝑝 (∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) ↔ ∃𝑢(𝑢 ∈ 𝑝 ∧ (∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡))))
70		3anass 1105	. . . . 5 ⊢ ((𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) ↔ (𝑢 ∈ 𝑝 ∧ (∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡))))
71	70	exbii 1867	. . . 4 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) ↔ ∃𝑢(𝑢 ∈ 𝑝 ∧ (∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡))))
72	69, 71	sylbb2 240	. . 3 ⊢ (∃𝑢 ∈ 𝑝 (∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → ∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)))
73	68, 72	eximii 1856	. 2 ⊢ ∃𝑝∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡))
74	49, 73	exlimiiv 1950	1 ⊢ ∃𝑧∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 399   ∨ wo 858  if-wif 1073   ∧ w3a 1097  ∀wal 1557  ∃wex 1798  ∀wral 3075  ∃wrex 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-rep 5224  ax-inf2 9590

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-ifp 1074  df-3an 1099  df-ex 1799  df-clel 2836  df-ral 3076  df-rex 3086

This theorem is referenced by: (None)