Detailed syntax breakdown of Definition df-ltxr
Step | Hyp | Ref
| Expression |
1 | | clt 11009 |
. 2
class
< |
2 | | vx |
. . . . . . 7
setvar 𝑥 |
3 | 2 | cv 1538 |
. . . . . 6
class 𝑥 |
4 | | cr 10870 |
. . . . . 6
class
ℝ |
5 | 3, 4 | wcel 2106 |
. . . . 5
wff 𝑥 ∈ ℝ |
6 | | vy |
. . . . . . 7
setvar 𝑦 |
7 | 6 | cv 1538 |
. . . . . 6
class 𝑦 |
8 | 7, 4 | wcel 2106 |
. . . . 5
wff 𝑦 ∈ ℝ |
9 | | cltrr 10875 |
. . . . . 6
class
<ℝ |
10 | 3, 7, 9 | wbr 5074 |
. . . . 5
wff 𝑥 <ℝ 𝑦 |
11 | 5, 8, 10 | w3a 1086 |
. . . 4
wff (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦) |
12 | 11, 2, 6 | copab 5136 |
. . 3
class
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)} |
13 | | cmnf 11007 |
. . . . . . 7
class
-∞ |
14 | 13 | csn 4561 |
. . . . . 6
class
{-∞} |
15 | 4, 14 | cun 3885 |
. . . . 5
class (ℝ
∪ {-∞}) |
16 | | cpnf 11006 |
. . . . . 6
class
+∞ |
17 | 16 | csn 4561 |
. . . . 5
class
{+∞} |
18 | 15, 17 | cxp 5587 |
. . . 4
class ((ℝ
∪ {-∞}) × {+∞}) |
19 | 14, 4 | cxp 5587 |
. . . 4
class
({-∞} × ℝ) |
20 | 18, 19 | cun 3885 |
. . 3
class
(((ℝ ∪ {-∞}) × {+∞}) ∪ ({-∞}
× ℝ)) |
21 | 12, 20 | cun 3885 |
. 2
class
({〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)} ∪ (((ℝ ∪
{-∞}) × {+∞}) ∪ ({-∞} ×
ℝ))) |
22 | 1, 21 | wceq 1539 |
1
wff < =
({〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦)} ∪ (((ℝ ∪
{-∞}) × {+∞}) ∪ ({-∞} ×
ℝ))) |