Theorem constrcbvlem 34369

Description: Technical lemma for eliminating the hypothesis of constr0 34351 and co. (Contributed by Thierry Arnoux, 2-Nov-2025.)

Assertion

Ref

Expression

constrcbvlem

⊢ rec((𝑧 ∈ V ↦ {𝑦 ∈ ℂ ∣ (∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑙 ∈ 𝑧 ∃𝑜 ∈ ℝ ∃𝑝 ∈ ℝ (𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑘 + (𝑝 · (𝑙 − 𝑘))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑘))) ≠ 0) ∨ ∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑚 ∈ 𝑧 ∃𝑞 ∈ 𝑧 ∃𝑜 ∈ ℝ (𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑘)) = (abs‘(𝑚 − 𝑞))) ∨ ∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑙 ∈ 𝑧 ∃𝑚 ∈ 𝑧 ∃𝑞 ∈ 𝑧 (𝑖 ≠ 𝑙 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑘)) ∧ (abs‘(𝑦 − 𝑙)) = (abs‘(𝑚 − 𝑞))))}), {0, 1}) = rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}), {0, 1})

Distinct variable groups:   𝑎,𝑏,𝑐,𝑑,𝑟,𝑠,𝑡,𝑥,𝑧   𝑦,𝑎,𝑏,𝑐,𝑑,𝑟,𝑡,𝑥,𝑧   𝑒,𝑎,𝑓,𝑐,𝑑,𝑠,𝑡,𝑥,𝑧   𝑖,𝑎,𝑗,𝑐,𝑑,𝑟,𝑡,𝑧   𝑒,𝑏,𝑓,𝑗   𝑘,𝑐,𝑙,𝑟,𝑡,𝑧   𝑚,𝑐,𝑡,𝑧   𝑑,𝑙   𝑒,𝑖,𝑘,𝑙,𝑚,𝑞,𝑦,𝑓,𝑗   𝑓,𝑜,𝑘,𝑙,𝑚,𝑞,𝑖   𝑖,𝑝   𝑗,𝑜,𝑝,𝑘,𝑙,𝑡,𝑦   𝑟,𝑝   𝑧,𝑞

Proof of Theorem constrcbvlem

