Step | Hyp | Ref
| Expression |
1 | | cltrr 11062 |
. 2
class
<ℝ |
2 | | vx |
. . . . . . 7
setvar 𝑥 |
3 | 2 | cv 1541 |
. . . . . 6
class 𝑥 |
4 | | cr 11057 |
. . . . . 6
class
ℝ |
5 | 3, 4 | wcel 2107 |
. . . . 5
wff 𝑥 ∈ ℝ |
6 | | vy |
. . . . . . 7
setvar 𝑦 |
7 | 6 | cv 1541 |
. . . . . 6
class 𝑦 |
8 | 7, 4 | wcel 2107 |
. . . . 5
wff 𝑦 ∈ ℝ |
9 | 5, 8 | wa 397 |
. . . 4
wff (𝑥 ∈ ℝ ∧ 𝑦 ∈
ℝ) |
10 | | vz |
. . . . . . . . . . 11
setvar 𝑧 |
11 | 10 | cv 1541 |
. . . . . . . . . 10
class 𝑧 |
12 | | c0r 10809 |
. . . . . . . . . 10
class
0R |
13 | 11, 12 | cop 4597 |
. . . . . . . . 9
class
⟨𝑧,
0R⟩ |
14 | 3, 13 | wceq 1542 |
. . . . . . . 8
wff 𝑥 = ⟨𝑧,
0R⟩ |
15 | | vw |
. . . . . . . . . . 11
setvar 𝑤 |
16 | 15 | cv 1541 |
. . . . . . . . . 10
class 𝑤 |
17 | 16, 12 | cop 4597 |
. . . . . . . . 9
class
⟨𝑤,
0R⟩ |
18 | 7, 17 | wceq 1542 |
. . . . . . . 8
wff 𝑦 = ⟨𝑤,
0R⟩ |
19 | 14, 18 | wa 397 |
. . . . . . 7
wff (𝑥 = ⟨𝑧, 0R⟩ ∧
𝑦 = ⟨𝑤,
0R⟩) |
20 | | cltr 10814 |
. . . . . . . 8
class
<R |
21 | 11, 16, 20 | wbr 5110 |
. . . . . . 7
wff 𝑧 <R
𝑤 |
22 | 19, 21 | wa 397 |
. . . . . 6
wff ((𝑥 = ⟨𝑧, 0R⟩ ∧
𝑦 = ⟨𝑤,
0R⟩) ∧ 𝑧 <R 𝑤) |
23 | 22, 15 | wex 1782 |
. . . . 5
wff
∃𝑤((𝑥 = ⟨𝑧, 0R⟩ ∧
𝑦 = ⟨𝑤,
0R⟩) ∧ 𝑧 <R 𝑤) |
24 | 23, 10 | wex 1782 |
. . . 4
wff
∃𝑧∃𝑤((𝑥 = ⟨𝑧, 0R⟩ ∧
𝑦 = ⟨𝑤,
0R⟩) ∧ 𝑧 <R 𝑤) |
25 | 9, 24 | wa 397 |
. . 3
wff ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧
∃𝑧∃𝑤((𝑥 = ⟨𝑧, 0R⟩ ∧
𝑦 = ⟨𝑤,
0R⟩) ∧ 𝑧 <R 𝑤)) |
26 | 25, 2, 6 | copab 5172 |
. 2
class
{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧
∃𝑧∃𝑤((𝑥 = ⟨𝑧, 0R⟩ ∧
𝑦 = ⟨𝑤,
0R⟩) ∧ 𝑧 <R 𝑤))} |
27 | 1, 26 | wceq 1542 |
1
wff
<ℝ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ∃𝑧∃𝑤((𝑥 = ⟨𝑧, 0R⟩ ∧
𝑦 = ⟨𝑤,
0R⟩) ∧ 𝑧 <R 𝑤))} |