Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . . . . 6
⊢
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})) = ({〈3,
-1〉} ∪ (((1...𝑁)
∖ {3}) × {0})) |
2 | 1 | axlowdimlem7 27039 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘3) → ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0}))
∈ (𝔼‘𝑁)) |
3 | 2 | adantr 484 |
. . . 4
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑖 ∈ (1...(𝑁 − 1))) → ({〈3, -1〉}
∪ (((1...𝑁) ∖
{3}) × {0})) ∈ (𝔼‘𝑁)) |
4 | | eluzge3nn 12486 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈ ℕ) |
5 | | eqid 2737 |
. . . . . 6
⊢
({〈(𝑖 + 1),
1〉} ∪ (((1...𝑁)
∖ {(𝑖 + 1)}) ×
{0})) = ({〈(𝑖 + 1),
1〉} ∪ (((1...𝑁)
∖ {(𝑖 + 1)}) ×
{0})) |
6 | 5 | axlowdimlem10 27042 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑖 ∈ (1...(𝑁 − 1))) → ({〈(𝑖 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑖 + 1)}) × {0})) ∈
(𝔼‘𝑁)) |
7 | 4, 6 | sylan 583 |
. . . 4
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑖 ∈ (1...(𝑁 − 1))) → ({〈(𝑖 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑖 + 1)}) × {0})) ∈
(𝔼‘𝑁)) |
8 | 3, 7 | ifcld 4485 |
. . 3
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑖 ∈ (1...(𝑁 − 1))) → if(𝑖 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑖 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑖 + 1)}) × {0})))
∈ (𝔼‘𝑁)) |
9 | | axlowdimlem15.1 |
. . 3
⊢ 𝐹 = (𝑖 ∈ (1...(𝑁 − 1)) ↦ if(𝑖 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑖 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑖 + 1)}) ×
{0})))) |
10 | 8, 9 | fmptd 6931 |
. 2
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝐹:(1...(𝑁 − 1))⟶(𝔼‘𝑁)) |
11 | | eqeq1 2741 |
. . . . . . . 8
⊢ (𝑖 = 𝑗 → (𝑖 = 1 ↔ 𝑗 = 1)) |
12 | | oveq1 7220 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑗 → (𝑖 + 1) = (𝑗 + 1)) |
13 | 12 | opeq1d 4790 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑗 → 〈(𝑖 + 1), 1〉 = 〈(𝑗 + 1), 1〉) |
14 | 13 | sneqd 4553 |
. . . . . . . . 9
⊢ (𝑖 = 𝑗 → {〈(𝑖 + 1), 1〉} = {〈(𝑗 + 1), 1〉}) |
15 | 12 | sneqd 4553 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑗 → {(𝑖 + 1)} = {(𝑗 + 1)}) |
16 | 15 | difeq2d 4037 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑗 → ((1...𝑁) ∖ {(𝑖 + 1)}) = ((1...𝑁) ∖ {(𝑗 + 1)})) |
17 | 16 | xpeq1d 5580 |
. . . . . . . . 9
⊢ (𝑖 = 𝑗 → (((1...𝑁) ∖ {(𝑖 + 1)}) × {0}) = (((1...𝑁) ∖ {(𝑗 + 1)}) × {0})) |
18 | 14, 17 | uneq12d 4078 |
. . . . . . . 8
⊢ (𝑖 = 𝑗 → ({〈(𝑖 + 1), 1〉} ∪ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0})) = ({〈(𝑗 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑗 + 1)}) ×
{0}))) |
19 | 11, 18 | ifbieq2d 4465 |
. . . . . . 7
⊢ (𝑖 = 𝑗 → if(𝑖 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑖 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑖 + 1)}) × {0}))) =
if(𝑗 = 1, ({〈3,
-1〉} ∪ (((1...𝑁)
∖ {3}) × {0})), ({〈(𝑗 + 1), 1〉} ∪ (((1...𝑁) ∖ {(𝑗 + 1)}) × {0})))) |
20 | | snex 5324 |
. . . . . . . . 9
⊢ {〈3,
-1〉} ∈ V |
21 | | ovex 7246 |
. . . . . . . . . . 11
⊢
(1...𝑁) ∈
V |
22 | 21 | difexi 5221 |
. . . . . . . . . 10
⊢
((1...𝑁) ∖
{3}) ∈ V |
23 | | snex 5324 |
. . . . . . . . . 10
⊢ {0}
∈ V |
24 | 22, 23 | xpex 7538 |
. . . . . . . . 9
⊢
(((1...𝑁) ∖
{3}) × {0}) ∈ V |
25 | 20, 24 | unex 7531 |
. . . . . . . 8
⊢
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})) ∈
V |
26 | | snex 5324 |
. . . . . . . . 9
⊢
{〈(𝑗 + 1),
1〉} ∈ V |
27 | 21 | difexi 5221 |
. . . . . . . . . 10
⊢
((1...𝑁) ∖
{(𝑗 + 1)}) ∈
V |
28 | 27, 23 | xpex 7538 |
. . . . . . . . 9
⊢
(((1...𝑁) ∖
{(𝑗 + 1)}) × {0})
∈ V |
29 | 26, 28 | unex 7531 |
. . . . . . . 8
⊢
({〈(𝑗 + 1),
1〉} ∪ (((1...𝑁)
∖ {(𝑗 + 1)}) ×
{0})) ∈ V |
30 | 25, 29 | ifex 4489 |
. . . . . . 7
⊢ if(𝑗 = 1, ({〈3, -1〉} ∪
(((1...𝑁) ∖ {3})
× {0})), ({〈(𝑗 +
1), 1〉} ∪ (((1...𝑁) ∖ {(𝑗 + 1)}) × {0}))) ∈
V |
31 | 19, 9, 30 | fvmpt 6818 |
. . . . . 6
⊢ (𝑗 ∈ (1...(𝑁 − 1)) → (𝐹‘𝑗) = if(𝑗 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑗 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑗 + 1)}) ×
{0})))) |
32 | | eqeq1 2741 |
. . . . . . . 8
⊢ (𝑖 = 𝑘 → (𝑖 = 1 ↔ 𝑘 = 1)) |
33 | | oveq1 7220 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑘 → (𝑖 + 1) = (𝑘 + 1)) |
34 | 33 | opeq1d 4790 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑘 → 〈(𝑖 + 1), 1〉 = 〈(𝑘 + 1), 1〉) |
35 | 34 | sneqd 4553 |
. . . . . . . . 9
⊢ (𝑖 = 𝑘 → {〈(𝑖 + 1), 1〉} = {〈(𝑘 + 1), 1〉}) |
36 | 33 | sneqd 4553 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑘 → {(𝑖 + 1)} = {(𝑘 + 1)}) |
37 | 36 | difeq2d 4037 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑘 → ((1...𝑁) ∖ {(𝑖 + 1)}) = ((1...𝑁) ∖ {(𝑘 + 1)})) |
38 | 37 | xpeq1d 5580 |
. . . . . . . . 9
⊢ (𝑖 = 𝑘 → (((1...𝑁) ∖ {(𝑖 + 1)}) × {0}) = (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})) |
39 | 35, 38 | uneq12d 4078 |
. . . . . . . 8
⊢ (𝑖 = 𝑘 → ({〈(𝑖 + 1), 1〉} ∪ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0})) = ({〈(𝑘 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑘 + 1)}) ×
{0}))) |
40 | 32, 39 | ifbieq2d 4465 |
. . . . . . 7
⊢ (𝑖 = 𝑘 → if(𝑖 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑖 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑖 + 1)}) × {0}))) =
if(𝑘 = 1, ({〈3,
-1〉} ∪ (((1...𝑁)
∖ {3}) × {0})), ({〈(𝑘 + 1), 1〉} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})))) |
41 | | snex 5324 |
. . . . . . . . 9
⊢
{〈(𝑘 + 1),
1〉} ∈ V |
42 | 21 | difexi 5221 |
. . . . . . . . . 10
⊢
((1...𝑁) ∖
{(𝑘 + 1)}) ∈
V |
43 | 42, 23 | xpex 7538 |
. . . . . . . . 9
⊢
(((1...𝑁) ∖
{(𝑘 + 1)}) × {0})
∈ V |
44 | 41, 43 | unex 7531 |
. . . . . . . 8
⊢
({〈(𝑘 + 1),
1〉} ∪ (((1...𝑁)
∖ {(𝑘 + 1)}) ×
{0})) ∈ V |
45 | 25, 44 | ifex 4489 |
. . . . . . 7
⊢ if(𝑘 = 1, ({〈3, -1〉} ∪
(((1...𝑁) ∖ {3})
× {0})), ({〈(𝑘 +
1), 1〉} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))) ∈
V |
46 | 40, 9, 45 | fvmpt 6818 |
. . . . . 6
⊢ (𝑘 ∈ (1...(𝑁 − 1)) → (𝐹‘𝑘) = if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0})))) |
47 | 31, 46 | eqeqan12d 2751 |
. . . . 5
⊢ ((𝑗 ∈ (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}))))) |
48 | 47 | adantl 485 |
. . . 4
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑗 ∈ (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}))))) |
49 | | eqtr3 2763 |
. . . . . 6
⊢ ((𝑗 = 1 ∧ 𝑘 = 1) → 𝑗 = 𝑘) |
50 | 49 | 2a1d 26 |
. . . . 5
⊢ ((𝑗 = 1 ∧ 𝑘 = 1) → ((𝑁 ∈ (ℤ≥‘3)
∧ (𝑗 ∈ (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}))) → 𝑗 = 𝑘))) |
51 | | eqid 2737 |
. . . . . . . . . . 11
⊢
({〈(𝑘 + 1),
1〉} ∪ (((1...𝑁)
∖ {(𝑘 + 1)}) ×
{0})) = ({〈(𝑘 + 1),
1〉} ∪ (((1...𝑁)
∖ {(𝑘 + 1)}) ×
{0})) |
52 | 1, 51 | axlowdimlem13 27045 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...(𝑁 − 1))) → ({〈3, -1〉}
∪ (((1...𝑁) ∖
{3}) × {0})) ≠ ({〈(𝑘 + 1), 1〉} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))) |
53 | 52 | neneqd 2945 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...(𝑁 − 1))) → ¬ ({〈3,
-1〉} ∪ (((1...𝑁)
∖ {3}) × {0})) = ({〈(𝑘 + 1), 1〉} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))) |
54 | 53 | pm2.21d 121 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...(𝑁 − 1))) → (({〈3, -1〉}
∪ (((1...𝑁) ∖
{3}) × {0})) = ({〈(𝑘 + 1), 1〉} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})) → 𝑗 = 𝑘)) |
55 | 54 | adantrl 716 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝑗 ∈ (1...(𝑁 − 1)) ∧ 𝑘 ∈ (1...(𝑁 − 1)))) → (({〈3, -1〉}
∪ (((1...𝑁) ∖
{3}) × {0})) = ({〈(𝑘 + 1), 1〉} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})) → 𝑗 = 𝑘)) |
56 | 4, 55 | sylan 583 |
. . . . . 6
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑗 ∈ (1...(𝑁 − 1)) ∧ 𝑘 ∈ (1...(𝑁 − 1)))) → (({〈3, -1〉}
∪ (((1...𝑁) ∖
{3}) × {0})) = ({〈(𝑘 + 1), 1〉} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})) → 𝑗 = 𝑘)) |
57 | | iftrue 4445 |
. . . . . . . 8
⊢ (𝑗 = 1 → if(𝑗 = 1, ({〈3, -1〉} ∪
(((1...𝑁) ∖ {3})
× {0})), ({〈(𝑗 +
1), 1〉} ∪ (((1...𝑁) ∖ {(𝑗 + 1)}) × {0}))) = ({〈3, -1〉}
∪ (((1...𝑁) ∖
{3}) × {0}))) |
58 | | iffalse 4448 |
. . . . . . . 8
⊢ (¬
𝑘 = 1 → if(𝑘 = 1, ({〈3, -1〉} ∪
(((1...𝑁) ∖ {3})
× {0})), ({〈(𝑘 +
1), 1〉} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))) = ({〈(𝑘 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑘 + 1)}) ×
{0}))) |
59 | 57, 58 | eqeqan12d 2751 |
. . . . . . 7
⊢ ((𝑗 = 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}))) ↔ ({〈3,
-1〉} ∪ (((1...𝑁)
∖ {3}) × {0})) = ({〈(𝑘 + 1), 1〉} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})))) |
60 | 59 | imbi1d 345 |
. . . . . 6
⊢ ((𝑗 = 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}))) → 𝑗 = 𝑘) ↔ (({〈3, -1〉} ∪
(((1...𝑁) ∖ {3})
× {0})) = ({〈(𝑘
+ 1), 1〉} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})) → 𝑗 = 𝑘))) |
61 | 56, 60 | syl5ibr 249 |
. . . . 5
⊢ ((𝑗 = 1 ∧ ¬ 𝑘 = 1) → ((𝑁 ∈ (ℤ≥‘3)
∧ (𝑗 ∈ (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}))) → 𝑗 = 𝑘))) |
62 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
({〈(𝑗 + 1),
1〉} ∪ (((1...𝑁)
∖ {(𝑗 + 1)}) ×
{0})) = ({〈(𝑗 + 1),
1〉} ∪ (((1...𝑁)
∖ {(𝑗 + 1)}) ×
{0})) |
63 | 1, 62 | axlowdimlem13 27045 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 − 1))) → ({〈3, -1〉}
∪ (((1...𝑁) ∖
{3}) × {0})) ≠ ({〈(𝑗 + 1), 1〉} ∪ (((1...𝑁) ∖ {(𝑗 + 1)}) × {0}))) |
64 | 63 | necomd 2996 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 − 1))) → ({〈(𝑗 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑗 + 1)}) × {0})) ≠
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) ×
{0}))) |
65 | 64 | neneqd 2945 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 − 1))) → ¬ ({〈(𝑗 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑗 + 1)}) × {0})) =
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) ×
{0}))) |
66 | 65 | pm2.21d 121 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 − 1))) → (({〈(𝑗 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑗 + 1)}) × {0})) =
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})) → 𝑗 = 𝑘)) |
67 | 4, 66 | sylan 583 |
. . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑗 ∈ (1...(𝑁 − 1))) → (({〈(𝑗 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑗 + 1)}) × {0})) =
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})) → 𝑗 = 𝑘)) |
68 | 67 | adantrr 717 |
. . . . . 6
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑗 ∈ (1...(𝑁 − 1)) ∧ 𝑘 ∈ (1...(𝑁 − 1)))) → (({〈(𝑗 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑗 + 1)}) × {0})) =
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})) → 𝑗 = 𝑘)) |
69 | | iffalse 4448 |
. . . . . . . 8
⊢ (¬
𝑗 = 1 → if(𝑗 = 1, ({〈3, -1〉} ∪
(((1...𝑁) ∖ {3})
× {0})), ({〈(𝑗 +
1), 1〉} ∪ (((1...𝑁) ∖ {(𝑗 + 1)}) × {0}))) = ({〈(𝑗 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑗 + 1)}) ×
{0}))) |
70 | | iftrue 4445 |
. . . . . . . 8
⊢ (𝑘 = 1 → if(𝑘 = 1, ({〈3, -1〉} ∪
(((1...𝑁) ∖ {3})
× {0})), ({〈(𝑘 +
1), 1〉} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))) = ({〈3, -1〉}
∪ (((1...𝑁) ∖
{3}) × {0}))) |
71 | 69, 70 | eqeqan12d 2751 |
. . . . . . 7
⊢ ((¬
𝑗 = 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}))) ↔ ({〈(𝑗 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑗 + 1)}) × {0})) =
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) ×
{0})))) |
72 | 71 | imbi1d 345 |
. . . . . 6
⊢ ((¬
𝑗 = 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}))) → 𝑗 = 𝑘) ↔ (({〈(𝑗 + 1), 1〉} ∪ (((1...𝑁) ∖ {(𝑗 + 1)}) × {0})) = ({〈3, -1〉}
∪ (((1...𝑁) ∖
{3}) × {0})) → 𝑗
= 𝑘))) |
73 | 68, 72 | syl5ibr 249 |
. . . . 5
⊢ ((¬
𝑗 = 1 ∧ 𝑘 = 1) → ((𝑁 ∈ (ℤ≥‘3)
∧ (𝑗 ∈ (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}))) → 𝑗 = 𝑘))) |
74 | 62, 51 | axlowdimlem14 27046 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 − 1)) ∧ 𝑘 ∈ (1...(𝑁 − 1))) → (({〈(𝑗 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑗 + 1)}) × {0})) =
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) × {0}))
→ 𝑗 = 𝑘)) |
75 | 74 | 3expb 1122 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝑗 ∈ (1...(𝑁 − 1)) ∧ 𝑘 ∈ (1...(𝑁 − 1)))) → (({〈(𝑗 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑗 + 1)}) × {0})) =
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) × {0}))
→ 𝑗 = 𝑘)) |
76 | 4, 75 | sylan 583 |
. . . . . 6
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑗 ∈ (1...(𝑁 − 1)) ∧ 𝑘 ∈ (1...(𝑁 − 1)))) → (({〈(𝑗 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑗 + 1)}) × {0})) =
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) × {0}))
→ 𝑗 = 𝑘)) |
77 | 69, 58 | eqeqan12d 2751 |
. . . . . . 7
⊢ ((¬
𝑗 = 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}))) ↔ ({〈(𝑗 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑗 + 1)}) × {0})) =
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0})))) |
78 | 77 | imbi1d 345 |
. . . . . 6
⊢ ((¬
𝑗 = 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}))) → 𝑗 = 𝑘) ↔ (({〈(𝑗 + 1), 1〉} ∪ (((1...𝑁) ∖ {(𝑗 + 1)}) × {0})) = ({〈(𝑘 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑘 + 1)}) × {0})) →
𝑗 = 𝑘))) |
79 | 76, 78 | syl5ibr 249 |
. . . . 5
⊢ ((¬
𝑗 = 1 ∧ ¬ 𝑘 = 1) → ((𝑁 ∈ (ℤ≥‘3)
∧ (𝑗 ∈ (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}))) → 𝑗 = 𝑘))) |
80 | 50, 61, 73, 79 | 4cases 1041 |
. . . 4
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑗 ∈ (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}))) → 𝑗 = 𝑘)) |
81 | 48, 80 | sylbid 243 |
. . 3
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑗 ∈ (1...(𝑁 − 1)) ∧ 𝑘 ∈ (1...(𝑁 − 1)))) → ((𝐹‘𝑗) = (𝐹‘𝑘) → 𝑗 = 𝑘)) |
82 | 81 | ralrimivva 3112 |
. 2
⊢ (𝑁 ∈
(ℤ≥‘3) → ∀𝑗 ∈ (1...(𝑁 − 1))∀𝑘 ∈ (1...(𝑁 − 1))((𝐹‘𝑗) = (𝐹‘𝑘) → 𝑗 = 𝑘)) |
83 | | dff13 7067 |
. 2
⊢ (𝐹:(1...(𝑁 − 1))–1-1→(𝔼‘𝑁) ↔ (𝐹:(1...(𝑁 − 1))⟶(𝔼‘𝑁) ∧ ∀𝑗 ∈ (1...(𝑁 − 1))∀𝑘 ∈ (1...(𝑁 − 1))((𝐹‘𝑗) = (𝐹‘𝑘) → 𝑗 = 𝑘))) |
84 | 10, 82, 83 | sylanbrc 586 |
1
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝐹:(1...(𝑁 − 1))–1-1→(𝔼‘𝑁)) |