Definition df-constr 33723

Description: Define the set of geometrically constructible points, by recursively adding the line-line, line-circle and circle-circle intersections constructions using points in a previous iteration. (Contributed by Saveliy Skresanov, 19-Jan-2025.)

Assertion

Ref	Expression
df-constr	⊢ Constr = (rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}), {0, 1}) “ ω)

Distinct variable group:   𝑎,𝑏,𝑐,𝑑,𝑒,𝑓,𝑟,𝑠,𝑡,𝑥

Detailed syntax breakdown of Definition df-constr

Step	Hyp	Ref	Expression
1		cconstr 33722	. 2 class Constr
2		vs	. . . . 5 setvar 𝑠
3		cvv 3488	. . . . 5 class V
4		vx	. . . . . . . . . . . . . . . 16 setvar 𝑥
5	4	cv 1536	. . . . . . . . . . . . . . 15 class 𝑥
6		va	. . . . . . . . . . . . . . . . 17 setvar 𝑎
7	6	cv 1536	. . . . . . . . . . . . . . . 16 class 𝑎
8		vt	. . . . . . . . . . . . . . . . . 18 setvar 𝑡
9	8	cv 1536	. . . . . . . . . . . . . . . . 17 class 𝑡
10		vb	. . . . . . . . . . . . . . . . . . 19 setvar 𝑏
11	10	cv 1536	. . . . . . . . . . . . . . . . . 18 class 𝑏
12		cmin 11522	. . . . . . . . . . . . . . . . . 18 class −
13	11, 7, 12	co 7450	. . . . . . . . . . . . . . . . 17 class (𝑏 − 𝑎)
14		cmul 11191	. . . . . . . . . . . . . . . . 17 class ·
15	9, 13, 14	co 7450	. . . . . . . . . . . . . . . 16 class (𝑡 · (𝑏 − 𝑎))
16		caddc 11189	. . . . . . . . . . . . . . . 16 class +
17	7, 15, 16	co 7450	. . . . . . . . . . . . . . 15 class (𝑎 + (𝑡 · (𝑏 − 𝑎)))
18	5, 17	wceq 1537	. . . . . . . . . . . . . 14 wff 𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎)))
19		vc	. . . . . . . . . . . . . . . . 17 setvar 𝑐
20	19	cv 1536	. . . . . . . . . . . . . . . 16 class 𝑐
21		vr	. . . . . . . . . . . . . . . . . 18 setvar 𝑟
22	21	cv 1536	. . . . . . . . . . . . . . . . 17 class 𝑟
23		vd	. . . . . . . . . . . . . . . . . . 19 setvar 𝑑
24	23	cv 1536	. . . . . . . . . . . . . . . . . 18 class 𝑑
25	24, 20, 12	co 7450	. . . . . . . . . . . . . . . . 17 class (𝑑 − 𝑐)
26	22, 25, 14	co 7450	. . . . . . . . . . . . . . . 16 class (𝑟 · (𝑑 − 𝑐))
27	20, 26, 16	co 7450	. . . . . . . . . . . . . . 15 class (𝑐 + (𝑟 · (𝑑 − 𝑐)))
28	5, 27	wceq 1537	. . . . . . . . . . . . . 14 wff 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐)))
29		ccj 15147	. . . . . . . . . . . . . . . . . 18 class ∗
30	13, 29	cfv 6575	. . . . . . . . . . . . . . . . 17 class (∗‘(𝑏 − 𝑎))
31	30, 25, 14	co 7450	. . . . . . . . . . . . . . . 16 class ((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))
32		cim 15149	. . . . . . . . . . . . . . . 16 class ℑ
33	31, 32	cfv 6575	. . . . . . . . . . . . . . 15 class (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐)))
34		cc0 11186	. . . . . . . . . . . . . . 15 class 0
35	33, 34	wne 2946	. . . . . . . . . . . . . 14 wff (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0
36	18, 28, 35	w3a 1087	. . . . . . . . . . . . 13 wff (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)
37		cr 11185	. . . . . . . . . . . . 13 class ℝ
38	36, 21, 37	wrex 3076	. . . . . . . . . . . 12 wff ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)
39	38, 8, 37	wrex 3076	. . . . . . . . . . 11 wff ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)
40	2	cv 1536	. . . . . . . . . . 11 class 𝑠
41	39, 23, 40	wrex 3076	. . . . . . . . . 10 wff ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)
42	41, 19, 40	wrex 3076	. . . . . . . . 9 wff ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)
43	42, 10, 40	wrex 3076	. . . . . . . 8 wff ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)
44	43, 6, 40	wrex 3076	. . . . . . 7 wff ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)
45	5, 20, 12	co 7450	. . . . . . . . . . . . . . . 16 class (𝑥 − 𝑐)
46		cabs 15285	. . . . . . . . . . . . . . . 16 class abs
47	45, 46	cfv 6575	. . . . . . . . . . . . . . 15 class (abs‘(𝑥 − 𝑐))
48		ve	. . . . . . . . . . . . . . . . . 18 setvar 𝑒
49	48	cv 1536	. . . . . . . . . . . . . . . . 17 class 𝑒
50		vf	. . . . . . . . . . . . . . . . . 18 setvar 𝑓
51	50	cv 1536	. . . . . . . . . . . . . . . . 17 class 𝑓
52	49, 51, 12	co 7450	. . . . . . . . . . . . . . . 16 class (𝑒 − 𝑓)
53	52, 46	cfv 6575	. . . . . . . . . . . . . . 15 class (abs‘(𝑒 − 𝑓))
54	47, 53	wceq 1537	. . . . . . . . . . . . . 14 wff (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))
55	18, 54	wa 395	. . . . . . . . . . . . 13 wff (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))
56	55, 8, 37	wrex 3076	. . . . . . . . . . . 12 wff ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))
57	56, 50, 40	wrex 3076	. . . . . . . . . . 11 wff ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))
58	57, 48, 40	wrex 3076	. . . . . . . . . 10 wff ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))
59	58, 19, 40	wrex 3076	. . . . . . . . 9 wff ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))
60	59, 10, 40	wrex 3076	. . . . . . . 8 wff ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))
61	60, 6, 40	wrex 3076	. . . . . . 7 wff ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))
62	7, 24	wne 2946	. . . . . . . . . . . . . 14 wff 𝑎 ≠ 𝑑
63	5, 7, 12	co 7450	. . . . . . . . . . . . . . . 16 class (𝑥 − 𝑎)
64	63, 46	cfv 6575	. . . . . . . . . . . . . . 15 class (abs‘(𝑥 − 𝑎))
65	11, 20, 12	co 7450	. . . . . . . . . . . . . . . 16 class (𝑏 − 𝑐)
66	65, 46	cfv 6575	. . . . . . . . . . . . . . 15 class (abs‘(𝑏 − 𝑐))
67	64, 66	wceq 1537	. . . . . . . . . . . . . 14 wff (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐))
68	5, 24, 12	co 7450	. . . . . . . . . . . . . . . 16 class (𝑥 − 𝑑)
69	68, 46	cfv 6575	. . . . . . . . . . . . . . 15 class (abs‘(𝑥 − 𝑑))
70	69, 53	wceq 1537	. . . . . . . . . . . . . 14 wff (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))
71	62, 67, 70	w3a 1087	. . . . . . . . . . . . 13 wff (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))
72	71, 50, 40	wrex 3076	. . . . . . . . . . . 12 wff ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))
73	72, 48, 40	wrex 3076	. . . . . . . . . . 11 wff ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))
74	73, 23, 40	wrex 3076	. . . . . . . . . 10 wff ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))
75	74, 19, 40	wrex 3076	. . . . . . . . 9 wff ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))
76	75, 10, 40	wrex 3076	. . . . . . . 8 wff ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))
77	76, 6, 40	wrex 3076	. . . . . . 7 wff ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))
78	44, 61, 77	w3o 1086	. . . . . 6 wff (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))
79		cc 11184	. . . . . 6 class ℂ
80	78, 4, 79	crab 3443	. . . . 5 class {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}
81	2, 3, 80	cmpt 5249	. . . 4 class (𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))})
82		c1 11187	. . . . 5 class 1
83	34, 82	cpr 4650	. . . 4 class {0, 1}
84	81, 83	crdg 8467	. . 3 class rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}), {0, 1})
85		com 7905	. . 3 class ω
86	84, 85	cima 5703	. 2 class (rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}), {0, 1}) “ ω)
87	1, 86	wceq 1537	1 wff Constr = (rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}), {0, 1}) “ ω)

This definition is referenced by: (None)