Step | Hyp | Ref
| Expression |
1 | | uzuzle23 12515 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈
(ℤ≥‘2)) |
2 | | 0re 10865 |
. . . . 5
⊢ 0 ∈
ℝ |
3 | 2, 2 | axlowdimlem5 27069 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘2) → ({〈1, 0〉, 〈2, 0〉}
∪ ((3...𝑁) ×
{0})) ∈ (𝔼‘𝑁)) |
4 | 1, 3 | syl 17 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘3) → ({〈1, 0〉, 〈2, 0〉}
∪ ((3...𝑁) ×
{0})) ∈ (𝔼‘𝑁)) |
5 | | 1re 10863 |
. . . . 5
⊢ 1 ∈
ℝ |
6 | 5, 2 | axlowdimlem5 27069 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘2) → ({〈1, 1〉, 〈2, 0〉}
∪ ((3...𝑁) ×
{0})) ∈ (𝔼‘𝑁)) |
7 | 1, 6 | syl 17 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘3) → ({〈1, 1〉, 〈2, 0〉}
∪ ((3...𝑁) ×
{0})) ∈ (𝔼‘𝑁)) |
8 | 2, 5 | axlowdimlem5 27069 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘2) → ({〈1, 0〉, 〈2, 1〉}
∪ ((3...𝑁) ×
{0})) ∈ (𝔼‘𝑁)) |
9 | 1, 8 | syl 17 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘3) → ({〈1, 0〉, 〈2, 1〉}
∪ ((3...𝑁) ×
{0})) ∈ (𝔼‘𝑁)) |
10 | | eqid 2739 |
. . . 4
⊢ (𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) × {0}))))
= (𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪
(((1...𝑁) ∖ {3})
× {0})), ({〈(𝑘 +
1), 1〉} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})))) |
11 | 10 | axlowdimlem15 27079 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0})))):(1...(𝑁 −
1))–1-1→(𝔼‘𝑁)) |
12 | | eqid 2739 |
. . . . . 6
⊢
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})) = ({〈3,
-1〉} ∪ (((1...𝑁)
∖ {3}) × {0})) |
13 | | eqid 2739 |
. . . . . 6
⊢
({〈(𝑖 + 1),
1〉} ∪ (((1...𝑁)
∖ {(𝑖 + 1)}) ×
{0})) = ({〈(𝑖 + 1),
1〉} ∪ (((1...𝑁)
∖ {(𝑖 + 1)}) ×
{0})) |
14 | | eqid 2739 |
. . . . . 6
⊢
({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})) = ({〈1, 0〉,
〈2, 0〉} ∪ ((3...𝑁) × {0})) |
15 | 12, 13, 14, 2, 2 | axlowdimlem17 27081 |
. . . . 5
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑖 ∈ (2...(𝑁 − 1))) → 〈({〈3,
-1〉} ∪ (((1...𝑁)
∖ {3}) × {0})), ({〈1, 0〉, 〈2, 0〉} ∪
((3...𝑁) ×
{0}))〉Cgr〈({〈(𝑖 + 1), 1〉} ∪ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0})), ({〈1, 0〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))〉) |
16 | | eqid 2739 |
. . . . . 6
⊢
({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})) = ({〈1, 1〉,
〈2, 0〉} ∪ ((3...𝑁) × {0})) |
17 | 12, 13, 16, 5, 2 | axlowdimlem17 27081 |
. . . . 5
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑖 ∈ (2...(𝑁 − 1))) → 〈({〈3,
-1〉} ∪ (((1...𝑁)
∖ {3}) × {0})), ({〈1, 1〉, 〈2, 0〉} ∪
((3...𝑁) ×
{0}))〉Cgr〈({〈(𝑖 + 1), 1〉} ∪ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0})), ({〈1, 1〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))〉) |
18 | | eqid 2739 |
. . . . . 6
⊢
({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0})) = ({〈1, 0〉,
〈2, 1〉} ∪ ((3...𝑁) × {0})) |
19 | 12, 13, 18, 2, 5 | axlowdimlem17 27081 |
. . . . 5
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑖 ∈ (2...(𝑁 − 1))) → 〈({〈3,
-1〉} ∪ (((1...𝑁)
∖ {3}) × {0})), ({〈1, 0〉, 〈2, 1〉} ∪
((3...𝑁) ×
{0}))〉Cgr〈({〈(𝑖 + 1), 1〉} ∪ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0})), ({〈1, 0〉,
〈2, 1〉} ∪ ((3...𝑁) × {0}))〉) |
20 | | 1zzd 12238 |
. . . . . . . . . . . . . 14
⊢ ((3
∈ ℤ ∧ 𝑁
∈ ℤ ∧ 3 ≤ 𝑁) → 1 ∈ ℤ) |
21 | | peano2zm 12250 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈
ℤ) |
22 | 21 | 3ad2ant2 1136 |
. . . . . . . . . . . . . 14
⊢ ((3
∈ ℤ ∧ 𝑁
∈ ℤ ∧ 3 ≤ 𝑁) → (𝑁 − 1) ∈ ℤ) |
23 | | 2m1e1 11986 |
. . . . . . . . . . . . . . 15
⊢ (2
− 1) = 1 |
24 | | 2re 11934 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 ∈
ℝ |
25 | | 3re 11940 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 3 ∈
ℝ |
26 | | 2lt3 12032 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 <
3 |
27 | 24, 25, 26 | ltleii 10985 |
. . . . . . . . . . . . . . . . . . 19
⊢ 2 ≤
3 |
28 | | zre 12210 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) |
29 | | letr 10956 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((2
∈ ℝ ∧ 3 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((2 ≤ 3 ∧ 3
≤ 𝑁) → 2 ≤ 𝑁)) |
30 | 24, 25, 28, 29 | mp3an12i 1467 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℤ → ((2 ≤
3 ∧ 3 ≤ 𝑁) → 2
≤ 𝑁)) |
31 | 27, 30 | mpani 696 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℤ → (3 ≤
𝑁 → 2 ≤ 𝑁)) |
32 | 31 | imp 410 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℤ ∧ 3 ≤
𝑁) → 2 ≤ 𝑁) |
33 | 32 | 3adant1 1132 |
. . . . . . . . . . . . . . . 16
⊢ ((3
∈ ℤ ∧ 𝑁
∈ ℤ ∧ 3 ≤ 𝑁) → 2 ≤ 𝑁) |
34 | 28 | 3ad2ant2 1136 |
. . . . . . . . . . . . . . . . 17
⊢ ((3
∈ ℤ ∧ 𝑁
∈ ℤ ∧ 3 ≤ 𝑁) → 𝑁 ∈ ℝ) |
35 | | lesub1 11356 |
. . . . . . . . . . . . . . . . . 18
⊢ ((2
∈ ℝ ∧ 𝑁
∈ ℝ ∧ 1 ∈ ℝ) → (2 ≤ 𝑁 ↔ (2 − 1) ≤ (𝑁 − 1))) |
36 | 24, 5, 35 | mp3an13 1454 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℝ → (2 ≤
𝑁 ↔ (2 − 1) ≤
(𝑁 −
1))) |
37 | 34, 36 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((3
∈ ℤ ∧ 𝑁
∈ ℤ ∧ 3 ≤ 𝑁) → (2 ≤ 𝑁 ↔ (2 − 1) ≤ (𝑁 − 1))) |
38 | 33, 37 | mpbid 235 |
. . . . . . . . . . . . . . 15
⊢ ((3
∈ ℤ ∧ 𝑁
∈ ℤ ∧ 3 ≤ 𝑁) → (2 − 1) ≤ (𝑁 − 1)) |
39 | 23, 38 | eqbrtrrid 5106 |
. . . . . . . . . . . . . 14
⊢ ((3
∈ ℤ ∧ 𝑁
∈ ℤ ∧ 3 ≤ 𝑁) → 1 ≤ (𝑁 − 1)) |
40 | 20, 22, 39 | 3jca 1130 |
. . . . . . . . . . . . 13
⊢ ((3
∈ ℤ ∧ 𝑁
∈ ℤ ∧ 3 ≤ 𝑁) → (1 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ ∧
1 ≤ (𝑁 −
1))) |
41 | | eluz2 12474 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈
(ℤ≥‘3) ↔ (3 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 3 ≤
𝑁)) |
42 | | eluz2 12474 |
. . . . . . . . . . . . 13
⊢ ((𝑁 − 1) ∈
(ℤ≥‘1) ↔ (1 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ ∧
1 ≤ (𝑁 −
1))) |
43 | 40, 41, 42 | 3imtr4i 295 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − 1) ∈
(ℤ≥‘1)) |
44 | | eluzfz1 13149 |
. . . . . . . . . . . 12
⊢ ((𝑁 − 1) ∈
(ℤ≥‘1) → 1 ∈ (1...(𝑁 − 1))) |
45 | 43, 44 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘3) → 1 ∈ (1...(𝑁 − 1))) |
46 | 45 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑖 ∈ (2...(𝑁 − 1))) → 1 ∈ (1...(𝑁 − 1))) |
47 | | eqeq1 2743 |
. . . . . . . . . . . 12
⊢ (𝑘 = 1 → (𝑘 = 1 ↔ 1 = 1)) |
48 | | oveq1 7242 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 1 → (𝑘 + 1) = (1 + 1)) |
49 | 48 | opeq1d 4807 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 1 → 〈(𝑘 + 1), 1〉 = 〈(1 + 1),
1〉) |
50 | 49 | sneqd 4570 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 1 → {〈(𝑘 + 1), 1〉} = {〈(1 +
1), 1〉}) |
51 | 48 | sneqd 4570 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 1 → {(𝑘 + 1)} = {(1 + 1)}) |
52 | 51 | difeq2d 4054 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 1 → ((1...𝑁) ∖ {(𝑘 + 1)}) = ((1...𝑁) ∖ {(1 + 1)})) |
53 | 52 | xpeq1d 5598 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 1 → (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}) = (((1...𝑁) ∖ {(1 + 1)}) ×
{0})) |
54 | 50, 53 | uneq12d 4095 |
. . . . . . . . . . . 12
⊢ (𝑘 = 1 → ({〈(𝑘 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑘 + 1)}) × {0})) =
({〈(1 + 1), 1〉} ∪ (((1...𝑁) ∖ {(1 + 1)}) ×
{0}))) |
55 | 47, 54 | ifbieq2d 4482 |
. . . . . . . . . . 11
⊢ (𝑘 = 1 → if(𝑘 = 1, ({〈3, -1〉} ∪
(((1...𝑁) ∖ {3})
× {0})), ({〈(𝑘 +
1), 1〉} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))) = if(1 = 1, ({〈3,
-1〉} ∪ (((1...𝑁)
∖ {3}) × {0})), ({〈(1 + 1), 1〉} ∪ (((1...𝑁) ∖ {(1 + 1)}) ×
{0})))) |
56 | | snex 5341 |
. . . . . . . . . . . . 13
⊢ {〈3,
-1〉} ∈ V |
57 | | ovex 7268 |
. . . . . . . . . . . . . . 15
⊢
(1...𝑁) ∈
V |
58 | 57 | difexi 5238 |
. . . . . . . . . . . . . 14
⊢
((1...𝑁) ∖
{3}) ∈ V |
59 | | snex 5341 |
. . . . . . . . . . . . . 14
⊢ {0}
∈ V |
60 | 58, 59 | xpex 7560 |
. . . . . . . . . . . . 13
⊢
(((1...𝑁) ∖
{3}) × {0}) ∈ V |
61 | 56, 60 | unex 7553 |
. . . . . . . . . . . 12
⊢
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})) ∈
V |
62 | | snex 5341 |
. . . . . . . . . . . . 13
⊢ {〈(1
+ 1), 1〉} ∈ V |
63 | 57 | difexi 5238 |
. . . . . . . . . . . . . 14
⊢
((1...𝑁) ∖ {(1
+ 1)}) ∈ V |
64 | 63, 59 | xpex 7560 |
. . . . . . . . . . . . 13
⊢
(((1...𝑁) ∖
{(1 + 1)}) × {0}) ∈ V |
65 | 62, 64 | unex 7553 |
. . . . . . . . . . . 12
⊢
({〈(1 + 1), 1〉} ∪ (((1...𝑁) ∖ {(1 + 1)}) × {0})) ∈
V |
66 | 61, 65 | ifex 4506 |
. . . . . . . . . . 11
⊢ if(1 = 1,
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})), ({〈(1 +
1), 1〉} ∪ (((1...𝑁) ∖ {(1 + 1)}) × {0}))) ∈
V |
67 | 55, 10, 66 | fvmpt 6840 |
. . . . . . . . . 10
⊢ (1 ∈
(1...(𝑁 − 1)) →
((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪
(((1...𝑁) ∖ {3})
× {0})), ({〈(𝑘 +
1), 1〉} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1) = if(1 = 1,
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})), ({〈(1 +
1), 1〉} ∪ (((1...𝑁) ∖ {(1 + 1)}) ×
{0})))) |
68 | 46, 67 | syl 17 |
. . . . . . . . 9
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑖 ∈ (2...(𝑁 − 1))) → ((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1) = if(1 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(1 + 1), 1〉} ∪ (((1...𝑁) ∖ {(1 + 1)}) ×
{0})))) |
69 | | eqid 2739 |
. . . . . . . . . 10
⊢ 1 =
1 |
70 | 69 | iftruei 4463 |
. . . . . . . . 9
⊢ if(1 = 1,
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})), ({〈(1 +
1), 1〉} ∪ (((1...𝑁) ∖ {(1 + 1)}) × {0}))) =
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) ×
{0})) |
71 | 68, 70 | eqtrdi 2796 |
. . . . . . . 8
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑖 ∈ (2...(𝑁 − 1))) → ((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1) = ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) ×
{0}))) |
72 | 71 | opeq1d 4807 |
. . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑖 ∈ (2...(𝑁 − 1))) → 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), ({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 =
〈({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})), ({〈1,
0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉) |
73 | | 2eluzge1 12520 |
. . . . . . . . . . . . 13
⊢ 2 ∈
(ℤ≥‘1) |
74 | | fzss1 13181 |
. . . . . . . . . . . . 13
⊢ (2 ∈
(ℤ≥‘1) → (2...(𝑁 − 1)) ⊆ (1...(𝑁 − 1))) |
75 | 73, 74 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
(2...(𝑁 − 1))
⊆ (1...(𝑁 −
1)) |
76 | 75 | sseli 3913 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ (2...(𝑁 − 1)) → 𝑖 ∈ (1...(𝑁 − 1))) |
77 | 76 | adantl 485 |
. . . . . . . . . 10
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑖 ∈ (2...(𝑁 − 1))) → 𝑖 ∈ (1...(𝑁 − 1))) |
78 | | eqeq1 2743 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑖 → (𝑘 = 1 ↔ 𝑖 = 1)) |
79 | | oveq1 7242 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑖 → (𝑘 + 1) = (𝑖 + 1)) |
80 | 79 | opeq1d 4807 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑖 → 〈(𝑘 + 1), 1〉 = 〈(𝑖 + 1), 1〉) |
81 | 80 | sneqd 4570 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑖 → {〈(𝑘 + 1), 1〉} = {〈(𝑖 + 1), 1〉}) |
82 | 79 | sneqd 4570 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑖 → {(𝑘 + 1)} = {(𝑖 + 1)}) |
83 | 82 | difeq2d 4054 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑖 → ((1...𝑁) ∖ {(𝑘 + 1)}) = ((1...𝑁) ∖ {(𝑖 + 1)})) |
84 | 83 | xpeq1d 5598 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑖 → (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}) = (((1...𝑁) ∖ {(𝑖 + 1)}) × {0})) |
85 | 81, 84 | uneq12d 4095 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑖 → ({〈(𝑘 + 1), 1〉} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})) = ({〈(𝑖 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑖 + 1)}) ×
{0}))) |
86 | 78, 85 | ifbieq2d 4482 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑖 → if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) × {0}))) =
if(𝑖 = 1, ({〈3,
-1〉} ∪ (((1...𝑁)
∖ {3}) × {0})), ({〈(𝑖 + 1), 1〉} ∪ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0})))) |
87 | | snex 5341 |
. . . . . . . . . . . . 13
⊢
{〈(𝑖 + 1),
1〉} ∈ V |
88 | 57 | difexi 5238 |
. . . . . . . . . . . . . 14
⊢
((1...𝑁) ∖
{(𝑖 + 1)}) ∈
V |
89 | 88, 59 | xpex 7560 |
. . . . . . . . . . . . 13
⊢
(((1...𝑁) ∖
{(𝑖 + 1)}) × {0})
∈ V |
90 | 87, 89 | unex 7553 |
. . . . . . . . . . . 12
⊢
({〈(𝑖 + 1),
1〉} ∪ (((1...𝑁)
∖ {(𝑖 + 1)}) ×
{0})) ∈ V |
91 | 61, 90 | ifex 4506 |
. . . . . . . . . . 11
⊢ if(𝑖 = 1, ({〈3, -1〉} ∪
(((1...𝑁) ∖ {3})
× {0})), ({〈(𝑖 +
1), 1〉} ∪ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0}))) ∈
V |
92 | 86, 10, 91 | fvmpt 6840 |
. . . . . . . . . 10
⊢ (𝑖 ∈ (1...(𝑁 − 1)) → ((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖) = if(𝑖 = 1, ({〈3, -1〉} ∪
(((1...𝑁) ∖ {3})
× {0})), ({〈(𝑖 +
1), 1〉} ∪ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0})))) |
93 | 77, 92 | syl 17 |
. . . . . . . . 9
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑖 ∈ (2...(𝑁 − 1))) → ((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖) = if(𝑖 = 1, ({〈3, -1〉} ∪
(((1...𝑁) ∖ {3})
× {0})), ({〈(𝑖 +
1), 1〉} ∪ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0})))) |
94 | | 1lt2 12031 |
. . . . . . . . . . . . . . . 16
⊢ 1 <
2 |
95 | 5, 24 | ltnlei 10983 |
. . . . . . . . . . . . . . . 16
⊢ (1 < 2
↔ ¬ 2 ≤ 1) |
96 | 94, 95 | mpbi 233 |
. . . . . . . . . . . . . . 15
⊢ ¬ 2
≤ 1 |
97 | 96 | intnanr 491 |
. . . . . . . . . . . . . 14
⊢ ¬ (2
≤ 1 ∧ 1 ≤ (𝑁
− 1)) |
98 | | 1z 12237 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℤ |
99 | | 2z 12239 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℤ |
100 | | eluzelz 12478 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈ ℤ) |
101 | 100, 21 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − 1) ∈ ℤ) |
102 | | elfz 13131 |
. . . . . . . . . . . . . . 15
⊢ ((1
∈ ℤ ∧ 2 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) → (1 ∈
(2...(𝑁 − 1)) ↔
(2 ≤ 1 ∧ 1 ≤ (𝑁
− 1)))) |
103 | 98, 99, 101, 102 | mp3an12i 1467 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘3) → (1 ∈ (2...(𝑁 − 1)) ↔ (2 ≤ 1 ∧ 1 ≤
(𝑁 −
1)))) |
104 | 97, 103 | mtbiri 330 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈
(ℤ≥‘3) → ¬ 1 ∈ (2...(𝑁 − 1))) |
105 | | eleq1 2827 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 1 → (𝑖 ∈ (2...(𝑁 − 1)) ↔ 1 ∈ (2...(𝑁 − 1)))) |
106 | 105 | notbid 321 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 1 → (¬ 𝑖 ∈ (2...(𝑁 − 1)) ↔ ¬ 1 ∈
(2...(𝑁 −
1)))) |
107 | 104, 106 | syl5ibrcom 250 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑖 = 1 → ¬ 𝑖 ∈ (2...(𝑁 − 1)))) |
108 | 107 | con2d 136 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑖 ∈ (2...(𝑁 − 1)) → ¬ 𝑖 = 1)) |
109 | 108 | imp 410 |
. . . . . . . . . 10
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑖 ∈ (2...(𝑁 − 1))) → ¬ 𝑖 = 1) |
110 | 109 | iffalsed 4467 |
. . . . . . . . 9
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑖 ∈ (2...(𝑁 − 1))) → if(𝑖 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑖 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑖 + 1)}) × {0}))) =
({〈(𝑖 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑖 + 1)}) ×
{0}))) |
111 | 93, 110 | eqtrd 2779 |
. . . . . . . 8
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑖 ∈ (2...(𝑁 − 1))) → ((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖) =
({〈(𝑖 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑖 + 1)}) ×
{0}))) |
112 | 111 | opeq1d 4807 |
. . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑖 ∈ (2...(𝑁 − 1))) → 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖),
({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 = 〈({〈(𝑖 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑖 + 1)}) × {0})),
({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉) |
113 | 72, 112 | breq12d 5083 |
. . . . . 6
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑖 ∈ (2...(𝑁 − 1))) → (〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), ({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) ×
{0}))〉Cgr〈((𝑘
∈ (1...(𝑁 − 1))
↦ if(𝑘 = 1,
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})), ({〈(𝑘 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑘 + 1)}) ×
{0}))))‘𝑖),
({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 ↔
〈({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})), ({〈1,
0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉Cgr〈({〈(𝑖 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑖 + 1)}) × {0})),
({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉)) |
114 | 71 | opeq1d 4807 |
. . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑖 ∈ (2...(𝑁 − 1))) → 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), ({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 =
〈({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})), ({〈1,
1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉) |
115 | 111 | opeq1d 4807 |
. . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑖 ∈ (2...(𝑁 − 1))) → 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖),
({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 = 〈({〈(𝑖 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑖 + 1)}) × {0})),
({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉) |
116 | 114, 115 | breq12d 5083 |
. . . . . 6
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑖 ∈ (2...(𝑁 − 1))) → (〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), ({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) ×
{0}))〉Cgr〈((𝑘
∈ (1...(𝑁 − 1))
↦ if(𝑘 = 1,
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})), ({〈(𝑘 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑘 + 1)}) ×
{0}))))‘𝑖),
({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 ↔
〈({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})), ({〈1,
1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉Cgr〈({〈(𝑖 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑖 + 1)}) × {0})),
({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉)) |
117 | 45, 67 | syl 17 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘3) → ((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1) = if(1 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(1 + 1), 1〉} ∪ (((1...𝑁) ∖ {(1 + 1)}) ×
{0})))) |
118 | 117, 70 | eqtrdi 2796 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘3) → ((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1) = ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) ×
{0}))) |
119 | 118 | opeq1d 4807 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘3) → 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), ({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))〉 =
〈({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})), ({〈1,
0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))〉) |
120 | 119 | adantr 484 |
. . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑖 ∈ (2...(𝑁 − 1))) → 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), ({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))〉 =
〈({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})), ({〈1,
0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))〉) |
121 | 111 | opeq1d 4807 |
. . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑖 ∈ (2...(𝑁 − 1))) → 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖),
({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))〉 = 〈({〈(𝑖 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑖 + 1)}) × {0})),
({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))〉) |
122 | 120, 121 | breq12d 5083 |
. . . . . 6
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑖 ∈ (2...(𝑁 − 1))) → (〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), ({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) ×
{0}))〉Cgr〈((𝑘
∈ (1...(𝑁 − 1))
↦ if(𝑘 = 1,
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})), ({〈(𝑘 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑘 + 1)}) ×
{0}))))‘𝑖),
({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))〉 ↔
〈({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})), ({〈1,
0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))〉Cgr〈({〈(𝑖 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑖 + 1)}) × {0})),
({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))〉)) |
123 | 113, 116,
122 | 3anbi123d 1438 |
. . . . 5
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑖 ∈ (2...(𝑁 − 1))) → ((〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), ({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) ×
{0}))〉Cgr〈((𝑘
∈ (1...(𝑁 − 1))
↦ if(𝑘 = 1,
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})), ({〈(𝑘 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑘 + 1)}) ×
{0}))))‘𝑖),
({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 ∧ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), ({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) ×
{0}))〉Cgr〈((𝑘
∈ (1...(𝑁 − 1))
↦ if(𝑘 = 1,
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})), ({〈(𝑘 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑘 + 1)}) ×
{0}))))‘𝑖),
({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 ∧ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), ({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) ×
{0}))〉Cgr〈((𝑘
∈ (1...(𝑁 − 1))
↦ if(𝑘 = 1,
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})), ({〈(𝑘 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑘 + 1)}) ×
{0}))))‘𝑖),
({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))〉) ↔
(〈({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})), ({〈1,
0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉Cgr〈({〈(𝑖 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑖 + 1)}) × {0})),
({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 ∧ 〈({〈3,
-1〉} ∪ (((1...𝑁)
∖ {3}) × {0})), ({〈1, 1〉, 〈2, 0〉} ∪
((3...𝑁) ×
{0}))〉Cgr〈({〈(𝑖 + 1), 1〉} ∪ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0})), ({〈1, 1〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 ∧ 〈({〈3,
-1〉} ∪ (((1...𝑁)
∖ {3}) × {0})), ({〈1, 0〉, 〈2, 1〉} ∪
((3...𝑁) ×
{0}))〉Cgr〈({〈(𝑖 + 1), 1〉} ∪ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0})), ({〈1, 0〉,
〈2, 1〉} ∪ ((3...𝑁) × {0}))〉))) |
124 | 15, 17, 19, 123 | mpbir3and 1344 |
. . . 4
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑖 ∈ (2...(𝑁 − 1))) → (〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), ({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) ×
{0}))〉Cgr〈((𝑘
∈ (1...(𝑁 − 1))
↦ if(𝑘 = 1,
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})), ({〈(𝑘 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑘 + 1)}) ×
{0}))))‘𝑖),
({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 ∧ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), ({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) ×
{0}))〉Cgr〈((𝑘
∈ (1...(𝑁 − 1))
↦ if(𝑘 = 1,
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})), ({〈(𝑘 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑘 + 1)}) ×
{0}))))‘𝑖),
({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 ∧ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), ({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) ×
{0}))〉Cgr〈((𝑘
∈ (1...(𝑁 − 1))
↦ if(𝑘 = 1,
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})), ({〈(𝑘 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑘 + 1)}) ×
{0}))))‘𝑖),
({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))〉)) |
125 | 124 | ralrimiva 3108 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘3) → ∀𝑖 ∈ (2...(𝑁 − 1))(〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), ({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) ×
{0}))〉Cgr〈((𝑘
∈ (1...(𝑁 − 1))
↦ if(𝑘 = 1,
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})), ({〈(𝑘 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑘 + 1)}) ×
{0}))))‘𝑖),
({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 ∧ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), ({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) ×
{0}))〉Cgr〈((𝑘
∈ (1...(𝑁 − 1))
↦ if(𝑘 = 1,
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})), ({〈(𝑘 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑘 + 1)}) ×
{0}))))‘𝑖),
({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 ∧ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), ({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) ×
{0}))〉Cgr〈((𝑘
∈ (1...(𝑁 − 1))
↦ if(𝑘 = 1,
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})), ({〈(𝑘 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑘 + 1)}) ×
{0}))))‘𝑖),
({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))〉)) |
126 | 14, 16, 18 | axlowdimlem6 27070 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘2) → ¬ (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0})) Btwn 〈({〈1, 1〉, 〈2, 0〉} ∪
((3...𝑁) × {0})),
({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))〉 ∨ ({〈1,
1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})) Btwn 〈({〈1,
0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0})), ({〈1, 0〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 ∨ ({〈1,
0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0})) Btwn 〈({〈1,
0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})), ({〈1, 1〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))〉)) |
127 | 1, 126 | syl 17 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘3) → ¬ (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0})) Btwn 〈({〈1, 1〉, 〈2, 0〉} ∪
((3...𝑁) × {0})),
({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))〉 ∨ ({〈1,
1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})) Btwn 〈({〈1,
0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0})), ({〈1, 0〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 ∨ ({〈1,
0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0})) Btwn 〈({〈1,
0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})), ({〈1, 1〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))〉)) |
128 | | opeq2 4802 |
. . . . . . . 8
⊢ (𝑥 = ({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0})) → 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑥〉 =
〈((𝑘 ∈
(1...(𝑁 − 1)) ↦
if(𝑘 = 1, ({〈3,
-1〉} ∪ (((1...𝑁)
∖ {3}) × {0})), ({〈(𝑘 + 1), 1〉} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), ({〈1,
0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉) |
129 | | opeq2 4802 |
. . . . . . . 8
⊢ (𝑥 = ({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0})) → 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑥〉 = 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖),
({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉) |
130 | 128, 129 | breq12d 5083 |
. . . . . . 7
⊢ (𝑥 = ({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0})) → (〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑥〉Cgr〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑥〉 ↔ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), ({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) ×
{0}))〉Cgr〈((𝑘
∈ (1...(𝑁 − 1))
↦ if(𝑘 = 1,
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})), ({〈(𝑘 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑘 + 1)}) ×
{0}))))‘𝑖),
({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉)) |
131 | 130 | 3anbi1d 1442 |
. . . . . 6
⊢ (𝑥 = ({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0})) → ((〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑥〉Cgr〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑥〉 ∧ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑦〉Cgr〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑦〉 ∧ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑧〉Cgr〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑧〉) ↔ (〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), ({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) ×
{0}))〉Cgr〈((𝑘
∈ (1...(𝑁 − 1))
↦ if(𝑘 = 1,
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})), ({〈(𝑘 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑘 + 1)}) ×
{0}))))‘𝑖),
({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 ∧ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑦〉Cgr〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑦〉 ∧ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑧〉Cgr〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑧〉))) |
132 | 131 | ralbidv 3121 |
. . . . 5
⊢ (𝑥 = ({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0})) → (∀𝑖 ∈ (2...(𝑁 − 1))(〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑥〉Cgr〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑥〉 ∧ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑦〉Cgr〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑦〉 ∧ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑧〉Cgr〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑧〉) ↔ ∀𝑖 ∈ (2...(𝑁 − 1))(〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), ({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) ×
{0}))〉Cgr〈((𝑘
∈ (1...(𝑁 − 1))
↦ if(𝑘 = 1,
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})), ({〈(𝑘 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑘 + 1)}) ×
{0}))))‘𝑖),
({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 ∧ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑦〉Cgr〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑦〉 ∧ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑧〉Cgr〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑧〉))) |
133 | | breq1 5073 |
. . . . . . 7
⊢ (𝑥 = ({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0})) → (𝑥
Btwn 〈𝑦, 𝑧〉 ↔ ({〈1,
0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})) Btwn 〈𝑦, 𝑧〉)) |
134 | | opeq2 4802 |
. . . . . . . 8
⊢ (𝑥 = ({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0})) → 〈𝑧, 𝑥〉 = 〈𝑧, ({〈1, 0〉, 〈2, 0〉} ∪
((3...𝑁) ×
{0}))〉) |
135 | 134 | breq2d 5082 |
. . . . . . 7
⊢ (𝑥 = ({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0})) → (𝑦
Btwn 〈𝑧, 𝑥〉 ↔ 𝑦 Btwn 〈𝑧, ({〈1, 0〉, 〈2, 0〉} ∪
((3...𝑁) ×
{0}))〉)) |
136 | | opeq1 4801 |
. . . . . . . 8
⊢ (𝑥 = ({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0})) → 〈𝑥, 𝑦〉 = 〈({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0})), 𝑦〉) |
137 | 136 | breq2d 5082 |
. . . . . . 7
⊢ (𝑥 = ({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0})) → (𝑧
Btwn 〈𝑥, 𝑦〉 ↔ 𝑧 Btwn 〈({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0})), 𝑦〉)) |
138 | 133, 135,
137 | 3orbi123d 1437 |
. . . . . 6
⊢ (𝑥 = ({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0})) → ((𝑥
Btwn 〈𝑦, 𝑧〉 ∨ 𝑦 Btwn 〈𝑧, 𝑥〉 ∨ 𝑧 Btwn 〈𝑥, 𝑦〉) ↔ (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0})) Btwn 〈𝑦,
𝑧〉 ∨ 𝑦 Btwn 〈𝑧, ({〈1, 0〉, 〈2, 0〉} ∪
((3...𝑁) ×
{0}))〉 ∨ 𝑧 Btwn
〈({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})), 𝑦〉))) |
139 | 138 | notbid 321 |
. . . . 5
⊢ (𝑥 = ({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0})) → (¬ (𝑥 Btwn 〈𝑦, 𝑧〉 ∨ 𝑦 Btwn 〈𝑧, 𝑥〉 ∨ 𝑧 Btwn 〈𝑥, 𝑦〉) ↔ ¬ (({〈1, 0〉,
〈2, 0〉} ∪ ((3...𝑁) × {0})) Btwn 〈𝑦, 𝑧〉 ∨ 𝑦 Btwn 〈𝑧, ({〈1, 0〉, 〈2, 0〉} ∪
((3...𝑁) ×
{0}))〉 ∨ 𝑧 Btwn
〈({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})), 𝑦〉))) |
140 | 132, 139 | 3anbi23d 1441 |
. . . 4
⊢ (𝑥 = ({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0})) → (((𝑘
∈ (1...(𝑁 − 1))
↦ if(𝑘 = 1,
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})), ({〈(𝑘 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑘 + 1)}) ×
{0})))):(1...(𝑁 −
1))–1-1→(𝔼‘𝑁) ∧ ∀𝑖 ∈ (2...(𝑁 − 1))(〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑥〉Cgr〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑥〉 ∧ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑦〉Cgr〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑦〉 ∧ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑧〉Cgr〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑧〉) ∧ ¬ (𝑥 Btwn 〈𝑦, 𝑧〉 ∨ 𝑦 Btwn 〈𝑧, 𝑥〉 ∨ 𝑧 Btwn 〈𝑥, 𝑦〉)) ↔ ((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0})))):(1...(𝑁 −
1))–1-1→(𝔼‘𝑁) ∧ ∀𝑖 ∈ (2...(𝑁 − 1))(〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), ({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) ×
{0}))〉Cgr〈((𝑘
∈ (1...(𝑁 − 1))
↦ if(𝑘 = 1,
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})), ({〈(𝑘 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑘 + 1)}) ×
{0}))))‘𝑖),
({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 ∧ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑦〉Cgr〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑦〉 ∧ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑧〉Cgr〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑧〉) ∧ ¬ (({〈1,
0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})) Btwn 〈𝑦, 𝑧〉 ∨ 𝑦 Btwn 〈𝑧, ({〈1, 0〉, 〈2, 0〉} ∪
((3...𝑁) ×
{0}))〉 ∨ 𝑧 Btwn
〈({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})), 𝑦〉)))) |
141 | | opeq2 4802 |
. . . . . . . 8
⊢ (𝑦 = ({〈1, 1〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0})) → 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑦〉 =
〈((𝑘 ∈
(1...(𝑁 − 1)) ↦
if(𝑘 = 1, ({〈3,
-1〉} ∪ (((1...𝑁)
∖ {3}) × {0})), ({〈(𝑘 + 1), 1〉} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), ({〈1,
1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉) |
142 | | opeq2 4802 |
. . . . . . . 8
⊢ (𝑦 = ({〈1, 1〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0})) → 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑦〉 = 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖),
({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉) |
143 | 141, 142 | breq12d 5083 |
. . . . . . 7
⊢ (𝑦 = ({〈1, 1〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0})) → (〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑦〉Cgr〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑦〉 ↔ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), ({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) ×
{0}))〉Cgr〈((𝑘
∈ (1...(𝑁 − 1))
↦ if(𝑘 = 1,
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})), ({〈(𝑘 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑘 + 1)}) ×
{0}))))‘𝑖),
({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉)) |
144 | 143 | 3anbi2d 1443 |
. . . . . 6
⊢ (𝑦 = ({〈1, 1〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0})) → ((〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), ({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) ×
{0}))〉Cgr〈((𝑘
∈ (1...(𝑁 − 1))
↦ if(𝑘 = 1,
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})), ({〈(𝑘 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑘 + 1)}) ×
{0}))))‘𝑖),
({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 ∧ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑦〉Cgr〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑦〉 ∧ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑧〉Cgr〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑧〉) ↔ (〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), ({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) ×
{0}))〉Cgr〈((𝑘
∈ (1...(𝑁 − 1))
↦ if(𝑘 = 1,
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})), ({〈(𝑘 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑘 + 1)}) ×
{0}))))‘𝑖),
({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 ∧ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), ({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) ×
{0}))〉Cgr〈((𝑘
∈ (1...(𝑁 − 1))
↦ if(𝑘 = 1,
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})), ({〈(𝑘 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑘 + 1)}) ×
{0}))))‘𝑖),
({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 ∧ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑧〉Cgr〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑧〉))) |
145 | 144 | ralbidv 3121 |
. . . . 5
⊢ (𝑦 = ({〈1, 1〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0})) → (∀𝑖 ∈ (2...(𝑁 − 1))(〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), ({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) ×
{0}))〉Cgr〈((𝑘
∈ (1...(𝑁 − 1))
↦ if(𝑘 = 1,
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})), ({〈(𝑘 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑘 + 1)}) ×
{0}))))‘𝑖),
({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 ∧ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑦〉Cgr〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑦〉 ∧ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑧〉Cgr〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑧〉) ↔ ∀𝑖 ∈ (2...(𝑁 − 1))(〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), ({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) ×
{0}))〉Cgr〈((𝑘
∈ (1...(𝑁 − 1))
↦ if(𝑘 = 1,
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})), ({〈(𝑘 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑘 + 1)}) ×
{0}))))‘𝑖),
({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 ∧ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), ({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) ×
{0}))〉Cgr〈((𝑘
∈ (1...(𝑁 − 1))
↦ if(𝑘 = 1,
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})), ({〈(𝑘 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑘 + 1)}) ×
{0}))))‘𝑖),
({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 ∧ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑧〉Cgr〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑧〉))) |
146 | | opeq1 4801 |
. . . . . . . 8
⊢ (𝑦 = ({〈1, 1〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0})) → 〈𝑦, 𝑧〉 = 〈({〈1, 1〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0})), 𝑧〉) |
147 | 146 | breq2d 5082 |
. . . . . . 7
⊢ (𝑦 = ({〈1, 1〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0})) → (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})) Btwn 〈𝑦, 𝑧〉 ↔ ({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0})) Btwn 〈({〈1, 1〉, 〈2, 0〉} ∪
((3...𝑁) × {0})),
𝑧〉)) |
148 | | breq1 5073 |
. . . . . . 7
⊢ (𝑦 = ({〈1, 1〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0})) → (𝑦
Btwn 〈𝑧, ({〈1,
0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 ↔ ({〈1,
1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})) Btwn 〈𝑧, ({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))〉)) |
149 | | opeq2 4802 |
. . . . . . . 8
⊢ (𝑦 = ({〈1, 1〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0})) → 〈({〈1, 0〉, 〈2, 0〉} ∪
((3...𝑁) × {0})),
𝑦〉 = 〈({〈1,
0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})), ({〈1, 1〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))〉) |
150 | 149 | breq2d 5082 |
. . . . . . 7
⊢ (𝑦 = ({〈1, 1〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0})) → (𝑧
Btwn 〈({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})), 𝑦〉 ↔ 𝑧 Btwn 〈({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0})), ({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) ×
{0}))〉)) |
151 | 147, 148,
150 | 3orbi123d 1437 |
. . . . . 6
⊢ (𝑦 = ({〈1, 1〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0})) → ((({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})) Btwn 〈𝑦, 𝑧〉 ∨ 𝑦 Btwn 〈𝑧, ({〈1, 0〉, 〈2, 0〉} ∪
((3...𝑁) ×
{0}))〉 ∨ 𝑧 Btwn
〈({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})), 𝑦〉) ↔ (({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0})) Btwn 〈({〈1, 1〉, 〈2, 0〉} ∪
((3...𝑁) × {0})),
𝑧〉 ∨ ({〈1,
1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})) Btwn 〈𝑧, ({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))〉 ∨ 𝑧
Btwn 〈({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})), ({〈1, 1〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))〉))) |
152 | 151 | notbid 321 |
. . . . 5
⊢ (𝑦 = ({〈1, 1〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0})) → (¬ (({〈1, 0〉, 〈2, 0〉} ∪
((3...𝑁) × {0})) Btwn
〈𝑦, 𝑧〉 ∨ 𝑦 Btwn 〈𝑧, ({〈1, 0〉, 〈2, 0〉} ∪
((3...𝑁) ×
{0}))〉 ∨ 𝑧 Btwn
〈({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})), 𝑦〉) ↔ ¬ (({〈1, 0〉,
〈2, 0〉} ∪ ((3...𝑁) × {0})) Btwn 〈({〈1,
1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})), 𝑧〉 ∨ ({〈1, 1〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0})) Btwn 〈𝑧,
({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 ∨ 𝑧 Btwn 〈({〈1, 0〉,
〈2, 0〉} ∪ ((3...𝑁) × {0})), ({〈1, 1〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))〉))) |
153 | 145, 152 | 3anbi23d 1441 |
. . . 4
⊢ (𝑦 = ({〈1, 1〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0})) → (((𝑘
∈ (1...(𝑁 − 1))
↦ if(𝑘 = 1,
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})), ({〈(𝑘 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑘 + 1)}) ×
{0})))):(1...(𝑁 −
1))–1-1→(𝔼‘𝑁) ∧ ∀𝑖 ∈ (2...(𝑁 − 1))(〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), ({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) ×
{0}))〉Cgr〈((𝑘
∈ (1...(𝑁 − 1))
↦ if(𝑘 = 1,
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})), ({〈(𝑘 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑘 + 1)}) ×
{0}))))‘𝑖),
({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 ∧ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑦〉Cgr〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑦〉 ∧ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑧〉Cgr〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑧〉) ∧ ¬ (({〈1,
0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})) Btwn 〈𝑦, 𝑧〉 ∨ 𝑦 Btwn 〈𝑧, ({〈1, 0〉, 〈2, 0〉} ∪
((3...𝑁) ×
{0}))〉 ∨ 𝑧 Btwn
〈({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})), 𝑦〉)) ↔ ((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0})))):(1...(𝑁 −
1))–1-1→(𝔼‘𝑁) ∧ ∀𝑖 ∈ (2...(𝑁 − 1))(〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), ({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) ×
{0}))〉Cgr〈((𝑘
∈ (1...(𝑁 − 1))
↦ if(𝑘 = 1,
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})), ({〈(𝑘 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑘 + 1)}) ×
{0}))))‘𝑖),
({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 ∧ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), ({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) ×
{0}))〉Cgr〈((𝑘
∈ (1...(𝑁 − 1))
↦ if(𝑘 = 1,
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})), ({〈(𝑘 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑘 + 1)}) ×
{0}))))‘𝑖),
({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 ∧ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑧〉Cgr〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑧〉) ∧ ¬ (({〈1,
0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})) Btwn 〈({〈1,
1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})), 𝑧〉 ∨ ({〈1, 1〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0})) Btwn 〈𝑧,
({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 ∨ 𝑧 Btwn 〈({〈1, 0〉,
〈2, 0〉} ∪ ((3...𝑁) × {0})), ({〈1, 1〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))〉)))) |
154 | | opeq2 4802 |
. . . . . . . 8
⊢ (𝑧 = ({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0})) → 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑧〉 =
〈((𝑘 ∈
(1...(𝑁 − 1)) ↦
if(𝑘 = 1, ({〈3,
-1〉} ∪ (((1...𝑁)
∖ {3}) × {0})), ({〈(𝑘 + 1), 1〉} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))‘1), ({〈1,
0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))〉) |
155 | | opeq2 4802 |
. . . . . . . 8
⊢ (𝑧 = ({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0})) → 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑧〉 = 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖),
({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))〉) |
156 | 154, 155 | breq12d 5083 |
. . . . . . 7
⊢ (𝑧 = ({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0})) → (〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑧〉Cgr〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑧〉 ↔ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), ({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) ×
{0}))〉Cgr〈((𝑘
∈ (1...(𝑁 − 1))
↦ if(𝑘 = 1,
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})), ({〈(𝑘 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑘 + 1)}) ×
{0}))))‘𝑖),
({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))〉)) |
157 | 156 | 3anbi3d 1444 |
. . . . . 6
⊢ (𝑧 = ({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0})) → ((〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), ({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) ×
{0}))〉Cgr〈((𝑘
∈ (1...(𝑁 − 1))
↦ if(𝑘 = 1,
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})), ({〈(𝑘 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑘 + 1)}) ×
{0}))))‘𝑖),
({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 ∧ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), ({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) ×
{0}))〉Cgr〈((𝑘
∈ (1...(𝑁 − 1))
↦ if(𝑘 = 1,
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})), ({〈(𝑘 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑘 + 1)}) ×
{0}))))‘𝑖),
({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 ∧ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑧〉Cgr〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑧〉) ↔ (〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), ({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) ×
{0}))〉Cgr〈((𝑘
∈ (1...(𝑁 − 1))
↦ if(𝑘 = 1,
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})), ({〈(𝑘 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑘 + 1)}) ×
{0}))))‘𝑖),
({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 ∧ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), ({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) ×
{0}))〉Cgr〈((𝑘
∈ (1...(𝑁 − 1))
↦ if(𝑘 = 1,
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})), ({〈(𝑘 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑘 + 1)}) ×
{0}))))‘𝑖),
({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 ∧ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), ({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) ×
{0}))〉Cgr〈((𝑘
∈ (1...(𝑁 − 1))
↦ if(𝑘 = 1,
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})), ({〈(𝑘 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑘 + 1)}) ×
{0}))))‘𝑖),
({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))〉))) |
158 | 157 | ralbidv 3121 |
. . . . 5
⊢ (𝑧 = ({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0})) → (∀𝑖 ∈ (2...(𝑁 − 1))(〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), ({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) ×
{0}))〉Cgr〈((𝑘
∈ (1...(𝑁 − 1))
↦ if(𝑘 = 1,
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})), ({〈(𝑘 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑘 + 1)}) ×
{0}))))‘𝑖),
({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 ∧ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), ({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) ×
{0}))〉Cgr〈((𝑘
∈ (1...(𝑁 − 1))
↦ if(𝑘 = 1,
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})), ({〈(𝑘 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑘 + 1)}) ×
{0}))))‘𝑖),
({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 ∧ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑧〉Cgr〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑧〉) ↔ ∀𝑖 ∈ (2...(𝑁 − 1))(〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), ({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) ×
{0}))〉Cgr〈((𝑘
∈ (1...(𝑁 − 1))
↦ if(𝑘 = 1,
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})), ({〈(𝑘 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑘 + 1)}) ×
{0}))))‘𝑖),
({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 ∧ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), ({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) ×
{0}))〉Cgr〈((𝑘
∈ (1...(𝑁 − 1))
↦ if(𝑘 = 1,
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})), ({〈(𝑘 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑘 + 1)}) ×
{0}))))‘𝑖),
({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 ∧ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), ({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) ×
{0}))〉Cgr〈((𝑘
∈ (1...(𝑁 − 1))
↦ if(𝑘 = 1,
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})), ({〈(𝑘 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑘 + 1)}) ×
{0}))))‘𝑖),
({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))〉))) |
159 | | opeq2 4802 |
. . . . . . . 8
⊢ (𝑧 = ({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0})) → 〈({〈1, 1〉, 〈2, 0〉} ∪
((3...𝑁) × {0})),
𝑧〉 = 〈({〈1,
1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})), ({〈1, 0〉,
〈2, 1〉} ∪ ((3...𝑁) × {0}))〉) |
160 | 159 | breq2d 5082 |
. . . . . . 7
⊢ (𝑧 = ({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0})) → (({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})) Btwn
〈({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})), 𝑧〉 ↔ ({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0})) Btwn 〈({〈1, 1〉, 〈2, 0〉} ∪
((3...𝑁) × {0})),
({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))〉)) |
161 | | opeq1 4801 |
. . . . . . . 8
⊢ (𝑧 = ({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0})) → 〈𝑧, ({〈1, 0〉, 〈2, 0〉} ∪
((3...𝑁) ×
{0}))〉 = 〈({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0})), ({〈1,
0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉) |
162 | 161 | breq2d 5082 |
. . . . . . 7
⊢ (𝑧 = ({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0})) → (({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})) Btwn 〈𝑧, ({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0}))〉 ↔ ({〈1, 1〉, 〈2, 0〉} ∪
((3...𝑁) × {0})) Btwn
〈({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0})), ({〈1, 0〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))〉)) |
163 | | breq1 5073 |
. . . . . . 7
⊢ (𝑧 = ({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0})) → (𝑧
Btwn 〈({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})), ({〈1, 1〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 ↔ ({〈1,
0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0})) Btwn 〈({〈1,
0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})), ({〈1, 1〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))〉)) |
164 | 160, 162,
163 | 3orbi123d 1437 |
. . . . . 6
⊢ (𝑧 = ({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0})) → ((({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})) Btwn
〈({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})), 𝑧〉 ∨ ({〈1, 1〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0})) Btwn 〈𝑧,
({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 ∨ 𝑧 Btwn 〈({〈1, 0〉,
〈2, 0〉} ∪ ((3...𝑁) × {0})), ({〈1, 1〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))〉) ↔ (({〈1,
0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})) Btwn 〈({〈1,
1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})), ({〈1, 0〉,
〈2, 1〉} ∪ ((3...𝑁) × {0}))〉 ∨ ({〈1,
1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})) Btwn 〈({〈1,
0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0})), ({〈1, 0〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 ∨ ({〈1,
0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0})) Btwn 〈({〈1,
0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})), ({〈1, 1〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))〉))) |
165 | 164 | notbid 321 |
. . . . 5
⊢ (𝑧 = ({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0})) → (¬ (({〈1, 0〉, 〈2, 0〉} ∪
((3...𝑁) × {0})) Btwn
〈({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})), 𝑧〉 ∨ ({〈1, 1〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0})) Btwn 〈𝑧,
({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 ∨ 𝑧 Btwn 〈({〈1, 0〉,
〈2, 0〉} ∪ ((3...𝑁) × {0})), ({〈1, 1〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))〉) ↔ ¬
(({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})) Btwn 〈({〈1,
1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})), ({〈1, 0〉,
〈2, 1〉} ∪ ((3...𝑁) × {0}))〉 ∨ ({〈1,
1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})) Btwn 〈({〈1,
0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0})), ({〈1, 0〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 ∨ ({〈1,
0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0})) Btwn 〈({〈1,
0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})), ({〈1, 1〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))〉))) |
166 | 158, 165 | 3anbi23d 1441 |
. . . 4
⊢ (𝑧 = ({〈1, 0〉, 〈2,
1〉} ∪ ((3...𝑁)
× {0})) → (((𝑘
∈ (1...(𝑁 − 1))
↦ if(𝑘 = 1,
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})), ({〈(𝑘 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑘 + 1)}) ×
{0})))):(1...(𝑁 −
1))–1-1→(𝔼‘𝑁) ∧ ∀𝑖 ∈ (2...(𝑁 − 1))(〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), ({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) ×
{0}))〉Cgr〈((𝑘
∈ (1...(𝑁 − 1))
↦ if(𝑘 = 1,
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})), ({〈(𝑘 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑘 + 1)}) ×
{0}))))‘𝑖),
({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 ∧ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), ({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) ×
{0}))〉Cgr〈((𝑘
∈ (1...(𝑁 − 1))
↦ if(𝑘 = 1,
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})), ({〈(𝑘 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑘 + 1)}) ×
{0}))))‘𝑖),
({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 ∧ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑧〉Cgr〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑧〉) ∧ ¬ (({〈1,
0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})) Btwn 〈({〈1,
1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})), 𝑧〉 ∨ ({〈1, 1〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0})) Btwn 〈𝑧,
({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 ∨ 𝑧 Btwn 〈({〈1, 0〉,
〈2, 0〉} ∪ ((3...𝑁) × {0})), ({〈1, 1〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))〉)) ↔ ((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0})))):(1...(𝑁 −
1))–1-1→(𝔼‘𝑁) ∧ ∀𝑖 ∈ (2...(𝑁 − 1))(〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), ({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) ×
{0}))〉Cgr〈((𝑘
∈ (1...(𝑁 − 1))
↦ if(𝑘 = 1,
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})), ({〈(𝑘 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑘 + 1)}) ×
{0}))))‘𝑖),
({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 ∧ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), ({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) ×
{0}))〉Cgr〈((𝑘
∈ (1...(𝑁 − 1))
↦ if(𝑘 = 1,
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})), ({〈(𝑘 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑘 + 1)}) ×
{0}))))‘𝑖),
({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 ∧ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), ({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) ×
{0}))〉Cgr〈((𝑘
∈ (1...(𝑁 − 1))
↦ if(𝑘 = 1,
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})), ({〈(𝑘 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑘 + 1)}) ×
{0}))))‘𝑖),
({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))〉) ∧ ¬
(({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})) Btwn 〈({〈1,
1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})), ({〈1, 0〉,
〈2, 1〉} ∪ ((3...𝑁) × {0}))〉 ∨ ({〈1,
1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})) Btwn 〈({〈1,
0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0})), ({〈1, 0〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 ∨ ({〈1,
0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0})) Btwn 〈({〈1,
0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})), ({〈1, 1〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))〉)))) |
167 | 140, 153,
166 | rspc3ev 3566 |
. . 3
⊢
(((({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})) ∈ (𝔼‘𝑁) ∧ ({〈1, 1〉,
〈2, 0〉} ∪ ((3...𝑁) × {0})) ∈ (𝔼‘𝑁) ∧ ({〈1, 0〉,
〈2, 1〉} ∪ ((3...𝑁) × {0})) ∈ (𝔼‘𝑁)) ∧ ((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0})))):(1...(𝑁 −
1))–1-1→(𝔼‘𝑁) ∧ ∀𝑖 ∈ (2...(𝑁 − 1))(〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), ({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) ×
{0}))〉Cgr〈((𝑘
∈ (1...(𝑁 − 1))
↦ if(𝑘 = 1,
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})), ({〈(𝑘 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑘 + 1)}) ×
{0}))))‘𝑖),
({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 ∧ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), ({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) ×
{0}))〉Cgr〈((𝑘
∈ (1...(𝑁 − 1))
↦ if(𝑘 = 1,
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})), ({〈(𝑘 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑘 + 1)}) ×
{0}))))‘𝑖),
({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 ∧ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), ({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) ×
{0}))〉Cgr〈((𝑘
∈ (1...(𝑁 − 1))
↦ if(𝑘 = 1,
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})), ({〈(𝑘 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑘 + 1)}) ×
{0}))))‘𝑖),
({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0}))〉) ∧ ¬
(({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})) Btwn 〈({〈1,
1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})), ({〈1, 0〉,
〈2, 1〉} ∪ ((3...𝑁) × {0}))〉 ∨ ({〈1,
1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})) Btwn 〈({〈1,
0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0})), ({〈1, 0〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))〉 ∨ ({〈1,
0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0})) Btwn 〈({〈1,
0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})), ({〈1, 1〉,
〈2, 0〉} ∪ ((3...𝑁) × {0}))〉))) → ∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∃𝑧 ∈ (𝔼‘𝑁)((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0})))):(1...(𝑁 −
1))–1-1→(𝔼‘𝑁) ∧ ∀𝑖 ∈ (2...(𝑁 − 1))(〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑥〉Cgr〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑥〉 ∧ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑦〉Cgr〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑦〉 ∧ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑧〉Cgr〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑧〉) ∧ ¬ (𝑥 Btwn 〈𝑦, 𝑧〉 ∨ 𝑦 Btwn 〈𝑧, 𝑥〉 ∨ 𝑧 Btwn 〈𝑥, 𝑦〉))) |
168 | 4, 7, 9, 11, 125, 127, 167 | syl33anc 1387 |
. 2
⊢ (𝑁 ∈
(ℤ≥‘3) → ∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∃𝑧 ∈ (𝔼‘𝑁)((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0})))):(1...(𝑁 −
1))–1-1→(𝔼‘𝑁) ∧ ∀𝑖 ∈ (2...(𝑁 − 1))(〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑥〉Cgr〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑥〉 ∧ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑦〉Cgr〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑦〉 ∧ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑧〉Cgr〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑧〉) ∧ ¬ (𝑥 Btwn 〈𝑦, 𝑧〉 ∨ 𝑦 Btwn 〈𝑧, 𝑥〉 ∨ 𝑧 Btwn 〈𝑥, 𝑦〉))) |
169 | | ovex 7268 |
. . . 4
⊢
(1...(𝑁 − 1))
∈ V |
170 | 169 | mptex 7061 |
. . 3
⊢ (𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) × {0}))))
∈ V |
171 | | f1eq1 6632 |
. . . . . 6
⊢ (𝑝 = (𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) × {0}))))
→ (𝑝:(1...(𝑁 − 1))–1-1→(𝔼‘𝑁) ↔ (𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0})))):(1...(𝑁 −
1))–1-1→(𝔼‘𝑁))) |
172 | | fveq1 6738 |
. . . . . . . . . 10
⊢ (𝑝 = (𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) × {0}))))
→ (𝑝‘1) =
((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪
(((1...𝑁) ∖ {3})
× {0})), ({〈(𝑘 +
1), 1〉} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) ×
{0}))))‘1)) |
173 | 172 | opeq1d 4807 |
. . . . . . . . 9
⊢ (𝑝 = (𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) × {0}))))
→ 〈(𝑝‘1),
𝑥〉 = 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑥〉) |
174 | | fveq1 6738 |
. . . . . . . . . 10
⊢ (𝑝 = (𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) × {0}))))
→ (𝑝‘𝑖) = ((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖)) |
175 | 174 | opeq1d 4807 |
. . . . . . . . 9
⊢ (𝑝 = (𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) × {0}))))
→ 〈(𝑝‘𝑖), 𝑥〉 = 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑥〉) |
176 | 173, 175 | breq12d 5083 |
. . . . . . . 8
⊢ (𝑝 = (𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) × {0}))))
→ (〈(𝑝‘1),
𝑥〉Cgr〈(𝑝‘𝑖), 𝑥〉 ↔ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑥〉Cgr〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑥〉)) |
177 | 172 | opeq1d 4807 |
. . . . . . . . 9
⊢ (𝑝 = (𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) × {0}))))
→ 〈(𝑝‘1),
𝑦〉 = 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑦〉) |
178 | 174 | opeq1d 4807 |
. . . . . . . . 9
⊢ (𝑝 = (𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) × {0}))))
→ 〈(𝑝‘𝑖), 𝑦〉 = 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑦〉) |
179 | 177, 178 | breq12d 5083 |
. . . . . . . 8
⊢ (𝑝 = (𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) × {0}))))
→ (〈(𝑝‘1),
𝑦〉Cgr〈(𝑝‘𝑖), 𝑦〉 ↔ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑦〉Cgr〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑦〉)) |
180 | 172 | opeq1d 4807 |
. . . . . . . . 9
⊢ (𝑝 = (𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) × {0}))))
→ 〈(𝑝‘1),
𝑧〉 = 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑧〉) |
181 | 174 | opeq1d 4807 |
. . . . . . . . 9
⊢ (𝑝 = (𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) × {0}))))
→ 〈(𝑝‘𝑖), 𝑧〉 = 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑧〉) |
182 | 180, 181 | breq12d 5083 |
. . . . . . . 8
⊢ (𝑝 = (𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) × {0}))))
→ (〈(𝑝‘1),
𝑧〉Cgr〈(𝑝‘𝑖), 𝑧〉 ↔ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑧〉Cgr〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑧〉)) |
183 | 176, 179,
182 | 3anbi123d 1438 |
. . . . . . 7
⊢ (𝑝 = (𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) × {0}))))
→ ((〈(𝑝‘1),
𝑥〉Cgr〈(𝑝‘𝑖), 𝑥〉 ∧ 〈(𝑝‘1), 𝑦〉Cgr〈(𝑝‘𝑖), 𝑦〉 ∧ 〈(𝑝‘1), 𝑧〉Cgr〈(𝑝‘𝑖), 𝑧〉) ↔ (〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑥〉Cgr〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑥〉 ∧ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑦〉Cgr〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑦〉 ∧ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑧〉Cgr〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑧〉))) |
184 | 183 | ralbidv 3121 |
. . . . . 6
⊢ (𝑝 = (𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) × {0}))))
→ (∀𝑖 ∈
(2...(𝑁 −
1))(〈(𝑝‘1),
𝑥〉Cgr〈(𝑝‘𝑖), 𝑥〉 ∧ 〈(𝑝‘1), 𝑦〉Cgr〈(𝑝‘𝑖), 𝑦〉 ∧ 〈(𝑝‘1), 𝑧〉Cgr〈(𝑝‘𝑖), 𝑧〉) ↔ ∀𝑖 ∈ (2...(𝑁 − 1))(〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑥〉Cgr〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑥〉 ∧ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑦〉Cgr〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑦〉 ∧ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑧〉Cgr〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑧〉))) |
185 | 171, 184 | 3anbi12d 1439 |
. . . . 5
⊢ (𝑝 = (𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) × {0}))))
→ ((𝑝:(1...(𝑁 − 1))–1-1→(𝔼‘𝑁) ∧ ∀𝑖 ∈ (2...(𝑁 − 1))(〈(𝑝‘1), 𝑥〉Cgr〈(𝑝‘𝑖), 𝑥〉 ∧ 〈(𝑝‘1), 𝑦〉Cgr〈(𝑝‘𝑖), 𝑦〉 ∧ 〈(𝑝‘1), 𝑧〉Cgr〈(𝑝‘𝑖), 𝑧〉) ∧ ¬ (𝑥 Btwn 〈𝑦, 𝑧〉 ∨ 𝑦 Btwn 〈𝑧, 𝑥〉 ∨ 𝑧 Btwn 〈𝑥, 𝑦〉)) ↔ ((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0})))):(1...(𝑁 −
1))–1-1→(𝔼‘𝑁) ∧ ∀𝑖 ∈ (2...(𝑁 − 1))(〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑥〉Cgr〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑥〉 ∧ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑦〉Cgr〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑦〉 ∧ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑧〉Cgr〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑧〉) ∧ ¬ (𝑥 Btwn 〈𝑦, 𝑧〉 ∨ 𝑦 Btwn 〈𝑧, 𝑥〉 ∨ 𝑧 Btwn 〈𝑥, 𝑦〉)))) |
186 | 185 | rexbidv 3226 |
. . . 4
⊢ (𝑝 = (𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) × {0}))))
→ (∃𝑧 ∈
(𝔼‘𝑁)(𝑝:(1...(𝑁 − 1))–1-1→(𝔼‘𝑁) ∧ ∀𝑖 ∈ (2...(𝑁 − 1))(〈(𝑝‘1), 𝑥〉Cgr〈(𝑝‘𝑖), 𝑥〉 ∧ 〈(𝑝‘1), 𝑦〉Cgr〈(𝑝‘𝑖), 𝑦〉 ∧ 〈(𝑝‘1), 𝑧〉Cgr〈(𝑝‘𝑖), 𝑧〉) ∧ ¬ (𝑥 Btwn 〈𝑦, 𝑧〉 ∨ 𝑦 Btwn 〈𝑧, 𝑥〉 ∨ 𝑧 Btwn 〈𝑥, 𝑦〉)) ↔ ∃𝑧 ∈ (𝔼‘𝑁)((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0})))):(1...(𝑁 −
1))–1-1→(𝔼‘𝑁) ∧ ∀𝑖 ∈ (2...(𝑁 − 1))(〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑥〉Cgr〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑥〉 ∧ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑦〉Cgr〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑦〉 ∧ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑧〉Cgr〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑧〉) ∧ ¬ (𝑥 Btwn 〈𝑦, 𝑧〉 ∨ 𝑦 Btwn 〈𝑧, 𝑥〉 ∨ 𝑧 Btwn 〈𝑥, 𝑦〉)))) |
187 | 186 | 2rexbidv 3229 |
. . 3
⊢ (𝑝 = (𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) × {0}))))
→ (∃𝑥 ∈
(𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∃𝑧 ∈ (𝔼‘𝑁)(𝑝:(1...(𝑁 − 1))–1-1→(𝔼‘𝑁) ∧ ∀𝑖 ∈ (2...(𝑁 − 1))(〈(𝑝‘1), 𝑥〉Cgr〈(𝑝‘𝑖), 𝑥〉 ∧ 〈(𝑝‘1), 𝑦〉Cgr〈(𝑝‘𝑖), 𝑦〉 ∧ 〈(𝑝‘1), 𝑧〉Cgr〈(𝑝‘𝑖), 𝑧〉) ∧ ¬ (𝑥 Btwn 〈𝑦, 𝑧〉 ∨ 𝑦 Btwn 〈𝑧, 𝑥〉 ∨ 𝑧 Btwn 〈𝑥, 𝑦〉)) ↔ ∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∃𝑧 ∈ (𝔼‘𝑁)((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0})))):(1...(𝑁 −
1))–1-1→(𝔼‘𝑁) ∧ ∀𝑖 ∈ (2...(𝑁 − 1))(〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑥〉Cgr〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑥〉 ∧ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑦〉Cgr〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑦〉 ∧ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑧〉Cgr〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑧〉) ∧ ¬ (𝑥 Btwn 〈𝑦, 𝑧〉 ∨ 𝑦 Btwn 〈𝑧, 𝑥〉 ∨ 𝑧 Btwn 〈𝑥, 𝑦〉)))) |
188 | 170, 187 | spcev 3536 |
. 2
⊢
(∃𝑥 ∈
(𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∃𝑧 ∈ (𝔼‘𝑁)((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0})))):(1...(𝑁 −
1))–1-1→(𝔼‘𝑁) ∧ ∀𝑖 ∈ (2...(𝑁 − 1))(〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑥〉Cgr〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑥〉 ∧ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑦〉Cgr〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑦〉 ∧ 〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1), 𝑧〉Cgr〈((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖), 𝑧〉) ∧ ¬ (𝑥 Btwn 〈𝑦, 𝑧〉 ∨ 𝑦 Btwn 〈𝑧, 𝑥〉 ∨ 𝑧 Btwn 〈𝑥, 𝑦〉)) → ∃𝑝∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∃𝑧 ∈ (𝔼‘𝑁)(𝑝:(1...(𝑁 − 1))–1-1→(𝔼‘𝑁) ∧ ∀𝑖 ∈ (2...(𝑁 − 1))(〈(𝑝‘1), 𝑥〉Cgr〈(𝑝‘𝑖), 𝑥〉 ∧ 〈(𝑝‘1), 𝑦〉Cgr〈(𝑝‘𝑖), 𝑦〉 ∧ 〈(𝑝‘1), 𝑧〉Cgr〈(𝑝‘𝑖), 𝑧〉) ∧ ¬ (𝑥 Btwn 〈𝑦, 𝑧〉 ∨ 𝑦 Btwn 〈𝑧, 𝑥〉 ∨ 𝑧 Btwn 〈𝑥, 𝑦〉))) |
189 | 168, 188 | syl 17 |
1
⊢ (𝑁 ∈
(ℤ≥‘3) → ∃𝑝∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∃𝑧 ∈ (𝔼‘𝑁)(𝑝:(1...(𝑁 − 1))–1-1→(𝔼‘𝑁) ∧ ∀𝑖 ∈ (2...(𝑁 − 1))(〈(𝑝‘1), 𝑥〉Cgr〈(𝑝‘𝑖), 𝑥〉 ∧ 〈(𝑝‘1), 𝑦〉Cgr〈(𝑝‘𝑖), 𝑦〉 ∧ 〈(𝑝‘1), 𝑧〉Cgr〈(𝑝‘𝑖), 𝑧〉) ∧ ¬ (𝑥 Btwn 〈𝑦, 𝑧〉 ∨ 𝑦 Btwn 〈𝑧, 𝑥〉 ∨ 𝑧 Btwn 〈𝑥, 𝑦〉))) |