Detailed syntax breakdown of Definition df-constr
Step | Hyp | Ref
| Expression |
1 | | cconstr 33712 |
. 2
class
Constr |
2 | | vs |
. . . . 5
setvar 𝑠 |
3 | | cvv 3482 |
. . . . 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 11516 |
. . . . . . . . . . . . . . . . . 18
class
− |
13 | 11, 7, 12 | co 7445 |
. . . . . . . . . . . . . . . . 17
class (𝑏 − 𝑎) |
14 | | cmul 11185 |
. . . . . . . . . . . . . . . . 17
class
· |
15 | 9, 13, 14 | co 7445 |
. . . . . . . . . . . . . . . 16
class (𝑡 · (𝑏 − 𝑎)) |
16 | | caddc 11183 |
. . . . . . . . . . . . . . . 16
class
+ |
17 | 7, 15, 16 | co 7445 |
. . . . . . . . . . . . . . 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 7445 |
. . . . . . . . . . . . . . . . 17
class (𝑑 − 𝑐) |
26 | 22, 25, 14 | co 7445 |
. . . . . . . . . . . . . . . 16
class (𝑟 · (𝑑 − 𝑐)) |
27 | 20, 26, 16 | co 7445 |
. . . . . . . . . . . . . . 15
class (𝑐 + (𝑟 · (𝑑 − 𝑐))) |
28 | 5, 27 | wceq 1537 |
. . . . . . . . . . . . . 14
wff 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) |
29 | | ccj 15141 |
. . . . . . . . . . . . . . . . . 18
class
∗ |
30 | 13, 29 | cfv 6572 |
. . . . . . . . . . . . . . . . 17
class
(∗‘(𝑏
− 𝑎)) |
31 | 30, 25, 14 | co 7445 |
. . . . . . . . . . . . . . . 16
class
((∗‘(𝑏
− 𝑎)) · (𝑑 − 𝑐)) |
32 | | cim 15143 |
. . . . . . . . . . . . . . . 16
class
ℑ |
33 | 31, 32 | cfv 6572 |
. . . . . . . . . . . . . . 15
class
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) |
34 | | cc0 11180 |
. . . . . . . . . . . . . . 15
class
0 |
35 | 33, 34 | wne 2942 |
. . . . . . . . . . . . . 14
wff
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0 |
36 | 18, 28, 35 | w3a 1087 |
. . . . . . . . . . . . 13
wff (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) |
37 | | cr 11179 |
. . . . . . . . . . . . 13
class
ℝ |
38 | 36, 21, 37 | wrex 3072 |
. . . . . . . . . . . 12
wff
∃𝑟 ∈
ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) |
39 | 38, 8, 37 | wrex 3072 |
. . . . . . . . . . 11
wff
∃𝑡 ∈
ℝ ∃𝑟 ∈
ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) |
40 | 2 | cv 1536 |
. . . . . . . . . . 11
class 𝑠 |
41 | 39, 23, 40 | wrex 3072 |
. . . . . . . . . 10
wff
∃𝑑 ∈
𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) |
42 | 41, 19, 40 | wrex 3072 |
. . . . . . . . 9
wff
∃𝑐 ∈
𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) |
43 | 42, 10, 40 | wrex 3072 |
. . . . . . . 8
wff
∃𝑏 ∈
𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) |
44 | 43, 6, 40 | wrex 3072 |
. . . . . . 7
wff
∃𝑎 ∈
𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) |
45 | 5, 20, 12 | co 7445 |
. . . . . . . . . . . . . . . 16
class (𝑥 − 𝑐) |
46 | | cabs 15279 |
. . . . . . . . . . . . . . . 16
class
abs |
47 | 45, 46 | cfv 6572 |
. . . . . . . . . . . . . . 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 7445 |
. . . . . . . . . . . . . . . 16
class (𝑒 − 𝑓) |
53 | 52, 46 | cfv 6572 |
. . . . . . . . . . . . . . 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 3072 |
. . . . . . . . . . . 12
wff
∃𝑡 ∈
ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) |
57 | 56, 50, 40 | wrex 3072 |
. . . . . . . . . . 11
wff
∃𝑓 ∈
𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) |
58 | 57, 48, 40 | wrex 3072 |
. . . . . . . . . 10
wff
∃𝑒 ∈
𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) |
59 | 58, 19, 40 | wrex 3072 |
. . . . . . . . 9
wff
∃𝑐 ∈
𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) |
60 | 59, 10, 40 | wrex 3072 |
. . . . . . . 8
wff
∃𝑏 ∈
𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) |
61 | 60, 6, 40 | wrex 3072 |
. . . . . . 7
wff
∃𝑎 ∈
𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) |
62 | 7, 24 | wne 2942 |
. . . . . . . . . . . . . 14
wff 𝑎 ≠ 𝑑 |
63 | 5, 7, 12 | co 7445 |
. . . . . . . . . . . . . . . 16
class (𝑥 − 𝑎) |
64 | 63, 46 | cfv 6572 |
. . . . . . . . . . . . . . 15
class
(abs‘(𝑥
− 𝑎)) |
65 | 11, 20, 12 | co 7445 |
. . . . . . . . . . . . . . . 16
class (𝑏 − 𝑐) |
66 | 65, 46 | cfv 6572 |
. . . . . . . . . . . . . . 15
class
(abs‘(𝑏
− 𝑐)) |
67 | 64, 66 | wceq 1537 |
. . . . . . . . . . . . . 14
wff
(abs‘(𝑥
− 𝑎)) =
(abs‘(𝑏 − 𝑐)) |
68 | 5, 24, 12 | co 7445 |
. . . . . . . . . . . . . . . 16
class (𝑥 − 𝑑) |
69 | 68, 46 | cfv 6572 |
. . . . . . . . . . . . . . 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 3072 |
. . . . . . . . . . . 12
wff
∃𝑓 ∈
𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))) |
73 | 72, 48, 40 | wrex 3072 |
. . . . . . . . . . 11
wff
∃𝑒 ∈
𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))) |
74 | 73, 23, 40 | wrex 3072 |
. . . . . . . . . 10
wff
∃𝑑 ∈
𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))) |
75 | 74, 19, 40 | wrex 3072 |
. . . . . . . . 9
wff
∃𝑐 ∈
𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))) |
76 | 75, 10, 40 | wrex 3072 |
. . . . . . . 8
wff
∃𝑏 ∈
𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))) |
77 | 76, 6, 40 | wrex 3072 |
. . . . . . 7
wff
∃𝑎 ∈
𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))) |
78 | 44, 61, 77 | w3o 1086 |
. . . . . 6
wff
(∃𝑎 ∈
𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) |
79 | | cc 11178 |
. . . . . 6
class
ℂ |
80 | 78, 4, 79 | crab 3438 |
. . . . 5
class {𝑥 ∈ ℂ ∣
(∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))} |
81 | 2, 3, 80 | cmpt 5252 |
. . . 4
class (𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣
(∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}) |
82 | | c1 11181 |
. . . . 5
class
1 |
83 | 34, 82 | cpr 4650 |
. . . 4
class {0,
1} |
84 | 81, 83 | crdg 8461 |
. . 3
class
rec((𝑠 ∈ V
↦ {𝑥 ∈ ℂ
∣ (∃𝑎 ∈
𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧
(ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}), {0, 1}) |
85 | | com 7899 |
. . 3
class
ω |
86 | 84, 85 | cima 5702 |
. 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}) “
ω) |