Theorem axprALT2 35287

Description: Alternate proof of axpr 5374, proved from predicate calculus, ax-rep 5226, and ax-inf2 9562. (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 5372	. . 3 ⊢ ∃𝑧∀𝑤(𝑤 ∈ 𝑧 ↔ ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))
2		elequ1 2121	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑠 → (𝑡 ∈ 𝑝 ↔ 𝑠 ∈ 𝑝))
3		elequ2 2129	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑠 → (𝑢 ∈ 𝑡 ↔ 𝑢 ∈ 𝑠))
4	2, 3	anbi12d 633	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑠 → ((𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡) ↔ (𝑠 ∈ 𝑝 ∧ 𝑢 ∈ 𝑠)))
5	4	cbvexvw 2039	. . . . . . . . . . 11 ⊢ (∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡) ↔ ∃𝑠(𝑠 ∈ 𝑝 ∧ 𝑢 ∈ 𝑠))
6		elex2 2814	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ 𝑠 → ∃𝑛 𝑛 ∈ 𝑠)
7	6	anim2i 618	. . . . . . . . . . . 12 ⊢ ((𝑠 ∈ 𝑝 ∧ 𝑢 ∈ 𝑠) → (𝑠 ∈ 𝑝 ∧ ∃𝑛 𝑛 ∈ 𝑠))
8	7	eximi 1837	. . . . . . . . . . 11 ⊢ (∃𝑠(𝑠 ∈ 𝑝 ∧ 𝑢 ∈ 𝑠) → ∃𝑠(𝑠 ∈ 𝑝 ∧ ∃𝑛 𝑛 ∈ 𝑠))
9	5, 8	sylbi 217	. . . . . . . . . 10 ⊢ (∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡) → ∃𝑠(𝑠 ∈ 𝑝 ∧ ∃𝑛 𝑛 ∈ 𝑠))
10	9	3ad2ant3 1136	. . . . . . . . 9 ⊢ ((𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → ∃𝑠(𝑠 ∈ 𝑝 ∧ ∃𝑛 𝑛 ∈ 𝑠))
11	10	exlimiv 1932	. . . . . . . 8 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → ∃𝑠(𝑠 ∈ 𝑝 ∧ ∃𝑛 𝑛 ∈ 𝑠))
12		ax-1 6	. . . . . . . . . 10 ⊢ (𝑠 ∈ 𝑝 → (𝑤 = 𝑥 → 𝑠 ∈ 𝑝))
13		ifptru 1075	. . . . . . . . . . 11 ⊢ (∃𝑛 𝑛 ∈ 𝑠 → (if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦) ↔ 𝑤 = 𝑥))
14	13	biimprd 248	. . . . . . . . . 10 ⊢ (∃𝑛 𝑛 ∈ 𝑠 → (𝑤 = 𝑥 → if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))
15	12, 14	anim12ii 619	. . . . . . . . 9 ⊢ ((𝑠 ∈ 𝑝 ∧ ∃𝑛 𝑛 ∈ 𝑠) → (𝑤 = 𝑥 → (𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
16	15	eximi 1837	. . . . . . . 8 ⊢ (∃𝑠(𝑠 ∈ 𝑝 ∧ ∃𝑛 𝑛 ∈ 𝑠) → ∃𝑠(𝑤 = 𝑥 → (𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
17		19.37imv 1949	. . . . . . . 8 ⊢ (∃𝑠(𝑤 = 𝑥 → (𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))) → (𝑤 = 𝑥 → ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
18	11, 16, 17	3syl 18	. . . . . . 7 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → (𝑤 = 𝑥 → ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
19		3simpa 1149	. . . . . . . . . 10 ⊢ ((𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → (𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢))
20	19	eximi 1837	. . . . . . . . 9 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → ∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢))
21		elequ1 2121	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑠 → (𝑢 ∈ 𝑝 ↔ 𝑠 ∈ 𝑝))
22		elequ2 2129	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑠 → (𝑡 ∈ 𝑢 ↔ 𝑡 ∈ 𝑠))
23	22	notbid 318	. . . . . . . . . . . . . 14 ⊢ (𝑢 = 𝑠 → (¬ 𝑡 ∈ 𝑢 ↔ ¬ 𝑡 ∈ 𝑠))
24	23	albidv 1922	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑠 → (∀𝑡 ¬ 𝑡 ∈ 𝑢 ↔ ∀𝑡 ¬ 𝑡 ∈ 𝑠))
25		elequ1 2121	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 𝑛 → (𝑡 ∈ 𝑠 ↔ 𝑛 ∈ 𝑠))
26	25	notbid 318	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑛 → (¬ 𝑡 ∈ 𝑠 ↔ ¬ 𝑛 ∈ 𝑠))
27	26	cbvalvw 2038	. . . . . . . . . . . . 13 ⊢ (∀𝑡 ¬ 𝑡 ∈ 𝑠 ↔ ∀𝑛 ¬ 𝑛 ∈ 𝑠)
28	24, 27	bitrdi 287	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑠 → (∀𝑡 ¬ 𝑡 ∈ 𝑢 ↔ ∀𝑛 ¬ 𝑛 ∈ 𝑠))
29	21, 28	anbi12d 633	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑠 → ((𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢) ↔ (𝑠 ∈ 𝑝 ∧ ∀𝑛 ¬ 𝑛 ∈ 𝑠)))
30	29	cbvexvw 2039	. . . . . . . . . 10 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢) ↔ ∃𝑠(𝑠 ∈ 𝑝 ∧ ∀𝑛 ¬ 𝑛 ∈ 𝑠))
31		alnex 1783	. . . . . . . . . . . . 13 ⊢ (∀𝑛 ¬ 𝑛 ∈ 𝑠 ↔ ¬ ∃𝑛 𝑛 ∈ 𝑠)
32	31	anbi2i 624	. . . . . . . . . . . 12 ⊢ ((𝑠 ∈ 𝑝 ∧ ∀𝑛 ¬ 𝑛 ∈ 𝑠) ↔ (𝑠 ∈ 𝑝 ∧ ¬ ∃𝑛 𝑛 ∈ 𝑠))
33	32	biimpi 216	. . . . . . . . . . 11 ⊢ ((𝑠 ∈ 𝑝 ∧ ∀𝑛 ¬ 𝑛 ∈ 𝑠) → (𝑠 ∈ 𝑝 ∧ ¬ ∃𝑛 𝑛 ∈ 𝑠))
34	33	eximi 1837	. . . . . . . . . 10 ⊢ (∃𝑠(𝑠 ∈ 𝑝 ∧ ∀𝑛 ¬ 𝑛 ∈ 𝑠) → ∃𝑠(𝑠 ∈ 𝑝 ∧ ¬ ∃𝑛 𝑛 ∈ 𝑠))
35	30, 34	sylbi 217	. . . . . . . . 9 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢) → ∃𝑠(𝑠 ∈ 𝑝 ∧ ¬ ∃𝑛 𝑛 ∈ 𝑠))
36	20, 35	syl 17	. . . . . . . 8 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → ∃𝑠(𝑠 ∈ 𝑝 ∧ ¬ ∃𝑛 𝑛 ∈ 𝑠))
37		ax-1 6	. . . . . . . . . 10 ⊢ (𝑠 ∈ 𝑝 → (𝑤 = 𝑦 → 𝑠 ∈ 𝑝))
38		ifpfal 1076	. . . . . . . . . . 11 ⊢ (¬ ∃𝑛 𝑛 ∈ 𝑠 → (if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦) ↔ 𝑤 = 𝑦))
39	38	biimprd 248	. . . . . . . . . 10 ⊢ (¬ ∃𝑛 𝑛 ∈ 𝑠 → (𝑤 = 𝑦 → if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))
40	37, 39	anim12ii 619	. . . . . . . . 9 ⊢ ((𝑠 ∈ 𝑝 ∧ ¬ ∃𝑛 𝑛 ∈ 𝑠) → (𝑤 = 𝑦 → (𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
41	40	eximi 1837	. . . . . . . 8 ⊢ (∃𝑠(𝑠 ∈ 𝑝 ∧ ¬ ∃𝑛 𝑛 ∈ 𝑠) → ∃𝑠(𝑤 = 𝑦 → (𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
42		19.37imv 1949	. . . . . . . 8 ⊢ (∃𝑠(𝑤 = 𝑦 → (𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))) → (𝑤 = 𝑦 → ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
43	36, 41, 42	3syl 18	. . . . . . 7 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → (𝑤 = 𝑦 → ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
44	18, 43	jaod 860	. . . . . 6 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → ((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))))
45		imbi2 348	. . . . . 6 ⊢ ((𝑤 ∈ 𝑧 ↔ ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))) → (((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧) ↔ ((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦)))))
46	44, 45	syl5ibrcom 247	. . . . 5 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → ((𝑤 ∈ 𝑧 ↔ ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))) → ((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧)))
47	46	alimdv 1918	. . . 4 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → (∀𝑤(𝑤 ∈ 𝑧 ↔ ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))) → ∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧)))
48	47	eximdv 1919	. . 3 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → (∃𝑧∀𝑤(𝑤 ∈ 𝑧 ↔ ∃𝑠(𝑠 ∈ 𝑝 ∧ if-(∃𝑛 𝑛 ∈ 𝑠, 𝑤 = 𝑥, 𝑤 = 𝑦))) → ∃𝑧∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧)))
49	1, 48	mpi 20	. 2 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → ∃𝑧∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧))
50		ax-inf2 9562	. . . . 5 ⊢ ∃𝑝(∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢) ∧ ∀𝑢(𝑢 ∈ 𝑝 → ∃𝑡(𝑡 ∈ 𝑝 ∧ ∀𝑣(𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢)))))
51		df-rex 3063	. . . . . 6 ⊢ (∃𝑢 ∈ 𝑝 ∀𝑡 ¬ 𝑡 ∈ 𝑢 ↔ ∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢))
52		df-ral 3053	. . . . . . . 8 ⊢ (∀𝑢 ∈ 𝑝 ∃𝑡(𝑡 ∈ 𝑝 ∧ ∀𝑣(𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢))) ↔ ∀𝑢(𝑢 ∈ 𝑝 → ∃𝑡(𝑡 ∈ 𝑝 ∧ ∀𝑣(𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢)))))
53		olc 869	. . . . . . . . . . . . . 14 ⊢ (𝑣 = 𝑢 → (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢))
54		biimpr 220	. . . . . . . . . . . . . 14 ⊢ ((𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢)) → ((𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢) → 𝑣 ∈ 𝑡))
55	53, 54	syl5 34	. . . . . . . . . . . . 13 ⊢ ((𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢)) → (𝑣 = 𝑢 → 𝑣 ∈ 𝑡))
56	55	alimi 1813	. . . . . . . . . . . 12 ⊢ (∀𝑣(𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢)) → ∀𝑣(𝑣 = 𝑢 → 𝑣 ∈ 𝑡))
57		elequ1 2121	. . . . . . . . . . . . 13 ⊢ (𝑣 = 𝑢 → (𝑣 ∈ 𝑡 ↔ 𝑢 ∈ 𝑡))
58	57	equsalvw 2006	. . . . . . . . . . . 12 ⊢ (∀𝑣(𝑣 = 𝑢 → 𝑣 ∈ 𝑡) ↔ 𝑢 ∈ 𝑡)
59	56, 58	sylib 218	. . . . . . . . . . 11 ⊢ (∀𝑣(𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢)) → 𝑢 ∈ 𝑡)
60	59	anim2i 618	. . . . . . . . . 10 ⊢ ((𝑡 ∈ 𝑝 ∧ ∀𝑣(𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢))) → (𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡))
61	60	eximi 1837	. . . . . . . . 9 ⊢ (∃𝑡(𝑡 ∈ 𝑝 ∧ ∀𝑣(𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢))) → ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡))
62	61	ralimi 3075	. . . . . . . 8 ⊢ (∀𝑢 ∈ 𝑝 ∃𝑡(𝑡 ∈ 𝑝 ∧ ∀𝑣(𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢))) → ∀𝑢 ∈ 𝑝 ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡))
63	52, 62	sylbir 235	. . . . . . 7 ⊢ (∀𝑢(𝑢 ∈ 𝑝 → ∃𝑡(𝑡 ∈ 𝑝 ∧ ∀𝑣(𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢)))) → ∀𝑢 ∈ 𝑝 ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡))
64	63	anim2i 618	. . . . . 6 ⊢ ((∃𝑢 ∈ 𝑝 ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∀𝑢(𝑢 ∈ 𝑝 → ∃𝑡(𝑡 ∈ 𝑝 ∧ ∀𝑣(𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢))))) → (∃𝑢 ∈ 𝑝 ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∀𝑢 ∈ 𝑝 ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)))
65	51, 64	sylanbr 583	. . . . 5 ⊢ ((∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢) ∧ ∀𝑢(𝑢 ∈ 𝑝 → ∃𝑡(𝑡 ∈ 𝑝 ∧ ∀𝑣(𝑣 ∈ 𝑡 ↔ (𝑣 ∈ 𝑢 ∨ 𝑣 = 𝑢))))) → (∃𝑢 ∈ 𝑝 ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∀𝑢 ∈ 𝑝 ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)))
66	50, 65	eximii 1839	. . . 4 ⊢ ∃𝑝(∃𝑢 ∈ 𝑝 ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∀𝑢 ∈ 𝑝 ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡))
67		r19.29r 3102	. . . 4 ⊢ ((∃𝑢 ∈ 𝑝 ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∀𝑢 ∈ 𝑝 ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → ∃𝑢 ∈ 𝑝 (∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)))
68	66, 67	eximii 1839	. . 3 ⊢ ∃𝑝∃𝑢 ∈ 𝑝 (∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡))
69		df-rex 3063	. . . 4 ⊢ (∃𝑢 ∈ 𝑝 (∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) ↔ ∃𝑢(𝑢 ∈ 𝑝 ∧ (∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡))))
70		3anass 1095	. . . . 5 ⊢ ((𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) ↔ (𝑢 ∈ 𝑝 ∧ (∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡))))
71	70	exbii 1850	. . . 4 ⊢ (∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) ↔ ∃𝑢(𝑢 ∈ 𝑝 ∧ (∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡))))
72	69, 71	sylbb2 238	. . 3 ⊢ (∃𝑢 ∈ 𝑝 (∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)) → ∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡)))
73	68, 72	eximii 1839	. 2 ⊢ ∃𝑝∃𝑢(𝑢 ∈ 𝑝 ∧ ∀𝑡 ¬ 𝑡 ∈ 𝑢 ∧ ∃𝑡(𝑡 ∈ 𝑝 ∧ 𝑢 ∈ 𝑡))
74	49, 73	exlimiiv 1933	1 ⊢ ∃𝑧∀𝑤((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 848  if-wif 1063   ∧ w3a 1087  ∀wal 1540  ∃wex 1781  ∀wral 3052  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-rep 5226  ax-inf2 9562

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ifp 1064  df-3an 1089  df-ex 1782  df-clel 2812  df-ral 3053  df-rex 3063

This theorem is referenced by: (None)