Detailed syntax breakdown of Definition df-ltr
Step | Hyp | Ref
| Expression |
1 | | cltr 10371 |
. 2
class
<R |
2 | | vx |
. . . . . . 7
setvar 𝑥 |
3 | 2 | cv 1541 |
. . . . . 6
class 𝑥 |
4 | | cnr 10365 |
. . . . . 6
class
R |
5 | 3, 4 | wcel 2114 |
. . . . 5
wff 𝑥 ∈
R |
6 | | vy |
. . . . . . 7
setvar 𝑦 |
7 | 6 | cv 1541 |
. . . . . 6
class 𝑦 |
8 | 7, 4 | wcel 2114 |
. . . . 5
wff 𝑦 ∈
R |
9 | 5, 8 | wa 399 |
. . . 4
wff (𝑥 ∈ R ∧
𝑦 ∈
R) |
10 | | vz |
. . . . . . . . . . . . . 14
setvar 𝑧 |
11 | 10 | cv 1541 |
. . . . . . . . . . . . 13
class 𝑧 |
12 | | vw |
. . . . . . . . . . . . . 14
setvar 𝑤 |
13 | 12 | cv 1541 |
. . . . . . . . . . . . 13
class 𝑤 |
14 | 11, 13 | cop 4522 |
. . . . . . . . . . . 12
class
〈𝑧, 𝑤〉 |
15 | | cer 10364 |
. . . . . . . . . . . 12
class
~R |
16 | 14, 15 | cec 8318 |
. . . . . . . . . . 11
class
[〈𝑧, 𝑤〉]
~R |
17 | 3, 16 | wceq 1542 |
. . . . . . . . . 10
wff 𝑥 = [〈𝑧, 𝑤〉]
~R |
18 | | vv |
. . . . . . . . . . . . . 14
setvar 𝑣 |
19 | 18 | cv 1541 |
. . . . . . . . . . . . 13
class 𝑣 |
20 | | vu |
. . . . . . . . . . . . . 14
setvar 𝑢 |
21 | 20 | cv 1541 |
. . . . . . . . . . . . 13
class 𝑢 |
22 | 19, 21 | cop 4522 |
. . . . . . . . . . . 12
class
〈𝑣, 𝑢〉 |
23 | 22, 15 | cec 8318 |
. . . . . . . . . . 11
class
[〈𝑣, 𝑢〉]
~R |
24 | 7, 23 | wceq 1542 |
. . . . . . . . . 10
wff 𝑦 = [〈𝑣, 𝑢〉]
~R |
25 | 17, 24 | wa 399 |
. . . . . . . . 9
wff (𝑥 = [〈𝑧, 𝑤〉] ~R ∧
𝑦 = [〈𝑣, 𝑢〉] ~R
) |
26 | | cpp 10361 |
. . . . . . . . . . 11
class
+P |
27 | 11, 21, 26 | co 7170 |
. . . . . . . . . 10
class (𝑧 +P
𝑢) |
28 | 13, 19, 26 | co 7170 |
. . . . . . . . . 10
class (𝑤 +P
𝑣) |
29 | | cltp 10363 |
. . . . . . . . . 10
class
<P |
30 | 27, 28, 29 | wbr 5030 |
. . . . . . . . 9
wff (𝑧 +P
𝑢)<P (𝑤 +P
𝑣) |
31 | 25, 30 | wa 399 |
. . . . . . . 8
wff ((𝑥 = [〈𝑧, 𝑤〉] ~R ∧
𝑦 = [〈𝑣, 𝑢〉] ~R ) ∧
(𝑧
+P 𝑢)<P (𝑤 +P
𝑣)) |
32 | 31, 20 | wex 1786 |
. . . . . . 7
wff
∃𝑢((𝑥 = [〈𝑧, 𝑤〉] ~R ∧
𝑦 = [〈𝑣, 𝑢〉] ~R ) ∧
(𝑧
+P 𝑢)<P (𝑤 +P
𝑣)) |
33 | 32, 18 | wex 1786 |
. . . . . 6
wff
∃𝑣∃𝑢((𝑥 = [〈𝑧, 𝑤〉] ~R ∧
𝑦 = [〈𝑣, 𝑢〉] ~R ) ∧
(𝑧
+P 𝑢)<P (𝑤 +P
𝑣)) |
34 | 33, 12 | wex 1786 |
. . . . 5
wff
∃𝑤∃𝑣∃𝑢((𝑥 = [〈𝑧, 𝑤〉] ~R ∧
𝑦 = [〈𝑣, 𝑢〉] ~R ) ∧
(𝑧
+P 𝑢)<P (𝑤 +P
𝑣)) |
35 | 34, 10 | wex 1786 |
. . . 4
wff
∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = [〈𝑧, 𝑤〉] ~R ∧
𝑦 = [〈𝑣, 𝑢〉] ~R ) ∧
(𝑧
+P 𝑢)<P (𝑤 +P
𝑣)) |
36 | 9, 35 | wa 399 |
. . 3
wff ((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = [〈𝑧, 𝑤〉] ~R ∧
𝑦 = [〈𝑣, 𝑢〉] ~R ) ∧
(𝑧
+P 𝑢)<P (𝑤 +P
𝑣))) |
37 | 36, 2, 6 | copab 5092 |
. 2
class
{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = [〈𝑧, 𝑤〉] ~R ∧
𝑦 = [〈𝑣, 𝑢〉] ~R ) ∧
(𝑧
+P 𝑢)<P (𝑤 +P
𝑣)))} |
38 | 1, 37 | wceq 1542 |
1
wff
<R = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ R ∧ 𝑦 ∈ R) ∧
∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = [〈𝑧, 𝑤〉] ~R ∧
𝑦 = [〈𝑣, 𝑢〉] ~R ) ∧
(𝑧
+P 𝑢)<P (𝑤 +P
𝑣)))} |