Step | Hyp | Ref
| Expression |
1 | | cofs 34558 |
. 2
class
OuterFiveSeg |
2 | | vp |
. . . . . . . . . . . . . . 15
setvar 𝑝 |
3 | 2 | cv 1540 |
. . . . . . . . . . . . . 14
class 𝑝 |
4 | | va |
. . . . . . . . . . . . . . . . 17
setvar 𝑎 |
5 | 4 | cv 1540 |
. . . . . . . . . . . . . . . 16
class 𝑎 |
6 | | vb |
. . . . . . . . . . . . . . . . 17
setvar 𝑏 |
7 | 6 | cv 1540 |
. . . . . . . . . . . . . . . 16
class 𝑏 |
8 | 5, 7 | cop 4592 |
. . . . . . . . . . . . . . 15
class
⟨𝑎, 𝑏⟩ |
9 | | vc |
. . . . . . . . . . . . . . . . 17
setvar 𝑐 |
10 | 9 | cv 1540 |
. . . . . . . . . . . . . . . 16
class 𝑐 |
11 | | vd |
. . . . . . . . . . . . . . . . 17
setvar 𝑑 |
12 | 11 | cv 1540 |
. . . . . . . . . . . . . . . 16
class 𝑑 |
13 | 10, 12 | cop 4592 |
. . . . . . . . . . . . . . 15
class
⟨𝑐, 𝑑⟩ |
14 | 8, 13 | cop 4592 |
. . . . . . . . . . . . . 14
class
⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ |
15 | 3, 14 | wceq 1541 |
. . . . . . . . . . . . 13
wff 𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ |
16 | | vq |
. . . . . . . . . . . . . . 15
setvar 𝑞 |
17 | 16 | cv 1540 |
. . . . . . . . . . . . . 14
class 𝑞 |
18 | | vx |
. . . . . . . . . . . . . . . . 17
setvar 𝑥 |
19 | 18 | cv 1540 |
. . . . . . . . . . . . . . . 16
class 𝑥 |
20 | | vy |
. . . . . . . . . . . . . . . . 17
setvar 𝑦 |
21 | 20 | cv 1540 |
. . . . . . . . . . . . . . . 16
class 𝑦 |
22 | 19, 21 | cop 4592 |
. . . . . . . . . . . . . . 15
class
⟨𝑥, 𝑦⟩ |
23 | | vz |
. . . . . . . . . . . . . . . . 17
setvar 𝑧 |
24 | 23 | cv 1540 |
. . . . . . . . . . . . . . . 16
class 𝑧 |
25 | | vw |
. . . . . . . . . . . . . . . . 17
setvar 𝑤 |
26 | 25 | cv 1540 |
. . . . . . . . . . . . . . . 16
class 𝑤 |
27 | 24, 26 | cop 4592 |
. . . . . . . . . . . . . . 15
class
⟨𝑧, 𝑤⟩ |
28 | 22, 27 | cop 4592 |
. . . . . . . . . . . . . 14
class
⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ |
29 | 17, 28 | wceq 1541 |
. . . . . . . . . . . . 13
wff 𝑞 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ |
30 | 5, 10 | cop 4592 |
. . . . . . . . . . . . . . . 16
class
⟨𝑎, 𝑐⟩ |
31 | | cbtwn 27836 |
. . . . . . . . . . . . . . . 16
class
Btwn |
32 | 7, 30, 31 | wbr 5105 |
. . . . . . . . . . . . . . 15
wff 𝑏 Btwn ⟨𝑎, 𝑐⟩ |
33 | 19, 24 | cop 4592 |
. . . . . . . . . . . . . . . 16
class
⟨𝑥, 𝑧⟩ |
34 | 21, 33, 31 | wbr 5105 |
. . . . . . . . . . . . . . 15
wff 𝑦 Btwn ⟨𝑥, 𝑧⟩ |
35 | 32, 34 | wa 396 |
. . . . . . . . . . . . . 14
wff (𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑦 Btwn ⟨𝑥, 𝑧⟩) |
36 | | ccgr 27837 |
. . . . . . . . . . . . . . . 16
class
Cgr |
37 | 8, 22, 36 | wbr 5105 |
. . . . . . . . . . . . . . 15
wff ⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩ |
38 | 7, 10 | cop 4592 |
. . . . . . . . . . . . . . . 16
class
⟨𝑏, 𝑐⟩ |
39 | 21, 24 | cop 4592 |
. . . . . . . . . . . . . . . 16
class
⟨𝑦, 𝑧⟩ |
40 | 38, 39, 36 | wbr 5105 |
. . . . . . . . . . . . . . 15
wff ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩ |
41 | 37, 40 | wa 396 |
. . . . . . . . . . . . . 14
wff
(⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩) |
42 | 5, 12 | cop 4592 |
. . . . . . . . . . . . . . . 16
class
⟨𝑎, 𝑑⟩ |
43 | 19, 26 | cop 4592 |
. . . . . . . . . . . . . . . 16
class
⟨𝑥, 𝑤⟩ |
44 | 42, 43, 36 | wbr 5105 |
. . . . . . . . . . . . . . 15
wff ⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩ |
45 | 7, 12 | cop 4592 |
. . . . . . . . . . . . . . . 16
class
⟨𝑏, 𝑑⟩ |
46 | 21, 26 | cop 4592 |
. . . . . . . . . . . . . . . 16
class
⟨𝑦, 𝑤⟩ |
47 | 45, 46, 36 | wbr 5105 |
. . . . . . . . . . . . . . 15
wff ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩ |
48 | 44, 47 | wa 396 |
. . . . . . . . . . . . . 14
wff
(⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩) |
49 | 35, 41, 48 | w3a 1087 |
. . . . . . . . . . . . 13
wff ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑦 Btwn ⟨𝑥, 𝑧⟩) ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩)) |
50 | 15, 29, 49 | w3a 1087 |
. . . . . . . . . . . 12
wff (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑦 Btwn ⟨𝑥, 𝑧⟩) ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩))) |
51 | | vn |
. . . . . . . . . . . . . 14
setvar 𝑛 |
52 | 51 | cv 1540 |
. . . . . . . . . . . . 13
class 𝑛 |
53 | | cee 27835 |
. . . . . . . . . . . . 13
class
𝔼 |
54 | 52, 53 | cfv 6496 |
. . . . . . . . . . . 12
class
(𝔼‘𝑛) |
55 | 50, 25, 54 | wrex 3073 |
. . . . . . . . . . 11
wff
∃𝑤 ∈
(𝔼‘𝑛)(𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑦 Btwn ⟨𝑥, 𝑧⟩) ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩))) |
56 | 55, 23, 54 | wrex 3073 |
. . . . . . . . . 10
wff
∃𝑧 ∈
(𝔼‘𝑛)∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑦 Btwn ⟨𝑥, 𝑧⟩) ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩))) |
57 | 56, 20, 54 | wrex 3073 |
. . . . . . . . 9
wff
∃𝑦 ∈
(𝔼‘𝑛)∃𝑧 ∈ (𝔼‘𝑛)∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑦 Btwn ⟨𝑥, 𝑧⟩) ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩))) |
58 | 57, 18, 54 | wrex 3073 |
. . . . . . . 8
wff
∃𝑥 ∈
(𝔼‘𝑛)∃𝑦 ∈ (𝔼‘𝑛)∃𝑧 ∈ (𝔼‘𝑛)∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑦 Btwn ⟨𝑥, 𝑧⟩) ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩))) |
59 | 58, 11, 54 | wrex 3073 |
. . . . . . 7
wff
∃𝑑 ∈
(𝔼‘𝑛)∃𝑥 ∈ (𝔼‘𝑛)∃𝑦 ∈ (𝔼‘𝑛)∃𝑧 ∈ (𝔼‘𝑛)∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑦 Btwn ⟨𝑥, 𝑧⟩) ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩))) |
60 | 59, 9, 54 | wrex 3073 |
. . . . . 6
wff
∃𝑐 ∈
(𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑥 ∈ (𝔼‘𝑛)∃𝑦 ∈ (𝔼‘𝑛)∃𝑧 ∈ (𝔼‘𝑛)∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑦 Btwn ⟨𝑥, 𝑧⟩) ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩))) |
61 | 60, 6, 54 | wrex 3073 |
. . . . 5
wff
∃𝑏 ∈
(𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑥 ∈ (𝔼‘𝑛)∃𝑦 ∈ (𝔼‘𝑛)∃𝑧 ∈ (𝔼‘𝑛)∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑦 Btwn ⟨𝑥, 𝑧⟩) ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩))) |
62 | 61, 4, 54 | wrex 3073 |
. . . 4
wff
∃𝑎 ∈
(𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑥 ∈ (𝔼‘𝑛)∃𝑦 ∈ (𝔼‘𝑛)∃𝑧 ∈ (𝔼‘𝑛)∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑦 Btwn ⟨𝑥, 𝑧⟩) ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩))) |
63 | | cn 12152 |
. . . 4
class
ℕ |
64 | 62, 51, 63 | wrex 3073 |
. . 3
wff
∃𝑛 ∈
ℕ ∃𝑎 ∈
(𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑥 ∈ (𝔼‘𝑛)∃𝑦 ∈ (𝔼‘𝑛)∃𝑧 ∈ (𝔼‘𝑛)∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑦 Btwn ⟨𝑥, 𝑧⟩) ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩))) |
65 | 64, 2, 16 | copab 5167 |
. 2
class
{⟨𝑝, 𝑞⟩ ∣ ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑥 ∈ (𝔼‘𝑛)∃𝑦 ∈ (𝔼‘𝑛)∃𝑧 ∈ (𝔼‘𝑛)∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑦 Btwn ⟨𝑥, 𝑧⟩) ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩)))} |
66 | 1, 65 | wceq 1541 |
1
wff
OuterFiveSeg = {⟨𝑝,
𝑞⟩ ∣
∃𝑛 ∈ ℕ
∃𝑎 ∈
(𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑥 ∈ (𝔼‘𝑛)∃𝑦 ∈ (𝔼‘𝑛)∃𝑧 ∈ (𝔼‘𝑛)∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑥, 𝑦⟩, ⟨𝑧, 𝑤⟩⟩ ∧ ((𝑏 Btwn ⟨𝑎, 𝑐⟩ ∧ 𝑦 Btwn ⟨𝑥, 𝑧⟩) ∧ (⟨𝑎, 𝑏⟩Cgr⟨𝑥, 𝑦⟩ ∧ ⟨𝑏, 𝑐⟩Cgr⟨𝑦, 𝑧⟩) ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑥, 𝑤⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑦, 𝑤⟩)))} |