Detailed syntax breakdown of Definition df-ifs
Step | Hyp | Ref
| Expression |
1 | | cifs 34316 |
. 2
class
InnerFiveSeg |
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 4572 |
. . . . . . . . . . . . . . 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 4572 |
. . . . . . . . . . . . . . 15
class
〈𝑐, 𝑑〉 |
14 | 8, 13 | cop 4572 |
. . . . . . . . . . . . . 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 4572 |
. . . . . . . . . . . . . . 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 4572 |
. . . . . . . . . . . . . . 15
class
〈𝑧, 𝑤〉 |
28 | 22, 27 | cop 4572 |
. . . . . . . . . . . . . 14
class
〈〈𝑥, 𝑦〉, 〈𝑧, 𝑤〉〉 |
29 | 17, 28 | wceq 1541 |
. . . . . . . . . . . . 13
wff 𝑞 = 〈〈𝑥, 𝑦〉, 〈𝑧, 𝑤〉〉 |
30 | 5, 10 | cop 4572 |
. . . . . . . . . . . . . . . 16
class
〈𝑎, 𝑐〉 |
31 | | cbtwn 27238 |
. . . . . . . . . . . . . . . 16
class
Btwn |
32 | 7, 30, 31 | wbr 5078 |
. . . . . . . . . . . . . . 15
wff 𝑏 Btwn 〈𝑎, 𝑐〉 |
33 | 19, 24 | cop 4572 |
. . . . . . . . . . . . . . . 16
class
〈𝑥, 𝑧〉 |
34 | 21, 33, 31 | wbr 5078 |
. . . . . . . . . . . . . . 15
wff 𝑦 Btwn 〈𝑥, 𝑧〉 |
35 | 32, 34 | wa 395 |
. . . . . . . . . . . . . 14
wff (𝑏 Btwn 〈𝑎, 𝑐〉 ∧ 𝑦 Btwn 〈𝑥, 𝑧〉) |
36 | | ccgr 27239 |
. . . . . . . . . . . . . . . 16
class
Cgr |
37 | 30, 33, 36 | wbr 5078 |
. . . . . . . . . . . . . . 15
wff 〈𝑎, 𝑐〉Cgr〈𝑥, 𝑧〉 |
38 | 7, 10 | cop 4572 |
. . . . . . . . . . . . . . . 16
class
〈𝑏, 𝑐〉 |
39 | 21, 24 | cop 4572 |
. . . . . . . . . . . . . . . 16
class
〈𝑦, 𝑧〉 |
40 | 38, 39, 36 | wbr 5078 |
. . . . . . . . . . . . . . 15
wff 〈𝑏, 𝑐〉Cgr〈𝑦, 𝑧〉 |
41 | 37, 40 | wa 395 |
. . . . . . . . . . . . . 14
wff
(〈𝑎, 𝑐〉Cgr〈𝑥, 𝑧〉 ∧ 〈𝑏, 𝑐〉Cgr〈𝑦, 𝑧〉) |
42 | 5, 12 | cop 4572 |
. . . . . . . . . . . . . . . 16
class
〈𝑎, 𝑑〉 |
43 | 19, 26 | cop 4572 |
. . . . . . . . . . . . . . . 16
class
〈𝑥, 𝑤〉 |
44 | 42, 43, 36 | wbr 5078 |
. . . . . . . . . . . . . . 15
wff 〈𝑎, 𝑑〉Cgr〈𝑥, 𝑤〉 |
45 | 13, 27, 36 | wbr 5078 |
. . . . . . . . . . . . . . 15
wff 〈𝑐, 𝑑〉Cgr〈𝑧, 𝑤〉 |
46 | 44, 45 | wa 395 |
. . . . . . . . . . . . . 14
wff
(〈𝑎, 𝑑〉Cgr〈𝑥, 𝑤〉 ∧ 〈𝑐, 𝑑〉Cgr〈𝑧, 𝑤〉) |
47 | 35, 41, 46 | w3a 1085 |
. . . . . . . . . . . . 13
wff ((𝑏 Btwn 〈𝑎, 𝑐〉 ∧ 𝑦 Btwn 〈𝑥, 𝑧〉) ∧ (〈𝑎, 𝑐〉Cgr〈𝑥, 𝑧〉 ∧ 〈𝑏, 𝑐〉Cgr〈𝑦, 𝑧〉) ∧ (〈𝑎, 𝑑〉Cgr〈𝑥, 𝑤〉 ∧ 〈𝑐, 𝑑〉Cgr〈𝑧, 𝑤〉)) |
48 | 15, 29, 47 | w3a 1085 |
. . . . . . . . . . . 12
wff (𝑝 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑞 = 〈〈𝑥, 𝑦〉, 〈𝑧, 𝑤〉〉 ∧ ((𝑏 Btwn 〈𝑎, 𝑐〉 ∧ 𝑦 Btwn 〈𝑥, 𝑧〉) ∧ (〈𝑎, 𝑐〉Cgr〈𝑥, 𝑧〉 ∧ 〈𝑏, 𝑐〉Cgr〈𝑦, 𝑧〉) ∧ (〈𝑎, 𝑑〉Cgr〈𝑥, 𝑤〉 ∧ 〈𝑐, 𝑑〉Cgr〈𝑧, 𝑤〉))) |
49 | | vn |
. . . . . . . . . . . . . 14
setvar 𝑛 |
50 | 49 | cv 1540 |
. . . . . . . . . . . . 13
class 𝑛 |
51 | | cee 27237 |
. . . . . . . . . . . . 13
class
𝔼 |
52 | 50, 51 | cfv 6430 |
. . . . . . . . . . . 12
class
(𝔼‘𝑛) |
53 | 48, 25, 52 | wrex 3066 |
. . . . . . . . . . 11
wff
∃𝑤 ∈
(𝔼‘𝑛)(𝑝 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑞 = 〈〈𝑥, 𝑦〉, 〈𝑧, 𝑤〉〉 ∧ ((𝑏 Btwn 〈𝑎, 𝑐〉 ∧ 𝑦 Btwn 〈𝑥, 𝑧〉) ∧ (〈𝑎, 𝑐〉Cgr〈𝑥, 𝑧〉 ∧ 〈𝑏, 𝑐〉Cgr〈𝑦, 𝑧〉) ∧ (〈𝑎, 𝑑〉Cgr〈𝑥, 𝑤〉 ∧ 〈𝑐, 𝑑〉Cgr〈𝑧, 𝑤〉))) |
54 | 53, 23, 52 | wrex 3066 |
. . . . . . . . . 10
wff
∃𝑧 ∈
(𝔼‘𝑛)∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑞 = 〈〈𝑥, 𝑦〉, 〈𝑧, 𝑤〉〉 ∧ ((𝑏 Btwn 〈𝑎, 𝑐〉 ∧ 𝑦 Btwn 〈𝑥, 𝑧〉) ∧ (〈𝑎, 𝑐〉Cgr〈𝑥, 𝑧〉 ∧ 〈𝑏, 𝑐〉Cgr〈𝑦, 𝑧〉) ∧ (〈𝑎, 𝑑〉Cgr〈𝑥, 𝑤〉 ∧ 〈𝑐, 𝑑〉Cgr〈𝑧, 𝑤〉))) |
55 | 54, 20, 52 | wrex 3066 |
. . . . . . . . 9
wff
∃𝑦 ∈
(𝔼‘𝑛)∃𝑧 ∈ (𝔼‘𝑛)∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑞 = 〈〈𝑥, 𝑦〉, 〈𝑧, 𝑤〉〉 ∧ ((𝑏 Btwn 〈𝑎, 𝑐〉 ∧ 𝑦 Btwn 〈𝑥, 𝑧〉) ∧ (〈𝑎, 𝑐〉Cgr〈𝑥, 𝑧〉 ∧ 〈𝑏, 𝑐〉Cgr〈𝑦, 𝑧〉) ∧ (〈𝑎, 𝑑〉Cgr〈𝑥, 𝑤〉 ∧ 〈𝑐, 𝑑〉Cgr〈𝑧, 𝑤〉))) |
56 | 55, 18, 52 | wrex 3066 |
. . . . . . . 8
wff
∃𝑥 ∈
(𝔼‘𝑛)∃𝑦 ∈ (𝔼‘𝑛)∃𝑧 ∈ (𝔼‘𝑛)∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑞 = 〈〈𝑥, 𝑦〉, 〈𝑧, 𝑤〉〉 ∧ ((𝑏 Btwn 〈𝑎, 𝑐〉 ∧ 𝑦 Btwn 〈𝑥, 𝑧〉) ∧ (〈𝑎, 𝑐〉Cgr〈𝑥, 𝑧〉 ∧ 〈𝑏, 𝑐〉Cgr〈𝑦, 𝑧〉) ∧ (〈𝑎, 𝑑〉Cgr〈𝑥, 𝑤〉 ∧ 〈𝑐, 𝑑〉Cgr〈𝑧, 𝑤〉))) |
57 | 56, 11, 52 | wrex 3066 |
. . . . . . 7
wff
∃𝑑 ∈
(𝔼‘𝑛)∃𝑥 ∈ (𝔼‘𝑛)∃𝑦 ∈ (𝔼‘𝑛)∃𝑧 ∈ (𝔼‘𝑛)∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑞 = 〈〈𝑥, 𝑦〉, 〈𝑧, 𝑤〉〉 ∧ ((𝑏 Btwn 〈𝑎, 𝑐〉 ∧ 𝑦 Btwn 〈𝑥, 𝑧〉) ∧ (〈𝑎, 𝑐〉Cgr〈𝑥, 𝑧〉 ∧ 〈𝑏, 𝑐〉Cgr〈𝑦, 𝑧〉) ∧ (〈𝑎, 𝑑〉Cgr〈𝑥, 𝑤〉 ∧ 〈𝑐, 𝑑〉Cgr〈𝑧, 𝑤〉))) |
58 | 57, 9, 52 | wrex 3066 |
. . . . . 6
wff
∃𝑐 ∈
(𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑥 ∈ (𝔼‘𝑛)∃𝑦 ∈ (𝔼‘𝑛)∃𝑧 ∈ (𝔼‘𝑛)∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑞 = 〈〈𝑥, 𝑦〉, 〈𝑧, 𝑤〉〉 ∧ ((𝑏 Btwn 〈𝑎, 𝑐〉 ∧ 𝑦 Btwn 〈𝑥, 𝑧〉) ∧ (〈𝑎, 𝑐〉Cgr〈𝑥, 𝑧〉 ∧ 〈𝑏, 𝑐〉Cgr〈𝑦, 𝑧〉) ∧ (〈𝑎, 𝑑〉Cgr〈𝑥, 𝑤〉 ∧ 〈𝑐, 𝑑〉Cgr〈𝑧, 𝑤〉))) |
59 | 58, 6, 52 | wrex 3066 |
. . . . 5
wff
∃𝑏 ∈
(𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑥 ∈ (𝔼‘𝑛)∃𝑦 ∈ (𝔼‘𝑛)∃𝑧 ∈ (𝔼‘𝑛)∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑞 = 〈〈𝑥, 𝑦〉, 〈𝑧, 𝑤〉〉 ∧ ((𝑏 Btwn 〈𝑎, 𝑐〉 ∧ 𝑦 Btwn 〈𝑥, 𝑧〉) ∧ (〈𝑎, 𝑐〉Cgr〈𝑥, 𝑧〉 ∧ 〈𝑏, 𝑐〉Cgr〈𝑦, 𝑧〉) ∧ (〈𝑎, 𝑑〉Cgr〈𝑥, 𝑤〉 ∧ 〈𝑐, 𝑑〉Cgr〈𝑧, 𝑤〉))) |
60 | 59, 4, 52 | wrex 3066 |
. . . 4
wff
∃𝑎 ∈
(𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑥 ∈ (𝔼‘𝑛)∃𝑦 ∈ (𝔼‘𝑛)∃𝑧 ∈ (𝔼‘𝑛)∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑞 = 〈〈𝑥, 𝑦〉, 〈𝑧, 𝑤〉〉 ∧ ((𝑏 Btwn 〈𝑎, 𝑐〉 ∧ 𝑦 Btwn 〈𝑥, 𝑧〉) ∧ (〈𝑎, 𝑐〉Cgr〈𝑥, 𝑧〉 ∧ 〈𝑏, 𝑐〉Cgr〈𝑦, 𝑧〉) ∧ (〈𝑎, 𝑑〉Cgr〈𝑥, 𝑤〉 ∧ 〈𝑐, 𝑑〉Cgr〈𝑧, 𝑤〉))) |
61 | | cn 11956 |
. . . 4
class
ℕ |
62 | 60, 49, 61 | wrex 3066 |
. . 3
wff
∃𝑛 ∈
ℕ ∃𝑎 ∈
(𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑥 ∈ (𝔼‘𝑛)∃𝑦 ∈ (𝔼‘𝑛)∃𝑧 ∈ (𝔼‘𝑛)∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑞 = 〈〈𝑥, 𝑦〉, 〈𝑧, 𝑤〉〉 ∧ ((𝑏 Btwn 〈𝑎, 𝑐〉 ∧ 𝑦 Btwn 〈𝑥, 𝑧〉) ∧ (〈𝑎, 𝑐〉Cgr〈𝑥, 𝑧〉 ∧ 〈𝑏, 𝑐〉Cgr〈𝑦, 𝑧〉) ∧ (〈𝑎, 𝑑〉Cgr〈𝑥, 𝑤〉 ∧ 〈𝑐, 𝑑〉Cgr〈𝑧, 𝑤〉))) |
63 | 62, 2, 16 | copab 5140 |
. 2
class
{〈𝑝, 𝑞〉 ∣ ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑥 ∈ (𝔼‘𝑛)∃𝑦 ∈ (𝔼‘𝑛)∃𝑧 ∈ (𝔼‘𝑛)∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑞 = 〈〈𝑥, 𝑦〉, 〈𝑧, 𝑤〉〉 ∧ ((𝑏 Btwn 〈𝑎, 𝑐〉 ∧ 𝑦 Btwn 〈𝑥, 𝑧〉) ∧ (〈𝑎, 𝑐〉Cgr〈𝑥, 𝑧〉 ∧ 〈𝑏, 𝑐〉Cgr〈𝑦, 𝑧〉) ∧ (〈𝑎, 𝑑〉Cgr〈𝑥, 𝑤〉 ∧ 〈𝑐, 𝑑〉Cgr〈𝑧, 𝑤〉)))} |
64 | 1, 63 | wceq 1541 |
1
wff
InnerFiveSeg = {〈𝑝,
𝑞〉 ∣
∃𝑛 ∈ ℕ
∃𝑎 ∈
(𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑥 ∈ (𝔼‘𝑛)∃𝑦 ∈ (𝔼‘𝑛)∃𝑧 ∈ (𝔼‘𝑛)∃𝑤 ∈ (𝔼‘𝑛)(𝑝 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑞 = 〈〈𝑥, 𝑦〉, 〈𝑧, 𝑤〉〉 ∧ ((𝑏 Btwn 〈𝑎, 𝑐〉 ∧ 𝑦 Btwn 〈𝑥, 𝑧〉) ∧ (〈𝑎, 𝑐〉Cgr〈𝑥, 𝑧〉 ∧ 〈𝑏, 𝑐〉Cgr〈𝑦, 𝑧〉) ∧ (〈𝑎, 𝑑〉Cgr〈𝑥, 𝑤〉 ∧ 〈𝑐, 𝑑〉Cgr〈𝑧, 𝑤〉)))} |