Step	Hyp	Ref	Expression
1		oveq1 7419	. . . . . . . . . . . . . . 15 ⊢ (𝑜 = 𝑡 → (𝑜 · (𝑗 − 𝑖)) = (𝑡 · (𝑗 − 𝑖)))
2	1	oveq2d 7428	. . . . . . . . . . . . . 14 ⊢ (𝑜 = 𝑡 → (𝑖 + (𝑜 · (𝑗 − 𝑖))) = (𝑖 + (𝑡 · (𝑗 − 𝑖))))
3	2	eqeq2d 2772	. . . . . . . . . . . . 13 ⊢ (𝑜 = 𝑡 → (𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ↔ 𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖)))))
4	3	3anbi1d 1468	. . . . . . . . . . . 12 ⊢ (𝑜 = 𝑡 → ((𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑘 + (𝑝 · (𝑙 − 𝑘))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑘))) ≠ 0) ↔ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑘 + (𝑝 · (𝑙 − 𝑘))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑘))) ≠ 0)))
5		oveq1 7419	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = 𝑟 → (𝑝 · (𝑙 − 𝑘)) = (𝑟 · (𝑙 − 𝑘)))
6	5	oveq2d 7428	. . . . . . . . . . . . . 14 ⊢ (𝑝 = 𝑟 → (𝑘 + (𝑝 · (𝑙 − 𝑘))) = (𝑘 + (𝑟 · (𝑙 − 𝑘))))
7	6	eqeq2d 2772	. . . . . . . . . . . . 13 ⊢ (𝑝 = 𝑟 → (𝑦 = (𝑘 + (𝑝 · (𝑙 − 𝑘))) ↔ 𝑦 = (𝑘 + (𝑟 · (𝑙 − 𝑘)))))
8	7	3anbi2d 1469	. . . . . . . . . . . 12 ⊢ (𝑝 = 𝑟 → ((𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑘 + (𝑝 · (𝑙 − 𝑘))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑘))) ≠ 0) ↔ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑘 + (𝑟 · (𝑙 − 𝑘))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑘))) ≠ 0)))
9	4, 8	cbvrex2vw 3246	. . . . . . . . . . 11 ⊢ (∃𝑜 ∈ ℝ ∃𝑝 ∈ ℝ (𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑘 + (𝑝 · (𝑙 − 𝑘))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑘))) ≠ 0) ↔ ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑘 + (𝑟 · (𝑙 − 𝑘))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑘))) ≠ 0))
10	9	2rexbii 3139	. . . . . . . . . 10 ⊢ (∃𝑘 ∈ 𝑧 ∃𝑙 ∈ 𝑧 ∃𝑜 ∈ ℝ ∃𝑝 ∈ ℝ (𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑘 + (𝑝 · (𝑙 − 𝑘))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑘))) ≠ 0) ↔ ∃𝑘 ∈ 𝑧 ∃𝑙 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑘 + (𝑟 · (𝑙 − 𝑘))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑘))) ≠ 0))
11		id 23	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑐 → 𝑘 = 𝑐)
12		oveq2 7420	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑐 → (𝑙 − 𝑘) = (𝑙 − 𝑐))
13	12	oveq2d 7428	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑐 → (𝑟 · (𝑙 − 𝑘)) = (𝑟 · (𝑙 − 𝑐)))
14	11, 13	oveq12d 7430	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑐 → (𝑘 + (𝑟 · (𝑙 − 𝑘))) = (𝑐 + (𝑟 · (𝑙 − 𝑐))))
15	14	eqeq2d 2772	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑐 → (𝑦 = (𝑘 + (𝑟 · (𝑙 − 𝑘))) ↔ 𝑦 = (𝑐 + (𝑟 · (𝑙 − 𝑐)))))
16	12	oveq2d 7428	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑐 → ((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑘)) = ((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑐)))
17	16	fveq2d 6881	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑐 → (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑘))) = (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑐))))
18	17	neeq1d 3015	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑐 → ((ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑘))) ≠ 0 ↔ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑐))) ≠ 0))
19	15, 18	3anbi23d 1467	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑐 → ((𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑘 + (𝑟 · (𝑙 − 𝑘))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑘))) ≠ 0) ↔ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑙 − 𝑐))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑐))) ≠ 0)))
20	19	2rexbidv 3228	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑐 → (∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑘 + (𝑟 · (𝑙 − 𝑘))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑘))) ≠ 0) ↔ ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑙 − 𝑐))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑐))) ≠ 0)))
21		oveq1 7419	. . . . . . . . . . . . . . . 16 ⊢ (𝑙 = 𝑑 → (𝑙 − 𝑐) = (𝑑 − 𝑐))
22	21	oveq2d 7428	. . . . . . . . . . . . . . 15 ⊢ (𝑙 = 𝑑 → (𝑟 · (𝑙 − 𝑐)) = (𝑟 · (𝑑 − 𝑐)))
23	22	oveq2d 7428	. . . . . . . . . . . . . 14 ⊢ (𝑙 = 𝑑 → (𝑐 + (𝑟 · (𝑙 − 𝑐))) = (𝑐 + (𝑟 · (𝑑 − 𝑐))))
24	23	eqeq2d 2772	. . . . . . . . . . . . 13 ⊢ (𝑙 = 𝑑 → (𝑦 = (𝑐 + (𝑟 · (𝑙 − 𝑐))) ↔ 𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐)))))
25	21	oveq2d 7428	. . . . . . . . . . . . . . 15 ⊢ (𝑙 = 𝑑 → ((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑐)) = ((∗‘(𝑗 − 𝑖)) · (𝑑 − 𝑐)))
26	25	fveq2d 6881	. . . . . . . . . . . . . 14 ⊢ (𝑙 = 𝑑 → (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑐))) = (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑑 − 𝑐))))
27	26	neeq1d 3015	. . . . . . . . . . . . 13 ⊢ (𝑙 = 𝑑 → ((ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑐))) ≠ 0 ↔ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑑 − 𝑐))) ≠ 0))
28	24, 27	3anbi23d 1467	. . . . . . . . . . . 12 ⊢ (𝑙 = 𝑑 → ((𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑙 − 𝑐))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑐))) ≠ 0) ↔ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑑 − 𝑐))) ≠ 0)))
29	28	2rexbidv 3228	. . . . . . . . . . 11 ⊢ (𝑙 = 𝑑 → (∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑙 − 𝑐))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑐))) ≠ 0) ↔ ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑑 − 𝑐))) ≠ 0)))
30	20, 29	cbvrex2vw 3246	. . . . . . . . . 10 ⊢ (∃𝑘 ∈ 𝑧 ∃𝑙 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑘 + (𝑟 · (𝑙 − 𝑘))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑘))) ≠ 0) ↔ ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑑 − 𝑐))) ≠ 0))
31	10, 30	bitri 278	. . . . . . . . 9 ⊢ (∃𝑘 ∈ 𝑧 ∃𝑙 ∈ 𝑧 ∃𝑜 ∈ ℝ ∃𝑝 ∈ ℝ (𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑘 + (𝑝 · (𝑙 − 𝑘))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑘))) ≠ 0) ↔ ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑑 − 𝑐))) ≠ 0))
32	31	2rexbii 3139	. . . . . . . 8 ⊢ (∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑙 ∈ 𝑧 ∃𝑜 ∈ ℝ ∃𝑝 ∈ ℝ (𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑘 + (𝑝 · (𝑙 − 𝑘))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑘))) ≠ 0) ↔ ∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑑 − 𝑐))) ≠ 0))
33		oveq2 7420	. . . . . . . . . . . . . . 15 ⊢ (𝑞 = 𝑓 → (𝑚 − 𝑞) = (𝑚 − 𝑓))
34	33	fveq2d 6881	. . . . . . . . . . . . . 14 ⊢ (𝑞 = 𝑓 → (abs‘(𝑚 − 𝑞)) = (abs‘(𝑚 − 𝑓)))
35	34	eqeq2d 2772	. . . . . . . . . . . . 13 ⊢ (𝑞 = 𝑓 → ((abs‘(𝑦 − 𝑘)) = (abs‘(𝑚 − 𝑞)) ↔ (abs‘(𝑦 − 𝑘)) = (abs‘(𝑚 − 𝑓))))
36	35	anbi2d 642	. . . . . . . . . . . 12 ⊢ (𝑞 = 𝑓 → ((𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑘)) = (abs‘(𝑚 − 𝑞))) ↔ (𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑘)) = (abs‘(𝑚 − 𝑓)))))
37	3	anbi1d 643	. . . . . . . . . . . 12 ⊢ (𝑜 = 𝑡 → ((𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑘)) = (abs‘(𝑚 − 𝑓))) ↔ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑘)) = (abs‘(𝑚 − 𝑓)))))
38	36, 37	cbvrex2vw 3246	. . . . . . . . . . 11 ⊢ (∃𝑞 ∈ 𝑧 ∃𝑜 ∈ ℝ (𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑘)) = (abs‘(𝑚 − 𝑞))) ↔ ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑘)) = (abs‘(𝑚 − 𝑓))))
39	38	2rexbii 3139	. . . . . . . . . 10 ⊢ (∃𝑘 ∈ 𝑧 ∃𝑚 ∈ 𝑧 ∃𝑞 ∈ 𝑧 ∃𝑜 ∈ ℝ (𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑘)) = (abs‘(𝑚 − 𝑞))) ↔ ∃𝑘 ∈ 𝑧 ∃𝑚 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑘)) = (abs‘(𝑚 − 𝑓))))
40		oveq2 7420	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑐 → (𝑦 − 𝑘) = (𝑦 − 𝑐))
41	40	fveq2d 6881	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑐 → (abs‘(𝑦 − 𝑘)) = (abs‘(𝑦 − 𝑐)))
42	41	eqeq1d 2763	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑐 → ((abs‘(𝑦 − 𝑘)) = (abs‘(𝑚 − 𝑓)) ↔ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑚 − 𝑓))))
43	42	anbi2d 642	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑐 → ((𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑘)) = (abs‘(𝑚 − 𝑓))) ↔ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑚 − 𝑓)))))
44	43	2rexbidv 3228	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑐 → (∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑘)) = (abs‘(𝑚 − 𝑓))) ↔ ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑚 − 𝑓)))))
45		oveq1 7419	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑒 → (𝑚 − 𝑓) = (𝑒 − 𝑓))
46	45	fveq2d 6881	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑒 → (abs‘(𝑚 − 𝑓)) = (abs‘(𝑒 − 𝑓)))
47	46	eqeq2d 2772	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑒 → ((abs‘(𝑦 − 𝑐)) = (abs‘(𝑚 − 𝑓)) ↔ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓))))
48	47	anbi2d 642	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑒 → ((𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑚 − 𝑓))) ↔ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓)))))
49	48	2rexbidv 3228	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑒 → (∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑚 − 𝑓))) ↔ ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓)))))
50	44, 49	cbvrex2vw 3246	. . . . . . . . . 10 ⊢ (∃𝑘 ∈ 𝑧 ∃𝑚 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑘)) = (abs‘(𝑚 − 𝑓))) ↔ ∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓))))
51	39, 50	bitri 278	. . . . . . . . 9 ⊢ (∃𝑘 ∈ 𝑧 ∃𝑚 ∈ 𝑧 ∃𝑞 ∈ 𝑧 ∃𝑜 ∈ ℝ (𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑘)) = (abs‘(𝑚 − 𝑞))) ↔ ∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓))))
52	51	2rexbii 3139	. . . . . . . 8 ⊢ (∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑚 ∈ 𝑧 ∃𝑞 ∈ 𝑧 ∃𝑜 ∈ ℝ (𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑘)) = (abs‘(𝑚 − 𝑞))) ↔ ∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓))))
53		oveq1 7419	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑒 → (𝑚 − 𝑞) = (𝑒 − 𝑞))
54	53	fveq2d 6881	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑒 → (abs‘(𝑚 − 𝑞)) = (abs‘(𝑒 − 𝑞)))
55	54	eqeq2d 2772	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑒 → ((abs‘(𝑦 − 𝑙)) = (abs‘(𝑚 − 𝑞)) ↔ (abs‘(𝑦 − 𝑙)) = (abs‘(𝑒 − 𝑞))))
56	55	3anbi3d 1470	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑒 → ((𝑖 ≠ 𝑙 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑘)) ∧ (abs‘(𝑦 − 𝑙)) = (abs‘(𝑚 − 𝑞))) ↔ (𝑖 ≠ 𝑙 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑘)) ∧ (abs‘(𝑦 − 𝑙)) = (abs‘(𝑒 − 𝑞)))))
57		oveq2 7420	. . . . . . . . . . . . . . 15 ⊢ (𝑞 = 𝑓 → (𝑒 − 𝑞) = (𝑒 − 𝑓))
58	57	fveq2d 6881	. . . . . . . . . . . . . 14 ⊢ (𝑞 = 𝑓 → (abs‘(𝑒 − 𝑞)) = (abs‘(𝑒 − 𝑓)))
59	58	eqeq2d 2772	. . . . . . . . . . . . 13 ⊢ (𝑞 = 𝑓 → ((abs‘(𝑦 − 𝑙)) = (abs‘(𝑒 − 𝑞)) ↔ (abs‘(𝑦 − 𝑙)) = (abs‘(𝑒 − 𝑓))))
60	59	3anbi3d 1470	. . . . . . . . . . . 12 ⊢ (𝑞 = 𝑓 → ((𝑖 ≠ 𝑙 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑘)) ∧ (abs‘(𝑦 − 𝑙)) = (abs‘(𝑒 − 𝑞))) ↔ (𝑖 ≠ 𝑙 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑘)) ∧ (abs‘(𝑦 − 𝑙)) = (abs‘(𝑒 − 𝑓)))))
61	56, 60	cbvrex2vw 3246	. . . . . . . . . . 11 ⊢ (∃𝑚 ∈ 𝑧 ∃𝑞 ∈ 𝑧 (𝑖 ≠ 𝑙 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑘)) ∧ (abs‘(𝑦 − 𝑙)) = (abs‘(𝑚 − 𝑞))) ↔ ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑖 ≠ 𝑙 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑘)) ∧ (abs‘(𝑦 − 𝑙)) = (abs‘(𝑒 − 𝑓))))
62	61	2rexbii 3139	. . . . . . . . . 10 ⊢ (∃𝑘 ∈ 𝑧 ∃𝑙 ∈ 𝑧 ∃𝑚 ∈ 𝑧 ∃𝑞 ∈ 𝑧 (𝑖 ≠ 𝑙 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑘)) ∧ (abs‘(𝑦 − 𝑙)) = (abs‘(𝑚 − 𝑞))) ↔ ∃𝑘 ∈ 𝑧 ∃𝑙 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑖 ≠ 𝑙 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑘)) ∧ (abs‘(𝑦 − 𝑙)) = (abs‘(𝑒 − 𝑓))))
63		oveq2 7420	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑐 → (𝑗 − 𝑘) = (𝑗 − 𝑐))
64	63	fveq2d 6881	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑐 → (abs‘(𝑗 − 𝑘)) = (abs‘(𝑗 − 𝑐)))
65	64	eqeq2d 2772	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑐 → ((abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑘)) ↔ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑐))))
66	65	3anbi2d 1469	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑐 → ((𝑖 ≠ 𝑙 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑘)) ∧ (abs‘(𝑦 − 𝑙)) = (abs‘(𝑒 − 𝑓))) ↔ (𝑖 ≠ 𝑙 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑐)) ∧ (abs‘(𝑦 − 𝑙)) = (abs‘(𝑒 − 𝑓)))))
67	66	2rexbidv 3228	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑐 → (∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑖 ≠ 𝑙 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑘)) ∧ (abs‘(𝑦 − 𝑙)) = (abs‘(𝑒 − 𝑓))) ↔ ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑖 ≠ 𝑙 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑐)) ∧ (abs‘(𝑦 − 𝑙)) = (abs‘(𝑒 − 𝑓)))))
68		neeq2 3019	. . . . . . . . . . . . 13 ⊢ (𝑙 = 𝑑 → (𝑖 ≠ 𝑙 ↔ 𝑖 ≠ 𝑑))
69		oveq2 7420	. . . . . . . . . . . . . . 15 ⊢ (𝑙 = 𝑑 → (𝑦 − 𝑙) = (𝑦 − 𝑑))
70	69	fveq2d 6881	. . . . . . . . . . . . . 14 ⊢ (𝑙 = 𝑑 → (abs‘(𝑦 − 𝑙)) = (abs‘(𝑦 − 𝑑)))
71	70	eqeq1d 2763	. . . . . . . . . . . . 13 ⊢ (𝑙 = 𝑑 → ((abs‘(𝑦 − 𝑙)) = (abs‘(𝑒 − 𝑓)) ↔ (abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓))))
72	68, 71	3anbi13d 1466	. . . . . . . . . . . 12 ⊢ (𝑙 = 𝑑 → ((𝑖 ≠ 𝑙 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑐)) ∧ (abs‘(𝑦 − 𝑙)) = (abs‘(𝑒 − 𝑓))) ↔ (𝑖 ≠ 𝑑 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑐)) ∧ (abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓)))))
73	72	2rexbidv 3228	. . . . . . . . . . 11 ⊢ (𝑙 = 𝑑 → (∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑖 ≠ 𝑙 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑐)) ∧ (abs‘(𝑦 − 𝑙)) = (abs‘(𝑒 − 𝑓))) ↔ ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑖 ≠ 𝑑 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑐)) ∧ (abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓)))))
74	67, 73	cbvrex2vw 3246	. . . . . . . . . 10 ⊢ (∃𝑘 ∈ 𝑧 ∃𝑙 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑖 ≠ 𝑙 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑘)) ∧ (abs‘(𝑦 − 𝑙)) = (abs‘(𝑒 − 𝑓))) ↔ ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑖 ≠ 𝑑 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑐)) ∧ (abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓))))
75	62, 74	bitri 278	. . . . . . . . 9 ⊢ (∃𝑘 ∈ 𝑧 ∃𝑙 ∈ 𝑧 ∃𝑚 ∈ 𝑧 ∃𝑞 ∈ 𝑧 (𝑖 ≠ 𝑙 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑘)) ∧ (abs‘(𝑦 − 𝑙)) = (abs‘(𝑚 − 𝑞))) ↔ ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑖 ≠ 𝑑 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑐)) ∧ (abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓))))
76	75	2rexbii 3139	. . . . . . . 8 ⊢ (∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑙 ∈ 𝑧 ∃𝑚 ∈ 𝑧 ∃𝑞 ∈ 𝑧 (𝑖 ≠ 𝑙 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑘)) ∧ (abs‘(𝑦 − 𝑙)) = (abs‘(𝑚 − 𝑞))) ↔ ∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑖 ≠ 𝑑 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑐)) ∧ (abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓))))
77	32, 52, 76	3orbi123i 1174	. . . . . . 7 ⊢ ((∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑙 ∈ 𝑧 ∃𝑜 ∈ ℝ ∃𝑝 ∈ ℝ (𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑘 + (𝑝 · (𝑙 − 𝑘))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑘))) ≠ 0) ∨ ∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑚 ∈ 𝑧 ∃𝑞 ∈ 𝑧 ∃𝑜 ∈ ℝ (𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑘)) = (abs‘(𝑚 − 𝑞))) ∨ ∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑙 ∈ 𝑧 ∃𝑚 ∈ 𝑧 ∃𝑞 ∈ 𝑧 (𝑖 ≠ 𝑙 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑘)) ∧ (abs‘(𝑦 − 𝑙)) = (abs‘(𝑚 − 𝑞)))) ↔ (∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑖 ≠ 𝑑 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑐)) ∧ (abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓)))))
78		id 23	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑎 → 𝑖 = 𝑎)
79		oveq2 7420	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑎 → (𝑗 − 𝑖) = (𝑗 − 𝑎))
80	79	oveq2d 7428	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑎 → (𝑡 · (𝑗 − 𝑖)) = (𝑡 · (𝑗 − 𝑎)))
81	78, 80	oveq12d 7430	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑎 → (𝑖 + (𝑡 · (𝑗 − 𝑖))) = (𝑎 + (𝑡 · (𝑗 − 𝑎))))
82	81	eqeq2d 2772	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑎 → (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ↔ 𝑦 = (𝑎 + (𝑡 · (𝑗 − 𝑎)))))
83	79	fveq2d 6881	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑎 → (∗‘(𝑗 − 𝑖)) = (∗‘(𝑗 − 𝑎)))
84	83	oveq1d 7427	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑎 → ((∗‘(𝑗 − 𝑖)) · (𝑑 − 𝑐)) = ((∗‘(𝑗 − 𝑎)) · (𝑑 − 𝑐)))
85	84	fveq2d 6881	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑎 → (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑑 − 𝑐))) = (ℑ‘((∗‘(𝑗 − 𝑎)) · (𝑑 − 𝑐))))
86	85	neeq1d 3015	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑎 → ((ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑑 − 𝑐))) ≠ 0 ↔ (ℑ‘((∗‘(𝑗 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0))
87	82, 86	3anbi13d 1466	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑎 → ((𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑑 − 𝑐))) ≠ 0) ↔ (𝑦 = (𝑎 + (𝑡 · (𝑗 − 𝑎))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑗 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)))
88	87	2rexbidv 3228	. . . . . . . . . 10 ⊢ (𝑖 = 𝑎 → (∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑑 − 𝑐))) ≠ 0) ↔ ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑗 − 𝑎))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑗 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)))
89	88	2rexbidv 3228	. . . . . . . . 9 ⊢ (𝑖 = 𝑎 → (∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑑 − 𝑐))) ≠ 0) ↔ ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑗 − 𝑎))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑗 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)))
90		oveq1 7419	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝑏 → (𝑗 − 𝑎) = (𝑏 − 𝑎))
91	90	oveq2d 7428	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑏 → (𝑡 · (𝑗 − 𝑎)) = (𝑡 · (𝑏 − 𝑎)))
92	91	oveq2d 7428	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑏 → (𝑎 + (𝑡 · (𝑗 − 𝑎))) = (𝑎 + (𝑡 · (𝑏 − 𝑎))))
93	92	eqeq2d 2772	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑏 → (𝑦 = (𝑎 + (𝑡 · (𝑗 − 𝑎))) ↔ 𝑦 = (𝑎 + (𝑡 · (𝑏 − 𝑎)))))
94	90	fveq2d 6881	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝑏 → (∗‘(𝑗 − 𝑎)) = (∗‘(𝑏 − 𝑎)))
95	94	oveq1d 7427	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑏 → ((∗‘(𝑗 − 𝑎)) · (𝑑 − 𝑐)) = ((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐)))
96	95	fveq2d 6881	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑏 → (ℑ‘((∗‘(𝑗 − 𝑎)) · (𝑑 − 𝑐))) = (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))))
97	96	neeq1d 3015	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑏 → ((ℑ‘((∗‘(𝑗 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0 ↔ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0))
98	93, 97	3anbi13d 1466	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑏 → ((𝑦 = (𝑎 + (𝑡 · (𝑗 − 𝑎))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑗 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ↔ (𝑦 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)))
99	98	2rexbidv 3228	. . . . . . . . . 10 ⊢ (𝑗 = 𝑏 → (∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑗 − 𝑎))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑗 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ↔ ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)))
100	99	2rexbidv 3228	. . . . . . . . 9 ⊢ (𝑗 = 𝑏 → (∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑗 − 𝑎))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑗 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ↔ ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)))
101	89, 100	cbvrex2vw 3246	. . . . . . . 8 ⊢ (∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑑 − 𝑐))) ≠ 0) ↔ ∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0))
102	82	anbi1d 643	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑎 → ((𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ↔ (𝑦 = (𝑎 + (𝑡 · (𝑗 − 𝑎))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓)))))
103	102	2rexbidv 3228	. . . . . . . . . 10 ⊢ (𝑖 = 𝑎 → (∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ↔ ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑗 − 𝑎))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓)))))
104	103	2rexbidv 3228	. . . . . . . . 9 ⊢ (𝑖 = 𝑎 → (∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ↔ ∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑗 − 𝑎))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓)))))
105	93	anbi1d 643	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑏 → ((𝑦 = (𝑎 + (𝑡 · (𝑗 − 𝑎))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ↔ (𝑦 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓)))))
106	105	2rexbidv 3228	. . . . . . . . . 10 ⊢ (𝑗 = 𝑏 → (∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑗 − 𝑎))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ↔ ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓)))))
107	106	2rexbidv 3228	. . . . . . . . 9 ⊢ (𝑗 = 𝑏 → (∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑗 − 𝑎))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ↔ ∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓)))))
108	104, 107	cbvrex2vw 3246	. . . . . . . 8 ⊢ (∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ↔ ∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓))))
109		neeq1 3018	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑎 → (𝑖 ≠ 𝑑 ↔ 𝑎 ≠ 𝑑))
110		oveq2 7420	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑎 → (𝑦 − 𝑖) = (𝑦 − 𝑎))
111	110	fveq2d 6881	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑎 → (abs‘(𝑦 − 𝑖)) = (abs‘(𝑦 − 𝑎)))
112	111	eqeq1d 2763	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑎 → ((abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑐)) ↔ (abs‘(𝑦 − 𝑎)) = (abs‘(𝑗 − 𝑐))))
113	109, 112	3anbi12d 1465	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑎 → ((𝑖 ≠ 𝑑 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑐)) ∧ (abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓))) ↔ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑦 − 𝑎)) = (abs‘(𝑗 − 𝑐)) ∧ (abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓)))))
114	113	2rexbidv 3228	. . . . . . . . . 10 ⊢ (𝑖 = 𝑎 → (∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑖 ≠ 𝑑 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑐)) ∧ (abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓))) ↔ ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑦 − 𝑎)) = (abs‘(𝑗 − 𝑐)) ∧ (abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓)))))
115	114	2rexbidv 3228	. . . . . . . . 9 ⊢ (𝑖 = 𝑎 → (∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑖 ≠ 𝑑 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑐)) ∧ (abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓))) ↔ ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑦 − 𝑎)) = (abs‘(𝑗 − 𝑐)) ∧ (abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓)))))
116		oveq1 7419	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑏 → (𝑗 − 𝑐) = (𝑏 − 𝑐))
117	116	fveq2d 6881	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑏 → (abs‘(𝑗 − 𝑐)) = (abs‘(𝑏 − 𝑐)))
118	117	eqeq2d 2772	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑏 → ((abs‘(𝑦 − 𝑎)) = (abs‘(𝑗 − 𝑐)) ↔ (abs‘(𝑦 − 𝑎)) = (abs‘(𝑏 − 𝑐))))
119	118	3anbi2d 1469	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑏 → ((𝑎 ≠ 𝑑 ∧ (abs‘(𝑦 − 𝑎)) = (abs‘(𝑗 − 𝑐)) ∧ (abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓))) ↔ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑦 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓)))))
120	119	2rexbidv 3228	. . . . . . . . . 10 ⊢ (𝑗 = 𝑏 → (∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑦 − 𝑎)) = (abs‘(𝑗 − 𝑐)) ∧ (abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓))) ↔ ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑦 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓)))))
121	120	2rexbidv 3228	. . . . . . . . 9 ⊢ (𝑗 = 𝑏 → (∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑦 − 𝑎)) = (abs‘(𝑗 − 𝑐)) ∧ (abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓))) ↔ ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑦 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓)))))
122	115, 121	cbvrex2vw 3246	. . . . . . . 8 ⊢ (∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑖 ≠ 𝑑 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑐)) ∧ (abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓))) ↔ ∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑦 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓))))
123	101, 108, 122	3orbi123i 1174	. . . . . . 7 ⊢ ((∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑖 ≠ 𝑑 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑐)) ∧ (abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) ↔ (∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑦 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓)))))
124	77, 123	bitri 278	. . . . . 6 ⊢ ((∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑙 ∈ 𝑧 ∃𝑜 ∈ ℝ ∃𝑝 ∈ ℝ (𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑘 + (𝑝 · (𝑙 − 𝑘))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑘))) ≠ 0) ∨ ∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑚 ∈ 𝑧 ∃𝑞 ∈ 𝑧 ∃𝑜 ∈ ℝ (𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑘)) = (abs‘(𝑚 − 𝑞))) ∨ ∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑙 ∈ 𝑧 ∃𝑚 ∈ 𝑧 ∃𝑞 ∈ 𝑧 (𝑖 ≠ 𝑙 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑘)) ∧ (abs‘(𝑦 − 𝑙)) = (abs‘(𝑚 − 𝑞)))) ↔ (∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑦 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓)))))
125	124	rabbii 3418	. . . . 5 ⊢ {𝑦 ∈ ℂ ∣ (∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑙 ∈ 𝑧 ∃𝑜 ∈ ℝ ∃𝑝 ∈ ℝ (𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑘 + (𝑝 · (𝑙 − 𝑘))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑘))) ≠ 0) ∨ ∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑚 ∈ 𝑧 ∃𝑞 ∈ 𝑧 ∃𝑜 ∈ ℝ (𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑘)) = (abs‘(𝑚 − 𝑞))) ∨ ∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑙 ∈ 𝑧 ∃𝑚 ∈ 𝑧 ∃𝑞 ∈ 𝑧 (𝑖 ≠ 𝑙 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑘)) ∧ (abs‘(𝑦 − 𝑙)) = (abs‘(𝑚 − 𝑞))))} = {𝑦 ∈ ℂ ∣ (∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑦 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}
126		eqeq1 2765	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑥 → (𝑦 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ↔ 𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎)))))
127		eqeq1 2765	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑥 → (𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ↔ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐)))))
128		biidd 265	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑥 → ((ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0 ↔ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0))
129	126, 127, 128	3anbi123d 1464	. . . . . . . . . 10 ⊢ (𝑦 = 𝑥 → ((𝑦 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ↔ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)))
130	129	2rexbidv 3228	. . . . . . . . 9 ⊢ (𝑦 = 𝑥 → (∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ↔ ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)))
131	130	2rexbidv 3228	. . . . . . . 8 ⊢ (𝑦 = 𝑥 → (∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ↔ ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)))
132	131	2rexbidv 3228	. . . . . . 7 ⊢ (𝑦 = 𝑥 → (∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ↔ ∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)))
133		oveq1 7419	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑥 → (𝑦 − 𝑐) = (𝑥 − 𝑐))
134	133	fveq2d 6881	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑥 → (abs‘(𝑦 − 𝑐)) = (abs‘(𝑥 − 𝑐)))
135	134	eqeq1d 2763	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑥 → ((abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓)) ↔ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))))
136	126, 135	anbi12d 644	. . . . . . . . . 10 ⊢ (𝑦 = 𝑥 → ((𝑦 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ↔ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))))
137	136	2rexbidv 3228	. . . . . . . . 9 ⊢ (𝑦 = 𝑥 → (∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ↔ ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))))
138	137	2rexbidv 3228	. . . . . . . 8 ⊢ (𝑦 = 𝑥 → (∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ↔ ∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))))
139	138	2rexbidv 3228	. . . . . . 7 ⊢ (𝑦 = 𝑥 → (∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ↔ ∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))))
140		biidd 265	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑥 → (𝑎 ≠ 𝑑 ↔ 𝑎 ≠ 𝑑))
141		oveq1 7419	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑥 → (𝑦 − 𝑎) = (𝑥 − 𝑎))
142	141	fveq2d 6881	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑥 → (abs‘(𝑦 − 𝑎)) = (abs‘(𝑥 − 𝑎)))
143	142	eqeq1d 2763	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑥 → ((abs‘(𝑦 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ↔ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐))))
144		oveq1 7419	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑥 → (𝑦 − 𝑑) = (𝑥 − 𝑑))
145	144	fveq2d 6881	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑥 → (abs‘(𝑦 − 𝑑)) = (abs‘(𝑥 − 𝑑)))
146	145	eqeq1d 2763	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑥 → ((abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓)) ↔ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))
147	140, 143, 146	3anbi123d 1464	. . . . . . . . . 10 ⊢ (𝑦 = 𝑥 → ((𝑎 ≠ 𝑑 ∧ (abs‘(𝑦 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓))) ↔ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))))
148	147	2rexbidv 3228	. . . . . . . . 9 ⊢ (𝑦 = 𝑥 → (∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑦 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓))) ↔ ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))))
149	148	2rexbidv 3228	. . . . . . . 8 ⊢ (𝑦 = 𝑥 → (∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑦 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓))) ↔ ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))))
150	149	2rexbidv 3228	. . . . . . 7 ⊢ (𝑦 = 𝑥 → (∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑦 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓))) ↔ ∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))))
151	132, 139, 150	3orbi123d 1463	. . . . . 6 ⊢ (𝑦 = 𝑥 → ((∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑦 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) ↔ (∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))))
152	151	cbvrabv 3423	. . . . 5 ⊢ {𝑦 ∈ ℂ ∣ (∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑦 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓))))} = {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}
153	125, 152	eqtri 2784	. . . 4 ⊢ {𝑦 ∈ ℂ ∣ (∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑙 ∈ 𝑧 ∃𝑜 ∈ ℝ ∃𝑝 ∈ ℝ (𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑘 + (𝑝 · (𝑙 − 𝑘))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑘))) ≠ 0) ∨ ∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑚 ∈ 𝑧 ∃𝑞 ∈ 𝑧 ∃𝑜 ∈ ℝ (𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑘)) = (abs‘(𝑚 − 𝑞))) ∨ ∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑙 ∈ 𝑧 ∃𝑚 ∈ 𝑧 ∃𝑞 ∈ 𝑧 (𝑖 ≠ 𝑙 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑘)) ∧ (abs‘(𝑦 − 𝑙)) = (abs‘(𝑚 − 𝑞))))} = {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}
154	153	mpteq2i 5201	. . 3 ⊢ (𝑧 ∈ V ↦ {𝑦 ∈ ℂ ∣ (∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑙 ∈ 𝑧 ∃𝑜 ∈ ℝ ∃𝑝 ∈ ℝ (𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑘 + (𝑝 · (𝑙 − 𝑘))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑘))) ≠ 0) ∨ ∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑚 ∈ 𝑧 ∃𝑞 ∈ 𝑧 ∃𝑜 ∈ ℝ (𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑘)) = (abs‘(𝑚 − 𝑞))) ∨ ∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑙 ∈ 𝑧 ∃𝑚 ∈ 𝑧 ∃𝑞 ∈ 𝑧 (𝑖 ≠ 𝑙 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑘)) ∧ (abs‘(𝑦 − 𝑙)) = (abs‘(𝑚 − 𝑞))))}) = (𝑧 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))})
155		elequ2 2160	. . . . . . . 8 ⊢ (𝑧 = 𝑠 → (𝑎 ∈ 𝑧 ↔ 𝑎 ∈ 𝑠))
156		elequ2 2160	. . . . . . . . . 10 ⊢ (𝑧 = 𝑠 → (𝑏 ∈ 𝑧 ↔ 𝑏 ∈ 𝑠))
157		elequ2 2160	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑠 → (𝑐 ∈ 𝑧 ↔ 𝑐 ∈ 𝑠))
158		rexeq 3316	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑠 → (∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ↔ ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)))
159	157, 158	anbi12d 644	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑠 → ((𝑐 ∈ 𝑧 ∧ ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) ↔ (𝑐 ∈ 𝑠 ∧ ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0))))
160	159	rexbidv2 3183	. . . . . . . . . 10 ⊢ (𝑧 = 𝑠 → (∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ↔ ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)))
161	156, 160	anbi12d 644	. . . . . . . . 9 ⊢ (𝑧 = 𝑠 → ((𝑏 ∈ 𝑧 ∧ ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) ↔ (𝑏 ∈ 𝑠 ∧ ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0))))
162	161	rexbidv2 3183	. . . . . . . 8 ⊢ (𝑧 = 𝑠 → (∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ↔ ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)))
163	155, 162	anbi12d 644	. . . . . . 7 ⊢ (𝑧 = 𝑠 → ((𝑎 ∈ 𝑧 ∧ ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) ↔ (𝑎 ∈ 𝑠 ∧ ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0))))
164	163	rexbidv2 3183	. . . . . 6 ⊢ (𝑧 = 𝑠 → (∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ↔ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)))
165		elequ2 2160	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑠 → (𝑒 ∈ 𝑧 ↔ 𝑒 ∈ 𝑠))
166		rexeq 3316	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑠 → (∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ↔ ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))))
167	165, 166	anbi12d 644	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑠 → ((𝑒 ∈ 𝑧 ∧ ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ↔ (𝑒 ∈ 𝑠 ∧ ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))))))
168	167	rexbidv2 3183	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑠 → (∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ↔ ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))))
169	157, 168	anbi12d 644	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑠 → ((𝑐 ∈ 𝑧 ∧ ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ↔ (𝑐 ∈ 𝑠 ∧ ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))))))
170	169	rexbidv2 3183	. . . . . . . . . 10 ⊢ (𝑧 = 𝑠 → (∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ↔ ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))))
171	156, 170	anbi12d 644	. . . . . . . . 9 ⊢ (𝑧 = 𝑠 → ((𝑏 ∈ 𝑧 ∧ ∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ↔ (𝑏 ∈ 𝑠 ∧ ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))))))
172	171	rexbidv2 3183	. . . . . . . 8 ⊢ (𝑧 = 𝑠 → (∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ↔ ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))))
173	155, 172	anbi12d 644	. . . . . . 7 ⊢ (𝑧 = 𝑠 → ((𝑎 ∈ 𝑧 ∧ ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ↔ (𝑎 ∈ 𝑠 ∧ ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))))))
174	173	rexbidv2 3183	. . . . . 6 ⊢ (𝑧 = 𝑠 → (∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ↔ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))))
175		elequ2 2160	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑠 → (𝑑 ∈ 𝑧 ↔ 𝑑 ∈ 𝑠))
176		rexeq 3316	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑠 → (∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))) ↔ ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))))
177	165, 176	anbi12d 644	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑠 → ((𝑒 ∈ 𝑧 ∧ ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) ↔ (𝑒 ∈ 𝑠 ∧ ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))))
178	177	rexbidv2 3183	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑠 → (∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))) ↔ ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))))
179	175, 178	anbi12d 644	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑠 → ((𝑑 ∈ 𝑧 ∧ ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) ↔ (𝑑 ∈ 𝑠 ∧ ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))))
180	179	rexbidv2 3183	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑠 → (∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))) ↔ ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))))
181	157, 180	anbi12d 644	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑠 → ((𝑐 ∈ 𝑧 ∧ ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) ↔ (𝑐 ∈ 𝑠 ∧ ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))))
182	181	rexbidv2 3183	. . . . . . . . . 10 ⊢ (𝑧 = 𝑠 → (∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))) ↔ ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))))
183	156, 182	anbi12d 644	. . . . . . . . 9 ⊢ (𝑧 = 𝑠 → ((𝑏 ∈ 𝑧 ∧ ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) ↔ (𝑏 ∈ 𝑠 ∧ ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))))
184	183	rexbidv2 3183	. . . . . . . 8 ⊢ (𝑧 = 𝑠 → (∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))) ↔ ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))))
185	155, 184	anbi12d 644	. . . . . . 7 ⊢ (𝑧 = 𝑠 → ((𝑎 ∈ 𝑧 ∧ ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) ↔ (𝑎 ∈ 𝑠 ∧ ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))))
186	185	rexbidv2 3183	. . . . . 6 ⊢ (𝑧 = 𝑠 → (∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))) ↔ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))))
187	164, 174, 186	3orbi123d 1463	. . . . 5 ⊢ (𝑧 = 𝑠 → ((∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) ↔ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))))
188	187	rabbidv 3420	. . . 4 ⊢ (𝑧 = 𝑠 → {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))} = {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))})
189	188	cbvmptv 5209	. . 3 ⊢ (𝑧 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}) = (𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))})
190	154, 189	eqtri 2784	. 2 ⊢ (𝑧 ∈ V ↦ {𝑦 ∈ ℂ ∣ (∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑙 ∈ 𝑧 ∃𝑜 ∈ ℝ ∃𝑝 ∈ ℝ (𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑘 + (𝑝 · (𝑙 − 𝑘))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑘))) ≠ 0) ∨ ∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑚 ∈ 𝑧 ∃𝑞 ∈ 𝑧 ∃𝑜 ∈ ℝ (𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑘)) = (abs‘(𝑚 − 𝑞))) ∨ ∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑙 ∈ 𝑧 ∃𝑚 ∈ 𝑧 ∃𝑞 ∈ 𝑧 (𝑖 ≠ 𝑙 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑘)) ∧ (abs‘(𝑦 − 𝑙)) = (abs‘(𝑚 − 𝑞))))}) = (𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))})
191		rdgeq1 8403	. 2 ⊢ ((𝑧 ∈ V ↦ {𝑦 ∈ ℂ ∣ (∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑙 ∈ 𝑧 ∃𝑜 ∈ ℝ ∃𝑝 ∈ ℝ (𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑘 + (𝑝 · (𝑙 − 𝑘))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑘))) ≠ 0) ∨ ∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑚 ∈ 𝑧 ∃𝑞 ∈ 𝑧 ∃𝑜 ∈ ℝ (𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑘)) = (abs‘(𝑚 − 𝑞))) ∨ ∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑙 ∈ 𝑧 ∃𝑚 ∈ 𝑧 ∃𝑞 ∈ 𝑧 (𝑖 ≠ 𝑙 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑘)) ∧ (abs‘(𝑦 − 𝑙)) = (abs‘(𝑚 − 𝑞))))}) = (𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}) → rec((𝑧 ∈ V ↦ {𝑦 ∈ ℂ ∣ (∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑙 ∈ 𝑧 ∃𝑜 ∈ ℝ ∃𝑝 ∈ ℝ (𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑘 + (𝑝 · (𝑙 − 𝑘))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑘))) ≠ 0) ∨ ∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑚 ∈ 𝑧 ∃𝑞 ∈ 𝑧 ∃𝑜 ∈ ℝ (𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑘)) = (abs‘(𝑚 − 𝑞))) ∨ ∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑙 ∈ 𝑧 ∃𝑚 ∈ 𝑧 ∃𝑞 ∈ 𝑧 (𝑖 ≠ 𝑙 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑘)) ∧ (abs‘(𝑦 − 𝑙)) = (abs‘(𝑚 − 𝑞))))}), {0, 1}) = rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}), {0, 1}))
192	190, 191	ax-mp 5	1 ⊢ rec((𝑧 ∈ V ↦ {𝑦 ∈ ℂ ∣ (∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑙 ∈ 𝑧 ∃𝑜 ∈ ℝ ∃𝑝 ∈ ℝ (𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑘 + (𝑝 · (𝑙 − 𝑘))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑘))) ≠ 0) ∨ ∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑚 ∈ 𝑧 ∃𝑞 ∈ 𝑧 ∃𝑜 ∈ ℝ (𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑘)) = (abs‘(𝑚 − 𝑞))) ∨ ∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑙 ∈ 𝑧 ∃𝑚 ∈ 𝑧 ∃𝑞 ∈ 𝑧 (𝑖 ≠ 𝑙 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑘)) ∧ (abs‘(𝑦 − 𝑙)) = (abs‘(𝑚 − 𝑞))))}), {0, 1}) = rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}), {0, 1})

This proof depends on syntax axioms:   ∧ wa 401   ∨ w3o 1102   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145   ≠ wne 2956  ∃wrex 3087  {crab 3413  Vcvv 3451  {cpr 4586   ↦ cmpt 5186  ‘cfv 6531  (class class class)co 7412  reccrdg 8401  ℂcc 11179  ℝcr 11180  0cc0 11181  1c1 11182   + caddc 11184   · cmul 11186   − cmin 11522  ∗ccj 15243  ℑcim 15245  abscabs 15381

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-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-xp 5657  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6297  df-iota 6487  df-fv 6539  df-ov 7415  df-frecs 8283  df-wrecs 8314  df-recs 8363  df-rdg 8402

This theorem is used by:  constrllcl  34370  constrlccl  34371  constrcccl  34372  constrext2chn  34373  constrcn  34374  nn0constr  34375  constrcjcl  34382