Step | Hyp | Ref
| Expression |
1 | | csegle 34449 |
. 2
class
Seg≤ |
2 | | vp |
. . . . . . . . . . 11
setvar 𝑝 |
3 | 2 | cv 1538 |
. . . . . . . . . 10
class 𝑝 |
4 | | va |
. . . . . . . . . . . 12
setvar 𝑎 |
5 | 4 | cv 1538 |
. . . . . . . . . . 11
class 𝑎 |
6 | | vb |
. . . . . . . . . . . 12
setvar 𝑏 |
7 | 6 | cv 1538 |
. . . . . . . . . . 11
class 𝑏 |
8 | 5, 7 | cop 4571 |
. . . . . . . . . 10
class
⟨𝑎, 𝑏⟩ |
9 | 3, 8 | wceq 1539 |
. . . . . . . . 9
wff 𝑝 = ⟨𝑎, 𝑏⟩ |
10 | | vq |
. . . . . . . . . . 11
setvar 𝑞 |
11 | 10 | cv 1538 |
. . . . . . . . . 10
class 𝑞 |
12 | | vc |
. . . . . . . . . . . 12
setvar 𝑐 |
13 | 12 | cv 1538 |
. . . . . . . . . . 11
class 𝑐 |
14 | | vd |
. . . . . . . . . . . 12
setvar 𝑑 |
15 | 14 | cv 1538 |
. . . . . . . . . . 11
class 𝑑 |
16 | 13, 15 | cop 4571 |
. . . . . . . . . 10
class
⟨𝑐, 𝑑⟩ |
17 | 11, 16 | wceq 1539 |
. . . . . . . . 9
wff 𝑞 = ⟨𝑐, 𝑑⟩ |
18 | | vy |
. . . . . . . . . . . . 13
setvar 𝑦 |
19 | 18 | cv 1538 |
. . . . . . . . . . . 12
class 𝑦 |
20 | | cbtwn 27298 |
. . . . . . . . . . . 12
class
Btwn |
21 | 19, 16, 20 | wbr 5081 |
. . . . . . . . . . 11
wff 𝑦 Btwn ⟨𝑐, 𝑑⟩ |
22 | 13, 19 | cop 4571 |
. . . . . . . . . . . 12
class
⟨𝑐, 𝑦⟩ |
23 | | ccgr 27299 |
. . . . . . . . . . . 12
class
Cgr |
24 | 8, 22, 23 | wbr 5081 |
. . . . . . . . . . 11
wff ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩ |
25 | 21, 24 | wa 397 |
. . . . . . . . . 10
wff (𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩) |
26 | | vn |
. . . . . . . . . . . 12
setvar 𝑛 |
27 | 26 | cv 1538 |
. . . . . . . . . . 11
class 𝑛 |
28 | | cee 27297 |
. . . . . . . . . . 11
class
𝔼 |
29 | 27, 28 | cfv 6454 |
. . . . . . . . . 10
class
(𝔼‘𝑛) |
30 | 25, 18, 29 | wrex 3071 |
. . . . . . . . 9
wff
∃𝑦 ∈
(𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩) |
31 | 9, 17, 30 | w3a 1087 |
. . . . . . . 8
wff (𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩)) |
32 | 31, 14, 29 | wrex 3071 |
. . . . . . 7
wff
∃𝑑 ∈
(𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩)) |
33 | 32, 12, 29 | wrex 3071 |
. . . . . 6
wff
∃𝑐 ∈
(𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩)) |
34 | 33, 6, 29 | wrex 3071 |
. . . . 5
wff
∃𝑏 ∈
(𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩)) |
35 | 34, 4, 29 | wrex 3071 |
. . . 4
wff
∃𝑎 ∈
(𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩)) |
36 | | cn 12015 |
. . . 4
class
ℕ |
37 | 35, 26, 36 | wrex 3071 |
. . 3
wff
∃𝑛 ∈
ℕ ∃𝑎 ∈
(𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩)) |
38 | 37, 2, 10 | copab 5143 |
. 2
class
{⟨𝑝, 𝑞⟩ ∣ ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))} |
39 | 1, 38 | wceq 1539 |
1
wff
Seg≤ = {⟨𝑝, 𝑞⟩ ∣ ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ ∃𝑦 ∈ (𝔼‘𝑛)(𝑦 Btwn ⟨𝑐, 𝑑⟩ ∧ ⟨𝑎, 𝑏⟩Cgr⟨𝑐, 𝑦⟩))} |