Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . . . . 6
⊢
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})) = ({〈3,
-1〉} ∪ (((1...𝑁)
∖ {3}) × {0})) |
2 | 1 | axlowdimlem7 25828 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘3) → ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0}))
∈ (𝔼‘𝑁)) |
3 | 2 | adantr 481 |
. . . 4
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑖 ∈ (1...(𝑁 − 1))) → ({〈3, -1〉}
∪ (((1...𝑁) ∖
{3}) × {0})) ∈ (𝔼‘𝑁)) |
4 | | eluzge3nn 11730 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈ ℕ) |
5 | | eqid 2622 |
. . . . . 6
⊢
({〈(𝑖 + 1),
1〉} ∪ (((1...𝑁)
∖ {(𝑖 + 1)}) ×
{0})) = ({〈(𝑖 + 1),
1〉} ∪ (((1...𝑁)
∖ {(𝑖 + 1)}) ×
{0})) |
6 | 5 | axlowdimlem10 25831 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑖 ∈ (1...(𝑁 − 1))) → ({〈(𝑖 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑖 + 1)}) × {0})) ∈
(𝔼‘𝑁)) |
7 | 4, 6 | sylan 488 |
. . . 4
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑖 ∈ (1...(𝑁 − 1))) → ({〈(𝑖 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑖 + 1)}) × {0})) ∈
(𝔼‘𝑁)) |
8 | 3, 7 | ifcld 4131 |
. . 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 6385 |
. 2
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝐹:(1...(𝑁 − 1))⟶(𝔼‘𝑁)) |
11 | | eqeq1 2626 |
. . . . . . . 8
⊢ (𝑖 = 𝑗 → (𝑖 = 1 ↔ 𝑗 = 1)) |
12 | | oveq1 6657 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑗 → (𝑖 + 1) = (𝑗 + 1)) |
13 | 12 | opeq1d 4408 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑗 → 〈(𝑖 + 1), 1〉 = 〈(𝑗 + 1), 1〉) |
14 | 13 | sneqd 4189 |
. . . . . . . . 9
⊢ (𝑖 = 𝑗 → {〈(𝑖 + 1), 1〉} = {〈(𝑗 + 1), 1〉}) |
15 | 12 | sneqd 4189 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑗 → {(𝑖 + 1)} = {(𝑗 + 1)}) |
16 | 15 | difeq2d 3728 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑗 → ((1...𝑁) ∖ {(𝑖 + 1)}) = ((1...𝑁) ∖ {(𝑗 + 1)})) |
17 | 16 | xpeq1d 5138 |
. . . . . . . . 9
⊢ (𝑖 = 𝑗 → (((1...𝑁) ∖ {(𝑖 + 1)}) × {0}) = (((1...𝑁) ∖ {(𝑗 + 1)}) × {0})) |
18 | 14, 17 | uneq12d 3768 |
. . . . . . . 8
⊢ (𝑖 = 𝑗 → ({〈(𝑖 + 1), 1〉} ∪ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0})) = ({〈(𝑗 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑗 + 1)}) ×
{0}))) |
19 | 11, 18 | ifbieq2d 4111 |
. . . . . . 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 4908 |
. . . . . . . . 9
⊢ {〈3,
-1〉} ∈ V |
21 | | ovex 6678 |
. . . . . . . . . . 11
⊢
(1...𝑁) ∈
V |
22 | | difexg 4808 |
. . . . . . . . . . 11
⊢
((1...𝑁) ∈ V
→ ((1...𝑁) ∖
{3}) ∈ V) |
23 | 21, 22 | ax-mp 5 |
. . . . . . . . . 10
⊢
((1...𝑁) ∖
{3}) ∈ V |
24 | | snex 4908 |
. . . . . . . . . 10
⊢ {0}
∈ V |
25 | 23, 24 | xpex 6962 |
. . . . . . . . 9
⊢
(((1...𝑁) ∖
{3}) × {0}) ∈ V |
26 | 20, 25 | unex 6956 |
. . . . . . . 8
⊢
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})) ∈
V |
27 | | snex 4908 |
. . . . . . . . 9
⊢
{〈(𝑗 + 1),
1〉} ∈ V |
28 | | difexg 4808 |
. . . . . . . . . . 11
⊢
((1...𝑁) ∈ V
→ ((1...𝑁) ∖
{(𝑗 + 1)}) ∈
V) |
29 | 21, 28 | ax-mp 5 |
. . . . . . . . . 10
⊢
((1...𝑁) ∖
{(𝑗 + 1)}) ∈
V |
30 | 29, 24 | xpex 6962 |
. . . . . . . . 9
⊢
(((1...𝑁) ∖
{(𝑗 + 1)}) × {0})
∈ V |
31 | 27, 30 | unex 6956 |
. . . . . . . 8
⊢
({〈(𝑗 + 1),
1〉} ∪ (((1...𝑁)
∖ {(𝑗 + 1)}) ×
{0})) ∈ V |
32 | 26, 31 | ifex 4156 |
. . . . . . 7
⊢ if(𝑗 = 1, ({〈3, -1〉} ∪
(((1...𝑁) ∖ {3})
× {0})), ({〈(𝑗 +
1), 1〉} ∪ (((1...𝑁) ∖ {(𝑗 + 1)}) × {0}))) ∈
V |
33 | 19, 9, 32 | fvmpt 6282 |
. . . . . 6
⊢ (𝑗 ∈ (1...(𝑁 − 1)) → (𝐹‘𝑗) = if(𝑗 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑗 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑗 + 1)}) ×
{0})))) |
34 | | eqeq1 2626 |
. . . . . . . 8
⊢ (𝑖 = 𝑘 → (𝑖 = 1 ↔ 𝑘 = 1)) |
35 | | oveq1 6657 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑘 → (𝑖 + 1) = (𝑘 + 1)) |
36 | 35 | opeq1d 4408 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑘 → 〈(𝑖 + 1), 1〉 = 〈(𝑘 + 1), 1〉) |
37 | 36 | sneqd 4189 |
. . . . . . . . 9
⊢ (𝑖 = 𝑘 → {〈(𝑖 + 1), 1〉} = {〈(𝑘 + 1), 1〉}) |
38 | 35 | sneqd 4189 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑘 → {(𝑖 + 1)} = {(𝑘 + 1)}) |
39 | 38 | difeq2d 3728 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑘 → ((1...𝑁) ∖ {(𝑖 + 1)}) = ((1...𝑁) ∖ {(𝑘 + 1)})) |
40 | 39 | xpeq1d 5138 |
. . . . . . . . 9
⊢ (𝑖 = 𝑘 → (((1...𝑁) ∖ {(𝑖 + 1)}) × {0}) = (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})) |
41 | 37, 40 | uneq12d 3768 |
. . . . . . . 8
⊢ (𝑖 = 𝑘 → ({〈(𝑖 + 1), 1〉} ∪ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0})) = ({〈(𝑘 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑘 + 1)}) ×
{0}))) |
42 | 34, 41 | ifbieq2d 4111 |
. . . . . . 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})))) |
43 | | snex 4908 |
. . . . . . . . 9
⊢
{〈(𝑘 + 1),
1〉} ∈ V |
44 | | difexg 4808 |
. . . . . . . . . . 11
⊢
((1...𝑁) ∈ V
→ ((1...𝑁) ∖
{(𝑘 + 1)}) ∈
V) |
45 | 21, 44 | ax-mp 5 |
. . . . . . . . . 10
⊢
((1...𝑁) ∖
{(𝑘 + 1)}) ∈
V |
46 | 45, 24 | xpex 6962 |
. . . . . . . . 9
⊢
(((1...𝑁) ∖
{(𝑘 + 1)}) × {0})
∈ V |
47 | 43, 46 | unex 6956 |
. . . . . . . 8
⊢
({〈(𝑘 + 1),
1〉} ∪ (((1...𝑁)
∖ {(𝑘 + 1)}) ×
{0})) ∈ V |
48 | 26, 47 | ifex 4156 |
. . . . . . 7
⊢ if(𝑘 = 1, ({〈3, -1〉} ∪
(((1...𝑁) ∖ {3})
× {0})), ({〈(𝑘 +
1), 1〉} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))) ∈
V |
49 | 42, 9, 48 | fvmpt 6282 |
. . . . . 6
⊢ (𝑘 ∈ (1...(𝑁 − 1)) → (𝐹‘𝑘) = if(𝑘 = 1, ({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})),
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0})))) |
50 | 33, 49 | eqeqan12d 2638 |
. . . . 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}))))) |
51 | 50 | adantl 482 |
. . . 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}))))) |
52 | | eqtr3 2643 |
. . . . . 6
⊢ ((𝑗 = 1 ∧ 𝑘 = 1) → 𝑗 = 𝑘) |
53 | 52 | 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}))) → 𝑗 = 𝑘))) |
54 | | eqid 2622 |
. . . . . . . . . . 11
⊢
({〈(𝑘 + 1),
1〉} ∪ (((1...𝑁)
∖ {(𝑘 + 1)}) ×
{0})) = ({〈(𝑘 + 1),
1〉} ∪ (((1...𝑁)
∖ {(𝑘 + 1)}) ×
{0})) |
55 | 1, 54 | axlowdimlem13 25834 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...(𝑁 − 1))) → ({〈3, -1〉}
∪ (((1...𝑁) ∖
{3}) × {0})) ≠ ({〈(𝑘 + 1), 1〉} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))) |
56 | 55 | neneqd 2799 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...(𝑁 − 1))) → ¬ ({〈3,
-1〉} ∪ (((1...𝑁)
∖ {3}) × {0})) = ({〈(𝑘 + 1), 1〉} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))) |
57 | 56 | pm2.21d 118 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...(𝑁 − 1))) → (({〈3, -1〉}
∪ (((1...𝑁) ∖
{3}) × {0})) = ({〈(𝑘 + 1), 1〉} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})) → 𝑗 = 𝑘)) |
58 | 57 | adantrl 752 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝑗 ∈ (1...(𝑁 − 1)) ∧ 𝑘 ∈ (1...(𝑁 − 1)))) → (({〈3, -1〉}
∪ (((1...𝑁) ∖
{3}) × {0})) = ({〈(𝑘 + 1), 1〉} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})) → 𝑗 = 𝑘)) |
59 | 4, 58 | sylan 488 |
. . . . . 6
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑗 ∈ (1...(𝑁 − 1)) ∧ 𝑘 ∈ (1...(𝑁 − 1)))) → (({〈3, -1〉}
∪ (((1...𝑁) ∖
{3}) × {0})) = ({〈(𝑘 + 1), 1〉} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})) → 𝑗 = 𝑘)) |
60 | | iftrue 4092 |
. . . . . . . 8
⊢ (𝑗 = 1 → if(𝑗 = 1, ({〈3, -1〉} ∪
(((1...𝑁) ∖ {3})
× {0})), ({〈(𝑗 +
1), 1〉} ∪ (((1...𝑁) ∖ {(𝑗 + 1)}) × {0}))) = ({〈3, -1〉}
∪ (((1...𝑁) ∖
{3}) × {0}))) |
61 | | iffalse 4095 |
. . . . . . . 8
⊢ (¬
𝑘 = 1 → if(𝑘 = 1, ({〈3, -1〉} ∪
(((1...𝑁) ∖ {3})
× {0})), ({〈(𝑘 +
1), 1〉} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))) = ({〈(𝑘 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑘 + 1)}) ×
{0}))) |
62 | 60, 61 | eqeqan12d 2638 |
. . . . . . 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})))) |
63 | 62 | imbi1d 331 |
. . . . . 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})) → 𝑗 = 𝑘))) |
64 | 59, 63 | syl5ibr 236 |
. . . . 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}))) → 𝑗 = 𝑘))) |
65 | | eqid 2622 |
. . . . . . . . . . . 12
⊢
({〈(𝑗 + 1),
1〉} ∪ (((1...𝑁)
∖ {(𝑗 + 1)}) ×
{0})) = ({〈(𝑗 + 1),
1〉} ∪ (((1...𝑁)
∖ {(𝑗 + 1)}) ×
{0})) |
66 | 1, 65 | axlowdimlem13 25834 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 − 1))) → ({〈3, -1〉}
∪ (((1...𝑁) ∖
{3}) × {0})) ≠ ({〈(𝑗 + 1), 1〉} ∪ (((1...𝑁) ∖ {(𝑗 + 1)}) × {0}))) |
67 | 66 | necomd 2849 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 − 1))) → ({〈(𝑗 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑗 + 1)}) × {0})) ≠
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) ×
{0}))) |
68 | 67 | neneqd 2799 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 − 1))) → ¬ ({〈(𝑗 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑗 + 1)}) × {0})) =
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) ×
{0}))) |
69 | 68 | pm2.21d 118 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 − 1))) → (({〈(𝑗 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑗 + 1)}) × {0})) =
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})) → 𝑗 = 𝑘)) |
70 | 4, 69 | sylan 488 |
. . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑗 ∈ (1...(𝑁 − 1))) → (({〈(𝑗 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑗 + 1)}) × {0})) =
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})) → 𝑗 = 𝑘)) |
71 | 70 | adantrr 753 |
. . . . . 6
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑗 ∈ (1...(𝑁 − 1)) ∧ 𝑘 ∈ (1...(𝑁 − 1)))) → (({〈(𝑗 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑗 + 1)}) × {0})) =
({〈3, -1〉} ∪ (((1...𝑁) ∖ {3}) × {0})) → 𝑗 = 𝑘)) |
72 | | iffalse 4095 |
. . . . . . . 8
⊢ (¬
𝑗 = 1 → if(𝑗 = 1, ({〈3, -1〉} ∪
(((1...𝑁) ∖ {3})
× {0})), ({〈(𝑗 +
1), 1〉} ∪ (((1...𝑁) ∖ {(𝑗 + 1)}) × {0}))) = ({〈(𝑗 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑗 + 1)}) ×
{0}))) |
73 | | iftrue 4092 |
. . . . . . . 8
⊢ (𝑘 = 1 → if(𝑘 = 1, ({〈3, -1〉} ∪
(((1...𝑁) ∖ {3})
× {0})), ({〈(𝑘 +
1), 1〉} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))) = ({〈3, -1〉}
∪ (((1...𝑁) ∖
{3}) × {0}))) |
74 | 72, 73 | eqeqan12d 2638 |
. . . . . . 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})))) |
75 | 74 | imbi1d 331 |
. . . . . 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})) → 𝑗
= 𝑘))) |
76 | 71, 75 | syl5ibr 236 |
. . . . 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}))) → 𝑗 = 𝑘))) |
77 | 65, 54 | axlowdimlem14 25835 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 − 1)) ∧ 𝑘 ∈ (1...(𝑁 − 1))) → (({〈(𝑗 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑗 + 1)}) × {0})) =
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) × {0}))
→ 𝑗 = 𝑘)) |
78 | 77 | 3expb 1266 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝑗 ∈ (1...(𝑁 − 1)) ∧ 𝑘 ∈ (1...(𝑁 − 1)))) → (({〈(𝑗 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑗 + 1)}) × {0})) =
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) × {0}))
→ 𝑗 = 𝑘)) |
79 | 4, 78 | sylan 488 |
. . . . . 6
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑗 ∈ (1...(𝑁 − 1)) ∧ 𝑘 ∈ (1...(𝑁 − 1)))) → (({〈(𝑗 + 1), 1〉} ∪
(((1...𝑁) ∖ {(𝑗 + 1)}) × {0})) =
({〈(𝑘 + 1), 1〉}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) × {0}))
→ 𝑗 = 𝑘)) |
80 | 72, 61 | eqeqan12d 2638 |
. . . . . . 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})))) |
81 | 80 | imbi1d 331 |
. . . . . 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})) →
𝑗 = 𝑘))) |
82 | 79, 81 | syl5ibr 236 |
. . . . 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}))) → 𝑗 = 𝑘))) |
83 | 53, 64, 76, 82 | 4cases 990 |
. . . 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}))) → 𝑗 = 𝑘)) |
84 | 51, 83 | sylbid 230 |
. . 3
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑗 ∈ (1...(𝑁 − 1)) ∧ 𝑘 ∈ (1...(𝑁 − 1)))) → ((𝐹‘𝑗) = (𝐹‘𝑘) → 𝑗 = 𝑘)) |
85 | 84 | ralrimivva 2971 |
. 2
⊢ (𝑁 ∈
(ℤ≥‘3) → ∀𝑗 ∈ (1...(𝑁 − 1))∀𝑘 ∈ (1...(𝑁 − 1))((𝐹‘𝑗) = (𝐹‘𝑘) → 𝑗 = 𝑘)) |
86 | | dff13 6512 |
. 2
⊢ (𝐹:(1...(𝑁 − 1))–1-1→(𝔼‘𝑁) ↔ (𝐹:(1...(𝑁 − 1))⟶(𝔼‘𝑁) ∧ ∀𝑗 ∈ (1...(𝑁 − 1))∀𝑘 ∈ (1...(𝑁 − 1))((𝐹‘𝑗) = (𝐹‘𝑘) → 𝑗 = 𝑘))) |
87 | 10, 85, 86 | sylanbrc 698 |
1
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝐹:(1...(𝑁 − 1))–1-1→(𝔼‘𝑁)) |