Detailed syntax breakdown of Definition df-ap
Step | Hyp | Ref
| Expression |
1 | | cap 8493 |
. 2
class
# |
2 | | vx |
. . . . . . . . . . 11
setvar 𝑥 |
3 | 2 | cv 1347 |
. . . . . . . . . 10
class 𝑥 |
4 | | vr |
. . . . . . . . . . . 12
setvar 𝑟 |
5 | 4 | cv 1347 |
. . . . . . . . . . 11
class 𝑟 |
6 | | ci 7769 |
. . . . . . . . . . . 12
class
i |
7 | | vs |
. . . . . . . . . . . . 13
setvar 𝑠 |
8 | 7 | cv 1347 |
. . . . . . . . . . . 12
class 𝑠 |
9 | | cmul 7772 |
. . . . . . . . . . . 12
class
· |
10 | 6, 8, 9 | co 5851 |
. . . . . . . . . . 11
class (i
· 𝑠) |
11 | | caddc 7770 |
. . . . . . . . . . 11
class
+ |
12 | 5, 10, 11 | co 5851 |
. . . . . . . . . 10
class (𝑟 + (i · 𝑠)) |
13 | 3, 12 | wceq 1348 |
. . . . . . . . 9
wff 𝑥 = (𝑟 + (i · 𝑠)) |
14 | | vy |
. . . . . . . . . . 11
setvar 𝑦 |
15 | 14 | cv 1347 |
. . . . . . . . . 10
class 𝑦 |
16 | | vt |
. . . . . . . . . . . 12
setvar 𝑡 |
17 | 16 | cv 1347 |
. . . . . . . . . . 11
class 𝑡 |
18 | | vu |
. . . . . . . . . . . . 13
setvar 𝑢 |
19 | 18 | cv 1347 |
. . . . . . . . . . . 12
class 𝑢 |
20 | 6, 19, 9 | co 5851 |
. . . . . . . . . . 11
class (i
· 𝑢) |
21 | 17, 20, 11 | co 5851 |
. . . . . . . . . 10
class (𝑡 + (i · 𝑢)) |
22 | 15, 21 | wceq 1348 |
. . . . . . . . 9
wff 𝑦 = (𝑡 + (i · 𝑢)) |
23 | 13, 22 | wa 103 |
. . . . . . . 8
wff (𝑥 = (𝑟 + (i · 𝑠)) ∧ 𝑦 = (𝑡 + (i · 𝑢))) |
24 | | creap 8486 |
. . . . . . . . . 10
class
#ℝ |
25 | 5, 17, 24 | wbr 3987 |
. . . . . . . . 9
wff 𝑟 #ℝ 𝑡 |
26 | 8, 19, 24 | wbr 3987 |
. . . . . . . . 9
wff 𝑠 #ℝ 𝑢 |
27 | 25, 26 | wo 703 |
. . . . . . . 8
wff (𝑟 #ℝ 𝑡 ∨ 𝑠 #ℝ 𝑢) |
28 | 23, 27 | wa 103 |
. . . . . . 7
wff ((𝑥 = (𝑟 + (i · 𝑠)) ∧ 𝑦 = (𝑡 + (i · 𝑢))) ∧ (𝑟 #ℝ 𝑡 ∨ 𝑠 #ℝ 𝑢)) |
29 | | cr 7766 |
. . . . . . 7
class
ℝ |
30 | 28, 18, 29 | wrex 2449 |
. . . . . 6
wff
∃𝑢 ∈
ℝ ((𝑥 = (𝑟 + (i · 𝑠)) ∧ 𝑦 = (𝑡 + (i · 𝑢))) ∧ (𝑟 #ℝ 𝑡 ∨ 𝑠 #ℝ 𝑢)) |
31 | 30, 16, 29 | wrex 2449 |
. . . . 5
wff
∃𝑡 ∈
ℝ ∃𝑢 ∈
ℝ ((𝑥 = (𝑟 + (i · 𝑠)) ∧ 𝑦 = (𝑡 + (i · 𝑢))) ∧ (𝑟 #ℝ 𝑡 ∨ 𝑠 #ℝ 𝑢)) |
32 | 31, 7, 29 | wrex 2449 |
. . . 4
wff
∃𝑠 ∈
ℝ ∃𝑡 ∈
ℝ ∃𝑢 ∈
ℝ ((𝑥 = (𝑟 + (i · 𝑠)) ∧ 𝑦 = (𝑡 + (i · 𝑢))) ∧ (𝑟 #ℝ 𝑡 ∨ 𝑠 #ℝ 𝑢)) |
33 | 32, 4, 29 | wrex 2449 |
. . 3
wff
∃𝑟 ∈
ℝ ∃𝑠 ∈
ℝ ∃𝑡 ∈
ℝ ∃𝑢 ∈
ℝ ((𝑥 = (𝑟 + (i · 𝑠)) ∧ 𝑦 = (𝑡 + (i · 𝑢))) ∧ (𝑟 #ℝ 𝑡 ∨ 𝑠 #ℝ 𝑢)) |
34 | 33, 2, 14 | copab 4047 |
. 2
class
{〈𝑥, 𝑦〉 ∣ ∃𝑟 ∈ ℝ ∃𝑠 ∈ ℝ ∃𝑡 ∈ ℝ ∃𝑢 ∈ ℝ ((𝑥 = (𝑟 + (i · 𝑠)) ∧ 𝑦 = (𝑡 + (i · 𝑢))) ∧ (𝑟 #ℝ 𝑡 ∨ 𝑠 #ℝ 𝑢))} |
35 | 1, 34 | wceq 1348 |
1
wff # =
{〈𝑥, 𝑦〉 ∣ ∃𝑟 ∈ ℝ ∃𝑠 ∈ ℝ ∃𝑡 ∈ ℝ ∃𝑢 ∈ ℝ ((𝑥 = (𝑟 + (i · 𝑠)) ∧ 𝑦 = (𝑡 + (i · 𝑢))) ∧ (𝑟 #ℝ 𝑡 ∨ 𝑠 #ℝ 𝑢))} |