Step | Hyp | Ref
| Expression |
1 | | uzuzle23 12035 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈
(ℤ≥‘2)) |
2 | | 0re 10378 |
. . . . 5
⊢ 0 ∈
ℝ |
3 | 2, 2 | axlowdimlem5 26295 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘2) → ({〈1, 0〉, 〈2, 0〉}
∪ ((3...𝑁) ×
{0})) ∈ (𝔼‘𝑁)) |
4 | 1, 3 | syl 17 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘3) → ({〈1, 0〉, 〈2, 0〉}
∪ ((3...𝑁) ×
{0})) ∈ (𝔼‘𝑁)) |
5 | | 1re 10376 |
. . . . 5
⊢ 1 ∈
ℝ |
6 | 5, 2 | axlowdimlem5 26295 |
. . . 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 26295 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘2) → ({〈1, 0〉, 〈2, 1〉}
∪ ((3...𝑁) ×
{0})) ∈ (𝔼‘𝑁)) |
9 | 1, 8 | syl 17 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘3) → ({〈1, 0〉, 〈2, 1〉}
∪ ((3...𝑁) ×
{0})) ∈ (𝔼‘𝑁)) |
10 | | eqid 2778 |
. . . 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 26305 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0})))):(1...(𝑁 −
1))–1-1→(𝔼‘𝑁)) |
12 | | eqid 2778 |
. . . . . 6
⊢
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})) = ({〈3,
-1〉} ∪ (((1...𝑁)
∖ {3}) × {0})) |
13 | | eqid 2778 |
. . . . . 6
⊢
({〈(𝑖 + 1),
1〉} ∪ (((1...𝑁)
∖ {(𝑖 + 1)}) ×
{0})) = ({〈(𝑖 + 1),
1〉} ∪ (((1...𝑁)
∖ {(𝑖 + 1)}) ×
{0})) |
14 | | eqid 2778 |
. . . . . 6
⊢
({〈1, 0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})) = ({〈1, 0〉,
〈2, 0〉} ∪ ((3...𝑁) × {0})) |
15 | 12, 13, 14, 2, 2 | axlowdimlem17 26307 |
. . . . 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 2778 |
. . . . . 6
⊢
({〈1, 1〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})) = ({〈1, 1〉,
〈2, 0〉} ∪ ((3...𝑁) × {0})) |
17 | 12, 13, 16, 5, 2 | axlowdimlem17 26307 |
. . . . 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 2778 |
. . . . . 6
⊢
({〈1, 0〉, 〈2, 1〉} ∪ ((3...𝑁) × {0})) = ({〈1, 0〉,
〈2, 1〉} ∪ ((3...𝑁) × {0})) |
19 | 12, 13, 18, 2, 5 | axlowdimlem17 26307 |
. . . . 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 11760 |
. . . . . . . . . . . . . 14
⊢ ((3
∈ ℤ ∧ 𝑁
∈ ℤ ∧ 3 ≤ 𝑁) → 1 ∈ ℤ) |
21 | | peano2zm 11772 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈
ℤ) |
22 | 21 | 3ad2ant2 1125 |
. . . . . . . . . . . . . 14
⊢ ((3
∈ ℤ ∧ 𝑁
∈ ℤ ∧ 3 ≤ 𝑁) → (𝑁 − 1) ∈ ℤ) |
23 | | 2m1e1 11508 |
. . . . . . . . . . . . . . 15
⊢ (2
− 1) = 1 |
24 | | 2re 11449 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 ∈
ℝ |
25 | | 3re 11455 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 3 ∈
ℝ |
26 | | 2lt3 11554 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 <
3 |
27 | 24, 25, 26 | ltleii 10499 |
. . . . . . . . . . . . . . . . . . 19
⊢ 2 ≤
3 |
28 | | zre 11732 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) |
29 | | letr 10470 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((2
∈ ℝ ∧ 3 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((2 ≤ 3 ∧ 3
≤ 𝑁) → 2 ≤ 𝑁)) |
30 | 24, 25, 29 | mp3an12 1524 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℝ → ((2 ≤
3 ∧ 3 ≤ 𝑁) → 2
≤ 𝑁)) |
31 | 28, 30 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℤ → ((2 ≤
3 ∧ 3 ≤ 𝑁) → 2
≤ 𝑁)) |
32 | 27, 31 | mpani 686 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℤ → (3 ≤
𝑁 → 2 ≤ 𝑁)) |
33 | 32 | imp 397 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℤ ∧ 3 ≤
𝑁) → 2 ≤ 𝑁) |
34 | 33 | 3adant1 1121 |
. . . . . . . . . . . . . . . 16
⊢ ((3
∈ ℤ ∧ 𝑁
∈ ℤ ∧ 3 ≤ 𝑁) → 2 ≤ 𝑁) |
35 | 28 | 3ad2ant2 1125 |
. . . . . . . . . . . . . . . . 17
⊢ ((3
∈ ℤ ∧ 𝑁
∈ ℤ ∧ 3 ≤ 𝑁) → 𝑁 ∈ ℝ) |
36 | | lesub1 10869 |
. . . . . . . . . . . . . . . . . 18
⊢ ((2
∈ ℝ ∧ 𝑁
∈ ℝ ∧ 1 ∈ ℝ) → (2 ≤ 𝑁 ↔ (2 − 1) ≤ (𝑁 − 1))) |
37 | 24, 5, 36 | mp3an13 1525 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℝ → (2 ≤
𝑁 ↔ (2 − 1) ≤
(𝑁 −
1))) |
38 | 35, 37 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((3
∈ ℤ ∧ 𝑁
∈ ℤ ∧ 3 ≤ 𝑁) → (2 ≤ 𝑁 ↔ (2 − 1) ≤ (𝑁 − 1))) |
39 | 34, 38 | mpbid 224 |
. . . . . . . . . . . . . . 15
⊢ ((3
∈ ℤ ∧ 𝑁
∈ ℤ ∧ 3 ≤ 𝑁) → (2 − 1) ≤ (𝑁 − 1)) |
40 | 23, 39 | syl5eqbrr 4922 |
. . . . . . . . . . . . . 14
⊢ ((3
∈ ℤ ∧ 𝑁
∈ ℤ ∧ 3 ≤ 𝑁) → 1 ≤ (𝑁 − 1)) |
41 | 20, 22, 40 | 3jca 1119 |
. . . . . . . . . . . . 13
⊢ ((3
∈ ℤ ∧ 𝑁
∈ ℤ ∧ 3 ≤ 𝑁) → (1 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ ∧
1 ≤ (𝑁 −
1))) |
42 | | eluz2 11998 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈
(ℤ≥‘3) ↔ (3 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 3 ≤
𝑁)) |
43 | | eluz2 11998 |
. . . . . . . . . . . . 13
⊢ ((𝑁 − 1) ∈
(ℤ≥‘1) ↔ (1 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ ∧
1 ≤ (𝑁 −
1))) |
44 | 41, 42, 43 | 3imtr4i 284 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − 1) ∈
(ℤ≥‘1)) |
45 | | eluzfz1 12665 |
. . . . . . . . . . . 12
⊢ ((𝑁 − 1) ∈
(ℤ≥‘1) → 1 ∈ (1...(𝑁 − 1))) |
46 | 44, 45 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘3) → 1 ∈ (1...(𝑁 − 1))) |
47 | 46 | adantr 474 |
. . . . . . . . . 10
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑖 ∈ (2...(𝑁 − 1))) → 1 ∈ (1...(𝑁 − 1))) |
48 | | eqeq1 2782 |
. . . . . . . . . . . 12
⊢ (𝑘 = 1 → (𝑘 = 1 ↔ 1 = 1)) |
49 | | oveq1 6929 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 1 → (𝑘 + 1) = (1 + 1)) |
50 | 49 | opeq1d 4642 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 1 → 〈(𝑘 + 1), 1〉 = 〈(1 + 1),
1〉) |
51 | 50 | sneqd 4410 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 1 → {〈(𝑘 + 1), 1〉} = {〈(1 +
1), 1〉}) |
52 | 49 | sneqd 4410 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 1 → {(𝑘 + 1)} = {(1 + 1)}) |
53 | 52 | difeq2d 3951 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 1 → ((1...𝑁) ∖ {(𝑘 + 1)}) = ((1...𝑁) ∖ {(1 + 1)})) |
54 | 53 | xpeq1d 5384 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 1 → (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}) = (((1...𝑁) ∖ {(1 + 1)}) ×
{0})) |
55 | 51, 54 | uneq12d 3991 |
. . . . . . . . . . . 12
⊢ (𝑘 = 1 → ({〈(𝑘 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑘 + 1)}) × {0})) =
({〈(1 + 1), 1〉} ∪ (((1...𝑁) ∖ {(1 + 1)}) ×
{0}))) |
56 | 48, 55 | ifbieq2d 4332 |
. . . . . . . . . . 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})))) |
57 | | snex 5140 |
. . . . . . . . . . . . 13
⊢ {〈3,
-1〉} ∈ V |
58 | | ovex 6954 |
. . . . . . . . . . . . . . 15
⊢
(1...𝑁) ∈
V |
59 | | difexg 5045 |
. . . . . . . . . . . . . . 15
⊢
((1...𝑁) ∈ V
→ ((1...𝑁) ∖
{3}) ∈ V) |
60 | 58, 59 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
((1...𝑁) ∖
{3}) ∈ V |
61 | | snex 5140 |
. . . . . . . . . . . . . 14
⊢ {0}
∈ V |
62 | 60, 61 | xpex 7240 |
. . . . . . . . . . . . 13
⊢
(((1...𝑁) ∖
{3}) × {0}) ∈ V |
63 | 57, 62 | unex 7233 |
. . . . . . . . . . . 12
⊢
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})) ∈
V |
64 | | snex 5140 |
. . . . . . . . . . . . 13
⊢ {〈(1
+ 1), 1〉} ∈ V |
65 | | difexg 5045 |
. . . . . . . . . . . . . . 15
⊢
((1...𝑁) ∈ V
→ ((1...𝑁) ∖ {(1
+ 1)}) ∈ V) |
66 | 58, 65 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
((1...𝑁) ∖ {(1
+ 1)}) ∈ V |
67 | 66, 61 | xpex 7240 |
. . . . . . . . . . . . 13
⊢
(((1...𝑁) ∖
{(1 + 1)}) × {0}) ∈ V |
68 | 64, 67 | unex 7233 |
. . . . . . . . . . . 12
⊢
({〈(1 + 1), 1〉} ∪ (((1...𝑁) ∖ {(1 + 1)}) × {0})) ∈
V |
69 | 63, 68 | ifex 4355 |
. . . . . . . . . . 11
⊢ if(1 = 1,
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})), ({〈(1 +
1), 1〉} ∪ (((1...𝑁) ∖ {(1 + 1)}) × {0}))) ∈
V |
70 | 56, 10, 69 | fvmpt 6542 |
. . . . . . . . . 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})))) |
71 | 47, 70 | 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})))) |
72 | | eqid 2778 |
. . . . . . . . . 10
⊢ 1 =
1 |
73 | 72 | iftruei 4314 |
. . . . . . . . 9
⊢ if(1 = 1,
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})), ({〈(1 +
1), 1〉} ∪ (((1...𝑁) ∖ {(1 + 1)}) × {0}))) =
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) ×
{0})) |
74 | 71, 73 | syl6eq 2830 |
. . . . . . . 8
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑖 ∈ (2...(𝑁 − 1))) → ((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1) = ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) ×
{0}))) |
75 | 74 | opeq1d 4642 |
. . . . . . 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}))〉) |
76 | | 2eluzge1 12040 |
. . . . . . . . . . . . 13
⊢ 2 ∈
(ℤ≥‘1) |
77 | | fzss1 12697 |
. . . . . . . . . . . . 13
⊢ (2 ∈
(ℤ≥‘1) → (2...(𝑁 − 1)) ⊆ (1...(𝑁 − 1))) |
78 | 76, 77 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
(2...(𝑁 − 1))
⊆ (1...(𝑁 −
1)) |
79 | 78 | sseli 3817 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ (2...(𝑁 − 1)) → 𝑖 ∈ (1...(𝑁 − 1))) |
80 | 79 | adantl 475 |
. . . . . . . . . 10
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑖 ∈ (2...(𝑁 − 1))) → 𝑖 ∈ (1...(𝑁 − 1))) |
81 | | eqeq1 2782 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑖 → (𝑘 = 1 ↔ 𝑖 = 1)) |
82 | | oveq1 6929 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑖 → (𝑘 + 1) = (𝑖 + 1)) |
83 | 82 | opeq1d 4642 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑖 → 〈(𝑘 + 1), 1〉 = 〈(𝑖 + 1), 1〉) |
84 | 83 | sneqd 4410 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑖 → {〈(𝑘 + 1), 1〉} = {〈(𝑖 + 1), 1〉}) |
85 | 82 | sneqd 4410 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑖 → {(𝑘 + 1)} = {(𝑖 + 1)}) |
86 | 85 | difeq2d 3951 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑖 → ((1...𝑁) ∖ {(𝑘 + 1)}) = ((1...𝑁) ∖ {(𝑖 + 1)})) |
87 | 86 | xpeq1d 5384 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑖 → (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}) = (((1...𝑁) ∖ {(𝑖 + 1)}) × {0})) |
88 | 84, 87 | uneq12d 3991 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑖 → ({〈(𝑘 + 1), 1〉} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})) = ({〈(𝑖 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑖 + 1)}) ×
{0}))) |
89 | 81, 88 | ifbieq2d 4332 |
. . . . . . . . . . 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})))) |
90 | | snex 5140 |
. . . . . . . . . . . . 13
⊢
{〈(𝑖 + 1),
1〉} ∈ V |
91 | | difexg 5045 |
. . . . . . . . . . . . . . 15
⊢
((1...𝑁) ∈ V
→ ((1...𝑁) ∖
{(𝑖 + 1)}) ∈
V) |
92 | 58, 91 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
((1...𝑁) ∖
{(𝑖 + 1)}) ∈
V |
93 | 92, 61 | xpex 7240 |
. . . . . . . . . . . . 13
⊢
(((1...𝑁) ∖
{(𝑖 + 1)}) × {0})
∈ V |
94 | 90, 93 | unex 7233 |
. . . . . . . . . . . 12
⊢
({〈(𝑖 + 1),
1〉} ∪ (((1...𝑁)
∖ {(𝑖 + 1)}) ×
{0})) ∈ V |
95 | 63, 94 | ifex 4355 |
. . . . . . . . . . 11
⊢ if(𝑖 = 1, ({〈3, -1〉} ∪
(((1...𝑁) ∖ {3})
× {0})), ({〈(𝑖 +
1), 1〉} ∪ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0}))) ∈
V |
96 | 89, 10, 95 | fvmpt 6542 |
. . . . . . . . . 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})))) |
97 | 80, 96 | 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})))) |
98 | | 1lt2 11553 |
. . . . . . . . . . . . . . . 16
⊢ 1 <
2 |
99 | 5, 24 | ltnlei 10497 |
. . . . . . . . . . . . . . . 16
⊢ (1 < 2
↔ ¬ 2 ≤ 1) |
100 | 98, 99 | mpbi 222 |
. . . . . . . . . . . . . . 15
⊢ ¬ 2
≤ 1 |
101 | 100 | intnanr 483 |
. . . . . . . . . . . . . 14
⊢ ¬ (2
≤ 1 ∧ 1 ≤ (𝑁
− 1)) |
102 | | eluzelz 12002 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈ ℤ) |
103 | 102, 21 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − 1) ∈ ℤ) |
104 | | 1z 11759 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℤ |
105 | | 2z 11761 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℤ |
106 | | elfz 12649 |
. . . . . . . . . . . . . . . 16
⊢ ((1
∈ ℤ ∧ 2 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) → (1 ∈
(2...(𝑁 − 1)) ↔
(2 ≤ 1 ∧ 1 ≤ (𝑁
− 1)))) |
107 | 104, 105,
106 | mp3an12 1524 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 − 1) ∈ ℤ
→ (1 ∈ (2...(𝑁
− 1)) ↔ (2 ≤ 1 ∧ 1 ≤ (𝑁 − 1)))) |
108 | 103, 107 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘3) → (1 ∈ (2...(𝑁 − 1)) ↔ (2 ≤ 1 ∧ 1 ≤
(𝑁 −
1)))) |
109 | 101, 108 | mtbiri 319 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈
(ℤ≥‘3) → ¬ 1 ∈ (2...(𝑁 − 1))) |
110 | | eleq1 2847 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 1 → (𝑖 ∈ (2...(𝑁 − 1)) ↔ 1 ∈ (2...(𝑁 − 1)))) |
111 | 110 | notbid 310 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 1 → (¬ 𝑖 ∈ (2...(𝑁 − 1)) ↔ ¬ 1 ∈
(2...(𝑁 −
1)))) |
112 | 109, 111 | syl5ibrcom 239 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑖 = 1 → ¬ 𝑖 ∈ (2...(𝑁 − 1)))) |
113 | 112 | con2d 132 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑖 ∈ (2...(𝑁 − 1)) → ¬ 𝑖 = 1)) |
114 | 113 | imp 397 |
. . . . . . . . . 10
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑖 ∈ (2...(𝑁 − 1))) → ¬ 𝑖 = 1) |
115 | 114 | iffalsed 4318 |
. . . . . . . . 9
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑖 ∈ (2...(𝑁 − 1))) → if(𝑖 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑖 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑖 + 1)}) × {0}))) =
({〈(𝑖 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑖 + 1)}) ×
{0}))) |
116 | 97, 115 | eqtrd 2814 |
. . . . . . . 8
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑖 ∈ (2...(𝑁 − 1))) → ((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘𝑖) =
({〈(𝑖 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑖 + 1)}) ×
{0}))) |
117 | 116 | opeq1d 4642 |
. . . . . . 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}))〉) |
118 | 75, 117 | breq12d 4899 |
. . . . . 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}))〉)) |
119 | 74 | opeq1d 4642 |
. . . . . . 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}))〉) |
120 | 116 | opeq1d 4642 |
. . . . . . 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}))〉) |
121 | 119, 120 | breq12d 4899 |
. . . . . 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}))〉)) |
122 | 46, 70 | 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})))) |
123 | 122, 73 | syl6eq 2830 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘3) → ((𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0}))))‘1) = ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) ×
{0}))) |
124 | 123 | opeq1d 4642 |
. . . . . . . 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}))〉) |
125 | 124 | adantr 474 |
. . . . . . 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}))〉) |
126 | 116 | opeq1d 4642 |
. . . . . . 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}))〉) |
127 | 125, 126 | breq12d 4899 |
. . . . . 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}))〉)) |
128 | 118, 121,
127 | 3anbi123d 1509 |
. . . . 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}))〉))) |
129 | 15, 17, 19, 128 | mpbir3and 1399 |
. . . 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}))〉)) |
130 | 129 | ralrimiva 3148 |
. . 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}))〉)) |
131 | 14, 16, 18 | axlowdimlem6 26296 |
. . . 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}))〉)) |
132 | 1, 131 | 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}))〉)) |
133 | | opeq2 4637 |
. . . . . . . 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}))〉) |
134 | | opeq2 4637 |
. . . . . . . 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}))〉) |
135 | 133, 134 | breq12d 4899 |
. . . . . . 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}))〉)) |
136 | 135 | 3anbi1d 1513 |
. . . . . 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}))))‘𝑖), 𝑧〉))) |
137 | 136 | ralbidv 3168 |
. . . . 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}))))‘𝑖), 𝑧〉))) |
138 | | breq1 4889 |
. . . . . . 7
⊢ (𝑥 = ({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0})) → (𝑥
Btwn 〈𝑦, 𝑧〉 ↔ ({〈1,
0〉, 〈2, 0〉} ∪ ((3...𝑁) × {0})) Btwn 〈𝑦, 𝑧〉)) |
139 | | opeq2 4637 |
. . . . . . . 8
⊢ (𝑥 = ({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0})) → 〈𝑧, 𝑥〉 = 〈𝑧, ({〈1, 0〉, 〈2, 0〉} ∪
((3...𝑁) ×
{0}))〉) |
140 | 139 | breq2d 4898 |
. . . . . . 7
⊢ (𝑥 = ({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0})) → (𝑦
Btwn 〈𝑧, 𝑥〉 ↔ 𝑦 Btwn 〈𝑧, ({〈1, 0〉, 〈2, 0〉} ∪
((3...𝑁) ×
{0}))〉)) |
141 | | opeq1 4636 |
. . . . . . . 8
⊢ (𝑥 = ({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0})) → 〈𝑥, 𝑦〉 = 〈({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0})), 𝑦〉) |
142 | 141 | breq2d 4898 |
. . . . . . 7
⊢ (𝑥 = ({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0})) → (𝑧
Btwn 〈𝑥, 𝑦〉 ↔ 𝑧 Btwn 〈({〈1, 0〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0})), 𝑦〉)) |
143 | 138, 140,
142 | 3orbi123d 1508 |
. . . . . 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})), 𝑦〉))) |
144 | 143 | notbid 310 |
. . . . 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})), 𝑦〉))) |
145 | 137, 144 | 3anbi23d 1512 |
. . . 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})), 𝑦〉)))) |
146 | | opeq2 4637 |
. . . . . . . 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}))〉) |
147 | | opeq2 4637 |
. . . . . . . 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}))〉) |
148 | 146, 147 | breq12d 4899 |
. . . . . . 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}))〉)) |
149 | 148 | 3anbi2d 1514 |
. . . . . 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}))))‘𝑖), 𝑧〉))) |
150 | 149 | ralbidv 3168 |
. . . . 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}))))‘𝑖), 𝑧〉))) |
151 | | opeq1 4636 |
. . . . . . . 8
⊢ (𝑦 = ({〈1, 1〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0})) → 〈𝑦, 𝑧〉 = 〈({〈1, 1〉, 〈2,
0〉} ∪ ((3...𝑁)
× {0})), 𝑧〉) |
152 | 151 | breq2d 4898 |
. . . . . . 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})),
𝑧〉)) |
153 | | breq1 4889 |
. . . . . . 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}))〉)) |
154 | | opeq2 4637 |
. . . . . . . 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}))〉) |
155 | 154 | breq2d 4898 |
. . . . . . 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}))〉)) |
156 | 152, 153,
155 | 3orbi123d 1508 |
. . . . . 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}))〉))) |
157 | 156 | notbid 310 |
. . . . 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}))〉))) |
158 | 150, 157 | 3anbi23d 1512 |
. . . 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}))〉)))) |
159 | | opeq2 4637 |
. . . . . . . 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}))〉) |
160 | | opeq2 4637 |
. . . . . . . 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}))〉) |
161 | 159, 160 | breq12d 4899 |
. . . . . . 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}))〉)) |
162 | 161 | 3anbi3d 1515 |
. . . . . 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}))〉))) |
163 | 162 | ralbidv 3168 |
. . . . 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}))〉))) |
164 | | opeq2 4637 |
. . . . . . . 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}))〉) |
165 | 164 | breq2d 4898 |
. . . . . . 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}))〉)) |
166 | | opeq1 4636 |
. . . . . . . 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}))〉) |
167 | 166 | breq2d 4898 |
. . . . . . 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}))〉)) |
168 | | breq1 4889 |
. . . . . . 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}))〉)) |
169 | 165, 167,
168 | 3orbi123d 1508 |
. . . . . 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}))〉))) |
170 | 169 | notbid 310 |
. . . . 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}))〉))) |
171 | 163, 170 | 3anbi23d 1512 |
. . . 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}))〉)))) |
172 | 145, 158,
171 | rspc3ev 3528 |
. . 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 〈𝑥, 𝑦〉))) |
173 | 4, 7, 9, 11, 130, 132, 172 | syl33anc 1453 |
. 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 〈𝑥, 𝑦〉))) |
174 | | ovex 6954 |
. . . 4
⊢
(1...(𝑁 − 1))
∈ V |
175 | 174 | mptex 6758 |
. . 3
⊢ (𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) × {0}))))
∈ V |
176 | | f1eq1 6346 |
. . . . . 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→(𝔼‘𝑁))) |
177 | | fveq1 6445 |
. . . . . . . . . 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)) |
178 | 177 | opeq1d 4642 |
. . . . . . . . 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), 𝑥〉) |
179 | | fveq1 6445 |
. . . . . . . . . 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}))))‘𝑖)) |
180 | 179 | opeq1d 4642 |
. . . . . . . . 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}))))‘𝑖), 𝑥〉) |
181 | 178, 180 | breq12d 4899 |
. . . . . . . 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}))))‘𝑖), 𝑥〉)) |
182 | 177 | opeq1d 4642 |
. . . . . . . . 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), 𝑦〉) |
183 | 179 | opeq1d 4642 |
. . . . . . . . 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}))))‘𝑖), 𝑦〉) |
184 | 182, 183 | breq12d 4899 |
. . . . . . . 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}))))‘𝑖), 𝑦〉)) |
185 | 177 | opeq1d 4642 |
. . . . . . . . 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), 𝑧〉) |
186 | 179 | opeq1d 4642 |
. . . . . . . . 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}))))‘𝑖), 𝑧〉) |
187 | 185, 186 | breq12d 4899 |
. . . . . . . 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}))))‘𝑖), 𝑧〉)) |
188 | 181, 184,
187 | 3anbi123d 1509 |
. . . . . . 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}))))‘𝑖), 𝑧〉))) |
189 | 188 | ralbidv 3168 |
. . . . . 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}))))‘𝑖), 𝑧〉))) |
190 | 176, 189 | 3anbi12d 1510 |
. . . . 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 〈𝑥, 𝑦〉)))) |
191 | 190 | rexbidv 3237 |
. . . 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 〈𝑥, 𝑦〉)))) |
192 | 191 | 2rexbidv 3242 |
. . 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 〈𝑥, 𝑦〉)))) |
193 | 175, 192 | spcev 3502 |
. 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 〈𝑥, 𝑦〉))) |
194 | 173, 193 | syl 17 |
1
⊢ (𝑁 ∈
(ℤ≥‘3) → ∃𝑝∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∃𝑧 ∈ (𝔼‘𝑁)(𝑝:(1...(𝑁 − 1))–1-1→(𝔼‘𝑁) ∧ ∀𝑖 ∈ (2...(𝑁 − 1))(〈(𝑝‘1), 𝑥〉Cgr〈(𝑝‘𝑖), 𝑥〉 ∧ 〈(𝑝‘1), 𝑦〉Cgr〈(𝑝‘𝑖), 𝑦〉 ∧ 〈(𝑝‘1), 𝑧〉Cgr〈(𝑝‘𝑖), 𝑧〉) ∧ ¬ (𝑥 Btwn 〈𝑦, 𝑧〉 ∨ 𝑦 Btwn 〈𝑧, 𝑥〉 ∨ 𝑧 Btwn 〈𝑥, 𝑦〉))) |