Detailed syntax breakdown of Definition df-ap
Step | Hyp | Ref
| Expression |
1 | | cap 7365 |
. 2
class # |
2 | | vx |
. . . . . . . . . . 11
setvar x |
3 | 2 | cv 1241 |
. . . . . . . . . 10
class x |
4 | | vr |
. . . . . . . . . . . 12
setvar 𝑟 |
5 | 4 | cv 1241 |
. . . . . . . . . . 11
class 𝑟 |
6 | | ci 6713 |
. . . . . . . . . . . 12
class i |
7 | | vs |
. . . . . . . . . . . . 13
setvar 𝑠 |
8 | 7 | cv 1241 |
. . . . . . . . . . . 12
class 𝑠 |
9 | | cmul 6716 |
. . . . . . . . . . . 12
class · |
10 | 6, 8, 9 | co 5455 |
. . . . . . . . . . 11
class (i · 𝑠) |
11 | | caddc 6714 |
. . . . . . . . . . 11
class + |
12 | 5, 10, 11 | co 5455 |
. . . . . . . . . 10
class (𝑟 + (i · 𝑠)) |
13 | 3, 12 | wceq 1242 |
. . . . . . . . 9
wff x = (𝑟 + (i · 𝑠)) |
14 | | vy |
. . . . . . . . . . 11
setvar y |
15 | 14 | cv 1241 |
. . . . . . . . . 10
class y |
16 | | vt |
. . . . . . . . . . . 12
setvar 𝑡 |
17 | 16 | cv 1241 |
. . . . . . . . . . 11
class 𝑡 |
18 | | vu |
. . . . . . . . . . . . 13
setvar u |
19 | 18 | cv 1241 |
. . . . . . . . . . . 12
class u |
20 | 6, 19, 9 | co 5455 |
. . . . . . . . . . 11
class (i · u) |
21 | 17, 20, 11 | co 5455 |
. . . . . . . . . 10
class (𝑡 + (i · u)) |
22 | 15, 21 | wceq 1242 |
. . . . . . . . 9
wff y = (𝑡 + (i · u)) |
23 | 13, 22 | wa 97 |
. . . . . . . 8
wff (x = (𝑟 + (i · 𝑠)) ∧
y = (𝑡 + (i · u))) |
24 | | creap 7358 |
. . . . . . . . . 10
class
#ℝ |
25 | 5, 17, 24 | wbr 3755 |
. . . . . . . . 9
wff 𝑟 #ℝ 𝑡 |
26 | 8, 19, 24 | wbr 3755 |
. . . . . . . . 9
wff 𝑠 #ℝ u |
27 | 25, 26 | wo 628 |
. . . . . . . 8
wff (𝑟 #ℝ 𝑡 ∨ 𝑠 #ℝ u) |
28 | 23, 27 | wa 97 |
. . . . . . 7
wff ((x = (𝑟 + (i · 𝑠)) ∧
y = (𝑡 + (i · u))) ∧ (𝑟 #ℝ 𝑡 ∨
𝑠 #ℝ u)) |
29 | | cr 6710 |
. . . . . . 7
class ℝ |
30 | 28, 18, 29 | wrex 2301 |
. . . . . 6
wff ∃u ∈ ℝ ((x =
(𝑟 + (i · 𝑠)) ∧ y = (𝑡 + (i · u))) ∧ (𝑟 #ℝ 𝑡 ∨
𝑠 #ℝ u)) |
31 | 30, 16, 29 | wrex 2301 |
. . . . 5
wff ∃𝑡 ∈ ℝ
∃u ∈ ℝ ((x =
(𝑟 + (i · 𝑠)) ∧ y = (𝑡 + (i · u))) ∧ (𝑟 #ℝ 𝑡 ∨
𝑠 #ℝ u)) |
32 | 31, 7, 29 | wrex 2301 |
. . . 4
wff ∃𝑠 ∈ ℝ
∃𝑡 ∈ ℝ
∃u ∈ ℝ ((x =
(𝑟 + (i · 𝑠)) ∧ y = (𝑡 + (i · u))) ∧ (𝑟 #ℝ 𝑡 ∨
𝑠 #ℝ u)) |
33 | 32, 4, 29 | wrex 2301 |
. . 3
wff ∃𝑟 ∈ ℝ
∃𝑠 ∈ ℝ
∃𝑡 ∈ ℝ
∃u ∈ ℝ ((x =
(𝑟 + (i · 𝑠)) ∧ y = (𝑡 + (i · u))) ∧ (𝑟 #ℝ 𝑡 ∨
𝑠 #ℝ u)) |
34 | 33, 2, 14 | copab 3808 |
. 2
class {〈x, y〉
∣ ∃𝑟 ∈ ℝ
∃𝑠 ∈ ℝ
∃𝑡 ∈ ℝ
∃u ∈ ℝ ((x =
(𝑟 + (i · 𝑠)) ∧ y = (𝑡 + (i · u))) ∧ (𝑟 #ℝ 𝑡 ∨
𝑠 #ℝ u))} |
35 | 1, 34 | wceq 1242 |
1
wff # = {〈x, y〉
∣ ∃𝑟 ∈ ℝ
∃𝑠 ∈ ℝ
∃𝑡 ∈ ℝ
∃u ∈ ℝ ((x =
(𝑟 + (i · 𝑠)) ∧ y = (𝑡 + (i · u))) ∧ (𝑟 #ℝ 𝑡 ∨
𝑠 #ℝ u))} |