Step | Hyp | Ref
| Expression |
1 | | uzuzle23 12819 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈
(ℤ≥‘2)) |
2 | | 0re 11162 |
. . . . 5
⊢ 0 ∈
ℝ |
3 | 2, 2 | axlowdimlem5 27937 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘2) → ({⟨1, 0⟩, ⟨2, 0⟩}
∪ ((3...𝑁) ×
{0})) ∈ (𝔼‘𝑁)) |
4 | 1, 3 | syl 17 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘3) → ({⟨1, 0⟩, ⟨2, 0⟩}
∪ ((3...𝑁) ×
{0})) ∈ (𝔼‘𝑁)) |
5 | | 1re 11160 |
. . . . 5
⊢ 1 ∈
ℝ |
6 | 5, 2 | axlowdimlem5 27937 |
. . . 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 27937 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘2) → ({⟨1, 0⟩, ⟨2, 1⟩}
∪ ((3...𝑁) ×
{0})) ∈ (𝔼‘𝑁)) |
9 | 1, 8 | syl 17 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘3) → ({⟨1, 0⟩, ⟨2, 1⟩}
∪ ((3...𝑁) ×
{0})) ∈ (𝔼‘𝑁)) |
10 | | eqid 2733 |
. . . 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 27947 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})),
({⟨(𝑘 + 1), 1⟩}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0})))):(1...(𝑁 −
1))–1-1→(𝔼‘𝑁)) |
12 | | eqid 2733 |
. . . . . 6
⊢
({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})) = ({⟨3,
-1⟩} ∪ (((1...𝑁)
∖ {3}) × {0})) |
13 | | eqid 2733 |
. . . . . 6
⊢
({⟨(𝑖 + 1),
1⟩} ∪ (((1...𝑁)
∖ {(𝑖 + 1)}) ×
{0})) = ({⟨(𝑖 + 1),
1⟩} ∪ (((1...𝑁)
∖ {(𝑖 + 1)}) ×
{0})) |
14 | | eqid 2733 |
. . . . . 6
⊢
({⟨1, 0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) = ({⟨1, 0⟩,
⟨2, 0⟩} ∪ ((3...𝑁) × {0})) |
15 | 12, 13, 14, 2, 2 | axlowdimlem17 27949 |
. . . . 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 2733 |
. . . . . 6
⊢
({⟨1, 1⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) = ({⟨1, 1⟩,
⟨2, 0⟩} ∪ ((3...𝑁) × {0})) |
17 | 12, 13, 16, 5, 2 | axlowdimlem17 27949 |
. . . . 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 2733 |
. . . . . 6
⊢
({⟨1, 0⟩, ⟨2, 1⟩} ∪ ((3...𝑁) × {0})) = ({⟨1, 0⟩,
⟨2, 1⟩} ∪ ((3...𝑁) × {0})) |
19 | 12, 13, 18, 2, 5 | axlowdimlem17 27949 |
. . . . 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 12539 |
. . . . . . . . . . . . . 14
⊢ ((3
∈ ℤ ∧ 𝑁
∈ ℤ ∧ 3 ≤ 𝑁) → 1 ∈ ℤ) |
21 | | peano2zm 12551 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈
ℤ) |
22 | 21 | 3ad2ant2 1135 |
. . . . . . . . . . . . . 14
⊢ ((3
∈ ℤ ∧ 𝑁
∈ ℤ ∧ 3 ≤ 𝑁) → (𝑁 − 1) ∈ ℤ) |
23 | | 2m1e1 12284 |
. . . . . . . . . . . . . . 15
⊢ (2
− 1) = 1 |
24 | | 2re 12232 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 ∈
ℝ |
25 | | 3re 12238 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 3 ∈
ℝ |
26 | | 2lt3 12330 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 <
3 |
27 | 24, 25, 26 | ltleii 11283 |
. . . . . . . . . . . . . . . . . . 19
⊢ 2 ≤
3 |
28 | | zre 12508 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) |
29 | | letr 11254 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((2
∈ ℝ ∧ 3 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((2 ≤ 3 ∧ 3
≤ 𝑁) → 2 ≤ 𝑁)) |
30 | 24, 25, 28, 29 | mp3an12i 1466 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℤ → ((2 ≤
3 ∧ 3 ≤ 𝑁) → 2
≤ 𝑁)) |
31 | 27, 30 | mpani 695 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℤ → (3 ≤
𝑁 → 2 ≤ 𝑁)) |
32 | 31 | imp 408 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℤ ∧ 3 ≤
𝑁) → 2 ≤ 𝑁) |
33 | 32 | 3adant1 1131 |
. . . . . . . . . . . . . . . 16
⊢ ((3
∈ ℤ ∧ 𝑁
∈ ℤ ∧ 3 ≤ 𝑁) → 2 ≤ 𝑁) |
34 | 28 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . . . 17
⊢ ((3
∈ ℤ ∧ 𝑁
∈ ℤ ∧ 3 ≤ 𝑁) → 𝑁 ∈ ℝ) |
35 | | lesub1 11654 |
. . . . . . . . . . . . . . . . . 18
⊢ ((2
∈ ℝ ∧ 𝑁
∈ ℝ ∧ 1 ∈ ℝ) → (2 ≤ 𝑁 ↔ (2 − 1) ≤ (𝑁 − 1))) |
36 | 24, 5, 35 | mp3an13 1453 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℝ → (2 ≤
𝑁 ↔ (2 − 1) ≤
(𝑁 −
1))) |
37 | 34, 36 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((3
∈ ℤ ∧ 𝑁
∈ ℤ ∧ 3 ≤ 𝑁) → (2 ≤ 𝑁 ↔ (2 − 1) ≤ (𝑁 − 1))) |
38 | 33, 37 | mpbid 231 |
. . . . . . . . . . . . . . 15
⊢ ((3
∈ ℤ ∧ 𝑁
∈ ℤ ∧ 3 ≤ 𝑁) → (2 − 1) ≤ (𝑁 − 1)) |
39 | 23, 38 | eqbrtrrid 5142 |
. . . . . . . . . . . . . 14
⊢ ((3
∈ ℤ ∧ 𝑁
∈ ℤ ∧ 3 ≤ 𝑁) → 1 ≤ (𝑁 − 1)) |
40 | 20, 22, 39 | 3jca 1129 |
. . . . . . . . . . . . 13
⊢ ((3
∈ ℤ ∧ 𝑁
∈ ℤ ∧ 3 ≤ 𝑁) → (1 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ ∧
1 ≤ (𝑁 −
1))) |
41 | | eluz2 12774 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈
(ℤ≥‘3) ↔ (3 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 3 ≤
𝑁)) |
42 | | eluz2 12774 |
. . . . . . . . . . . . 13
⊢ ((𝑁 − 1) ∈
(ℤ≥‘1) ↔ (1 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ ∧
1 ≤ (𝑁 −
1))) |
43 | 40, 41, 42 | 3imtr4i 292 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − 1) ∈
(ℤ≥‘1)) |
44 | | eluzfz1 13454 |
. . . . . . . . . . . 12
⊢ ((𝑁 − 1) ∈
(ℤ≥‘1) → 1 ∈ (1...(𝑁 − 1))) |
45 | 43, 44 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘3) → 1 ∈ (1...(𝑁 − 1))) |
46 | 45 | adantr 482 |
. . . . . . . . . 10
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑖 ∈ (2...(𝑁 − 1))) → 1 ∈ (1...(𝑁 − 1))) |
47 | | eqeq1 2737 |
. . . . . . . . . . . 12
⊢ (𝑘 = 1 → (𝑘 = 1 ↔ 1 = 1)) |
48 | | oveq1 7365 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 1 → (𝑘 + 1) = (1 + 1)) |
49 | 48 | opeq1d 4837 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 1 → ⟨(𝑘 + 1), 1⟩ = ⟨(1 + 1),
1⟩) |
50 | 49 | sneqd 4599 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 1 → {⟨(𝑘 + 1), 1⟩} = {⟨(1 +
1), 1⟩}) |
51 | 48 | sneqd 4599 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 1 → {(𝑘 + 1)} = {(1 + 1)}) |
52 | 51 | difeq2d 4083 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 1 → ((1...𝑁) ∖ {(𝑘 + 1)}) = ((1...𝑁) ∖ {(1 + 1)})) |
53 | 52 | xpeq1d 5663 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 1 → (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}) = (((1...𝑁) ∖ {(1 + 1)}) ×
{0})) |
54 | 50, 53 | uneq12d 4125 |
. . . . . . . . . . . 12
⊢ (𝑘 = 1 → ({⟨(𝑘 + 1), 1⟩} ∪
(((1...𝑁) ∖ {(𝑘 + 1)}) × {0})) =
({⟨(1 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(1 + 1)}) ×
{0}))) |
55 | 47, 54 | ifbieq2d 4513 |
. . . . . . . . . . 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 5389 |
. . . . . . . . . . . . 13
⊢ {⟨3,
-1⟩} ∈ V |
57 | | ovex 7391 |
. . . . . . . . . . . . . . 15
⊢
(1...𝑁) ∈
V |
58 | 57 | difexi 5286 |
. . . . . . . . . . . . . 14
⊢
((1...𝑁) ∖
{3}) ∈ V |
59 | | snex 5389 |
. . . . . . . . . . . . . 14
⊢ {0}
∈ V |
60 | 58, 59 | xpex 7688 |
. . . . . . . . . . . . 13
⊢
(((1...𝑁) ∖
{3}) × {0}) ∈ V |
61 | 56, 60 | unex 7681 |
. . . . . . . . . . . 12
⊢
({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})) ∈
V |
62 | | snex 5389 |
. . . . . . . . . . . . 13
⊢ {⟨(1
+ 1), 1⟩} ∈ V |
63 | 57 | difexi 5286 |
. . . . . . . . . . . . . 14
⊢
((1...𝑁) ∖ {(1
+ 1)}) ∈ V |
64 | 63, 59 | xpex 7688 |
. . . . . . . . . . . . 13
⊢
(((1...𝑁) ∖
{(1 + 1)}) × {0}) ∈ V |
65 | 62, 64 | unex 7681 |
. . . . . . . . . . . 12
⊢
({⟨(1 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(1 + 1)}) × {0})) ∈
V |
66 | 61, 65 | ifex 4537 |
. . . . . . . . . . 11
⊢ if(1 = 1,
({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(1 +
1), 1⟩} ∪ (((1...𝑁) ∖ {(1 + 1)}) × {0}))) ∈
V |
67 | 55, 10, 66 | fvmpt 6949 |
. . . . . . . . . 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 2733 |
. . . . . . . . . 10
⊢ 1 =
1 |
70 | 69 | iftruei 4494 |
. . . . . . . . 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 2789 |
. . . . . . . 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 4837 |
. . . . . . 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 12824 |
. . . . . . . . . . . . 13
⊢ 2 ∈
(ℤ≥‘1) |
74 | | fzss1 13486 |
. . . . . . . . . . . . 13
⊢ (2 ∈
(ℤ≥‘1) → (2...(𝑁 − 1)) ⊆ (1...(𝑁 − 1))) |
75 | 73, 74 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
(2...(𝑁 − 1))
⊆ (1...(𝑁 −
1)) |
76 | 75 | sseli 3941 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ (2...(𝑁 − 1)) → 𝑖 ∈ (1...(𝑁 − 1))) |
77 | 76 | adantl 483 |
. . . . . . . . . 10
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑖 ∈ (2...(𝑁 − 1))) → 𝑖 ∈ (1...(𝑁 − 1))) |
78 | | eqeq1 2737 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑖 → (𝑘 = 1 ↔ 𝑖 = 1)) |
79 | | oveq1 7365 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑖 → (𝑘 + 1) = (𝑖 + 1)) |
80 | 79 | opeq1d 4837 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑖 → ⟨(𝑘 + 1), 1⟩ = ⟨(𝑖 + 1), 1⟩) |
81 | 80 | sneqd 4599 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑖 → {⟨(𝑘 + 1), 1⟩} = {⟨(𝑖 + 1), 1⟩}) |
82 | 79 | sneqd 4599 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑖 → {(𝑘 + 1)} = {(𝑖 + 1)}) |
83 | 82 | difeq2d 4083 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑖 → ((1...𝑁) ∖ {(𝑘 + 1)}) = ((1...𝑁) ∖ {(𝑖 + 1)})) |
84 | 83 | xpeq1d 5663 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑖 → (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}) = (((1...𝑁) ∖ {(𝑖 + 1)}) × {0})) |
85 | 81, 84 | uneq12d 4125 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑖 → ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})) = ({⟨(𝑖 + 1), 1⟩} ∪
(((1...𝑁) ∖ {(𝑖 + 1)}) ×
{0}))) |
86 | 78, 85 | ifbieq2d 4513 |
. . . . . . . . . . 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 5389 |
. . . . . . . . . . . . 13
⊢
{⟨(𝑖 + 1),
1⟩} ∈ V |
88 | 57 | difexi 5286 |
. . . . . . . . . . . . . 14
⊢
((1...𝑁) ∖
{(𝑖 + 1)}) ∈
V |
89 | 88, 59 | xpex 7688 |
. . . . . . . . . . . . 13
⊢
(((1...𝑁) ∖
{(𝑖 + 1)}) × {0})
∈ V |
90 | 87, 89 | unex 7681 |
. . . . . . . . . . . 12
⊢
({⟨(𝑖 + 1),
1⟩} ∪ (((1...𝑁)
∖ {(𝑖 + 1)}) ×
{0})) ∈ V |
91 | 61, 90 | ifex 4537 |
. . . . . . . . . . 11
⊢ if(𝑖 = 1, ({⟨3, -1⟩} ∪
(((1...𝑁) ∖ {3})
× {0})), ({⟨(𝑖 +
1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0}))) ∈
V |
92 | 86, 10, 91 | fvmpt 6949 |
. . . . . . . . . 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 12329 |
. . . . . . . . . . . . . . . 16
⊢ 1 <
2 |
95 | 5, 24 | ltnlei 11281 |
. . . . . . . . . . . . . . . 16
⊢ (1 < 2
↔ ¬ 2 ≤ 1) |
96 | 94, 95 | mpbi 229 |
. . . . . . . . . . . . . . 15
⊢ ¬ 2
≤ 1 |
97 | 96 | intnanr 489 |
. . . . . . . . . . . . . 14
⊢ ¬ (2
≤ 1 ∧ 1 ≤ (𝑁
− 1)) |
98 | | 1z 12538 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℤ |
99 | | 2z 12540 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℤ |
100 | | eluzelz 12778 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈ ℤ) |
101 | 100, 21 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − 1) ∈ ℤ) |
102 | | elfz 13436 |
. . . . . . . . . . . . . . 15
⊢ ((1
∈ ℤ ∧ 2 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) → (1 ∈
(2...(𝑁 − 1)) ↔
(2 ≤ 1 ∧ 1 ≤ (𝑁
− 1)))) |
103 | 98, 99, 101, 102 | mp3an12i 1466 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘3) → (1 ∈ (2...(𝑁 − 1)) ↔ (2 ≤ 1 ∧ 1 ≤
(𝑁 −
1)))) |
104 | 97, 103 | mtbiri 327 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈
(ℤ≥‘3) → ¬ 1 ∈ (2...(𝑁 − 1))) |
105 | | eleq1 2822 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 1 → (𝑖 ∈ (2...(𝑁 − 1)) ↔ 1 ∈ (2...(𝑁 − 1)))) |
106 | 105 | notbid 318 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 1 → (¬ 𝑖 ∈ (2...(𝑁 − 1)) ↔ ¬ 1 ∈
(2...(𝑁 −
1)))) |
107 | 104, 106 | syl5ibrcom 247 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑖 = 1 → ¬ 𝑖 ∈ (2...(𝑁 − 1)))) |
108 | 107 | con2d 134 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑖 ∈ (2...(𝑁 − 1)) → ¬ 𝑖 = 1)) |
109 | 108 | imp 408 |
. . . . . . . . . 10
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑖 ∈ (2...(𝑁 − 1))) → ¬ 𝑖 = 1) |
110 | 109 | iffalsed 4498 |
. . . . . . . . 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 2773 |
. . . . . . . 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 4837 |
. . . . . . 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 5119 |
. . . . . 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 4837 |
. . . . . . 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 4837 |
. . . . . . 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 5119 |
. . . . . 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 2789 |
. . . . . . . . 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 4837 |
. . . . . . . 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 482 |
. . . . . . 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 4837 |
. . . . . . 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 5119 |
. . . . . 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 1437 |
. . . . 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 1343 |
. . . 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 3140 |
. . 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 27938 |
. . . 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 4832 |
. . . . . . . 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 4832 |
. . . . . . . 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 5119 |
. . . . . . 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 1441 |
. . . . . 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 3171 |
. . . . 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 5109 |
. . . . . . 7
⊢ (𝑥 = ({⟨1, 0⟩, ⟨2,
0⟩} ∪ ((3...𝑁)
× {0})) → (𝑥
Btwn ⟨𝑦, 𝑧⟩ ↔ ({⟨1,
0⟩, ⟨2, 0⟩} ∪ ((3...𝑁) × {0})) Btwn ⟨𝑦, 𝑧⟩)) |
134 | | opeq2 4832 |
. . . . . . . 8
⊢ (𝑥 = ({⟨1, 0⟩, ⟨2,
0⟩} ∪ ((3...𝑁)
× {0})) → ⟨𝑧, 𝑥⟩ = ⟨𝑧, ({⟨1, 0⟩, ⟨2, 0⟩} ∪
((3...𝑁) ×
{0}))⟩) |
135 | 134 | breq2d 5118 |
. . . . . . 7
⊢ (𝑥 = ({⟨1, 0⟩, ⟨2,
0⟩} ∪ ((3...𝑁)
× {0})) → (𝑦
Btwn ⟨𝑧, 𝑥⟩ ↔ 𝑦 Btwn ⟨𝑧, ({⟨1, 0⟩, ⟨2, 0⟩} ∪
((3...𝑁) ×
{0}))⟩)) |
136 | | opeq1 4831 |
. . . . . . . 8
⊢ (𝑥 = ({⟨1, 0⟩, ⟨2,
0⟩} ∪ ((3...𝑁)
× {0})) → ⟨𝑥, 𝑦⟩ = ⟨({⟨1, 0⟩, ⟨2,
0⟩} ∪ ((3...𝑁)
× {0})), 𝑦⟩) |
137 | 136 | breq2d 5118 |
. . . . . . 7
⊢ (𝑥 = ({⟨1, 0⟩, ⟨2,
0⟩} ∪ ((3...𝑁)
× {0})) → (𝑧
Btwn ⟨𝑥, 𝑦⟩ ↔ 𝑧 Btwn ⟨({⟨1, 0⟩, ⟨2,
0⟩} ∪ ((3...𝑁)
× {0})), 𝑦⟩)) |
138 | 133, 135,
137 | 3orbi123d 1436 |
. . . . . 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 318 |
. . . . 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 1440 |
. . . 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 4832 |
. . . . . . . 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 4832 |
. . . . . . . 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 5119 |
. . . . . . 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 1442 |
. . . . . 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 3171 |
. . . . 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 4831 |
. . . . . . . 8
⊢ (𝑦 = ({⟨1, 1⟩, ⟨2,
0⟩} ∪ ((3...𝑁)
× {0})) → ⟨𝑦, 𝑧⟩ = ⟨({⟨1, 1⟩, ⟨2,
0⟩} ∪ ((3...𝑁)
× {0})), 𝑧⟩) |
147 | 146 | breq2d 5118 |
. . . . . . 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 5109 |
. . . . . . 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 4832 |
. . . . . . . 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 5118 |
. . . . . . 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 1436 |
. . . . . 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 318 |
. . . . 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 1440 |
. . . 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 4832 |
. . . . . . . 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 4832 |
. . . . . . . 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 5119 |
. . . . . . 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 1443 |
. . . . . 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 3171 |
. . . . 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 4832 |
. . . . . . . 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 5118 |
. . . . . . 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 4831 |
. . . . . . . 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 5118 |
. . . . . . 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 5109 |
. . . . . . 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 1436 |
. . . . . 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 318 |
. . . . 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 1440 |
. . . 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 3593 |
. . 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 1386 |
. 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 7391 |
. . . 4
⊢
(1...(𝑁 − 1))
∈ V |
170 | 169 | mptex 7174 |
. . 3
⊢ (𝑘 ∈ (1...(𝑁 − 1)) ↦ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})),
({⟨(𝑘 + 1), 1⟩}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) × {0}))))
∈ V |
171 | | f1eq1 6734 |
. . . . . 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 6842 |
. . . . . . . . . 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 4837 |
. . . . . . . . 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 6842 |
. . . . . . . . . 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 4837 |
. . . . . . . . 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 5119 |
. . . . . . . 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 4837 |
. . . . . . . . 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 4837 |
. . . . . . . . 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 5119 |
. . . . . . . 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 4837 |
. . . . . . . . 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 4837 |
. . . . . . . . 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 5119 |
. . . . . . . 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 1437 |
. . . . . . 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 3171 |
. . . . . 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 1438 |
. . . . 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 3172 |
. . . 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 3210 |
. . 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 3564 |
. 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 ⟨𝑥, 𝑦⟩))) |