Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . . . 6
⊢
({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})) = ({⟨3,
-1⟩} ∪ (((1...𝑁)
∖ {3}) × {0})) |
2 | 1 | axlowdimlem7 28206 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘3) → ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0}))
∈ (𝔼‘𝑁)) |
3 | 2 | adantr 482 |
. . . 4
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑖 ∈ (1...(𝑁 − 1))) → ({⟨3, -1⟩}
∪ (((1...𝑁) ∖
{3}) × {0})) ∈ (𝔼‘𝑁)) |
4 | | eluzge3nn 12874 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈ ℕ) |
5 | | eqid 2733 |
. . . . . 6
⊢
({⟨(𝑖 + 1),
1⟩} ∪ (((1...𝑁)
∖ {(𝑖 + 1)}) ×
{0})) = ({⟨(𝑖 + 1),
1⟩} ∪ (((1...𝑁)
∖ {(𝑖 + 1)}) ×
{0})) |
6 | 5 | axlowdimlem10 28209 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑖 ∈ (1...(𝑁 − 1))) → ({⟨(𝑖 + 1), 1⟩} ∪
(((1...𝑁) ∖ {(𝑖 + 1)}) × {0})) ∈
(𝔼‘𝑁)) |
7 | 4, 6 | sylan 581 |
. . . 4
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑖 ∈ (1...(𝑁 − 1))) → ({⟨(𝑖 + 1), 1⟩} ∪
(((1...𝑁) ∖ {(𝑖 + 1)}) × {0})) ∈
(𝔼‘𝑁)) |
8 | 3, 7 | ifcld 4575 |
. . 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 7114 |
. 2
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝐹:(1...(𝑁 − 1))⟶(𝔼‘𝑁)) |
11 | | eqeq1 2737 |
. . . . . . . 8
⊢ (𝑖 = 𝑗 → (𝑖 = 1 ↔ 𝑗 = 1)) |
12 | | oveq1 7416 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑗 → (𝑖 + 1) = (𝑗 + 1)) |
13 | 12 | opeq1d 4880 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑗 → ⟨(𝑖 + 1), 1⟩ = ⟨(𝑗 + 1), 1⟩) |
14 | 13 | sneqd 4641 |
. . . . . . . . 9
⊢ (𝑖 = 𝑗 → {⟨(𝑖 + 1), 1⟩} = {⟨(𝑗 + 1), 1⟩}) |
15 | 12 | sneqd 4641 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑗 → {(𝑖 + 1)} = {(𝑗 + 1)}) |
16 | 15 | difeq2d 4123 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑗 → ((1...𝑁) ∖ {(𝑖 + 1)}) = ((1...𝑁) ∖ {(𝑗 + 1)})) |
17 | 16 | xpeq1d 5706 |
. . . . . . . . 9
⊢ (𝑖 = 𝑗 → (((1...𝑁) ∖ {(𝑖 + 1)}) × {0}) = (((1...𝑁) ∖ {(𝑗 + 1)}) × {0})) |
18 | 14, 17 | uneq12d 4165 |
. . . . . . . 8
⊢ (𝑖 = 𝑗 → ({⟨(𝑖 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0})) = ({⟨(𝑗 + 1), 1⟩} ∪
(((1...𝑁) ∖ {(𝑗 + 1)}) ×
{0}))) |
19 | 11, 18 | ifbieq2d 4555 |
. . . . . . 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 5432 |
. . . . . . . . 9
⊢ {⟨3,
-1⟩} ∈ V |
21 | | ovex 7442 |
. . . . . . . . . . 11
⊢
(1...𝑁) ∈
V |
22 | 21 | difexi 5329 |
. . . . . . . . . 10
⊢
((1...𝑁) ∖
{3}) ∈ V |
23 | | snex 5432 |
. . . . . . . . . 10
⊢ {0}
∈ V |
24 | 22, 23 | xpex 7740 |
. . . . . . . . 9
⊢
(((1...𝑁) ∖
{3}) × {0}) ∈ V |
25 | 20, 24 | unex 7733 |
. . . . . . . 8
⊢
({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})) ∈
V |
26 | | snex 5432 |
. . . . . . . . 9
⊢
{⟨(𝑗 + 1),
1⟩} ∈ V |
27 | 21 | difexi 5329 |
. . . . . . . . . 10
⊢
((1...𝑁) ∖
{(𝑗 + 1)}) ∈
V |
28 | 27, 23 | xpex 7740 |
. . . . . . . . 9
⊢
(((1...𝑁) ∖
{(𝑗 + 1)}) × {0})
∈ V |
29 | 26, 28 | unex 7733 |
. . . . . . . 8
⊢
({⟨(𝑗 + 1),
1⟩} ∪ (((1...𝑁)
∖ {(𝑗 + 1)}) ×
{0})) ∈ V |
30 | 25, 29 | ifex 4579 |
. . . . . . 7
⊢ if(𝑗 = 1, ({⟨3, -1⟩} ∪
(((1...𝑁) ∖ {3})
× {0})), ({⟨(𝑗 +
1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑗 + 1)}) × {0}))) ∈
V |
31 | 19, 9, 30 | fvmpt 6999 |
. . . . . 6
⊢ (𝑗 ∈ (1...(𝑁 − 1)) → (𝐹‘𝑗) = if(𝑗 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})),
({⟨(𝑗 + 1), 1⟩}
∪ (((1...𝑁) ∖
{(𝑗 + 1)}) ×
{0})))) |
32 | | eqeq1 2737 |
. . . . . . . 8
⊢ (𝑖 = 𝑘 → (𝑖 = 1 ↔ 𝑘 = 1)) |
33 | | oveq1 7416 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑘 → (𝑖 + 1) = (𝑘 + 1)) |
34 | 33 | opeq1d 4880 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑘 → ⟨(𝑖 + 1), 1⟩ = ⟨(𝑘 + 1), 1⟩) |
35 | 34 | sneqd 4641 |
. . . . . . . . 9
⊢ (𝑖 = 𝑘 → {⟨(𝑖 + 1), 1⟩} = {⟨(𝑘 + 1), 1⟩}) |
36 | 33 | sneqd 4641 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑘 → {(𝑖 + 1)} = {(𝑘 + 1)}) |
37 | 36 | difeq2d 4123 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑘 → ((1...𝑁) ∖ {(𝑖 + 1)}) = ((1...𝑁) ∖ {(𝑘 + 1)})) |
38 | 37 | xpeq1d 5706 |
. . . . . . . . 9
⊢ (𝑖 = 𝑘 → (((1...𝑁) ∖ {(𝑖 + 1)}) × {0}) = (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})) |
39 | 35, 38 | uneq12d 4165 |
. . . . . . . 8
⊢ (𝑖 = 𝑘 → ({⟨(𝑖 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0})) = ({⟨(𝑘 + 1), 1⟩} ∪
(((1...𝑁) ∖ {(𝑘 + 1)}) ×
{0}))) |
40 | 32, 39 | ifbieq2d 4555 |
. . . . . . 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 5432 |
. . . . . . . . 9
⊢
{⟨(𝑘 + 1),
1⟩} ∈ V |
42 | 21 | difexi 5329 |
. . . . . . . . . 10
⊢
((1...𝑁) ∖
{(𝑘 + 1)}) ∈
V |
43 | 42, 23 | xpex 7740 |
. . . . . . . . 9
⊢
(((1...𝑁) ∖
{(𝑘 + 1)}) × {0})
∈ V |
44 | 41, 43 | unex 7733 |
. . . . . . . 8
⊢
({⟨(𝑘 + 1),
1⟩} ∪ (((1...𝑁)
∖ {(𝑘 + 1)}) ×
{0})) ∈ V |
45 | 25, 44 | ifex 4579 |
. . . . . . 7
⊢ if(𝑘 = 1, ({⟨3, -1⟩} ∪
(((1...𝑁) ∖ {3})
× {0})), ({⟨(𝑘 +
1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))) ∈
V |
46 | 40, 9, 45 | fvmpt 6999 |
. . . . . 6
⊢ (𝑘 ∈ (1...(𝑁 − 1)) → (𝐹‘𝑘) = if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})),
({⟨(𝑘 + 1), 1⟩}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) ×
{0})))) |
47 | 31, 46 | eqeqan12d 2747 |
. . . . 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 483 |
. . . 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 2759 |
. . . . . 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 2733 |
. . . . . . . . . . 11
⊢
({⟨(𝑘 + 1),
1⟩} ∪ (((1...𝑁)
∖ {(𝑘 + 1)}) ×
{0})) = ({⟨(𝑘 + 1),
1⟩} ∪ (((1...𝑁)
∖ {(𝑘 + 1)}) ×
{0})) |
52 | 1, 51 | axlowdimlem13 28212 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...(𝑁 − 1))) → ({⟨3, -1⟩}
∪ (((1...𝑁) ∖
{3}) × {0})) ≠ ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))) |
53 | 52 | neneqd 2946 |
. . . . . . . . 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 715 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝑗 ∈ (1...(𝑁 − 1)) ∧ 𝑘 ∈ (1...(𝑁 − 1)))) → (({⟨3, -1⟩}
∪ (((1...𝑁) ∖
{3}) × {0})) = ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})) → 𝑗 = 𝑘)) |
56 | 4, 55 | sylan 581 |
. . . . . 6
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑗 ∈ (1...(𝑁 − 1)) ∧ 𝑘 ∈ (1...(𝑁 − 1)))) → (({⟨3, -1⟩}
∪ (((1...𝑁) ∖
{3}) × {0})) = ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})) → 𝑗 = 𝑘)) |
57 | | iftrue 4535 |
. . . . . . . 8
⊢ (𝑗 = 1 → if(𝑗 = 1, ({⟨3, -1⟩} ∪
(((1...𝑁) ∖ {3})
× {0})), ({⟨(𝑗 +
1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑗 + 1)}) × {0}))) = ({⟨3, -1⟩}
∪ (((1...𝑁) ∖
{3}) × {0}))) |
58 | | iffalse 4538 |
. . . . . . . 8
⊢ (¬
𝑘 = 1 → if(𝑘 = 1, ({⟨3, -1⟩} ∪
(((1...𝑁) ∖ {3})
× {0})), ({⟨(𝑘 +
1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))) = ({⟨(𝑘 + 1), 1⟩} ∪
(((1...𝑁) ∖ {(𝑘 + 1)}) ×
{0}))) |
59 | 57, 58 | eqeqan12d 2747 |
. . . . . . 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 342 |
. . . . . 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 | imbitrrid 245 |
. . . . 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 2733 |
. . . . . . . . . . . 12
⊢
({⟨(𝑗 + 1),
1⟩} ∪ (((1...𝑁)
∖ {(𝑗 + 1)}) ×
{0})) = ({⟨(𝑗 + 1),
1⟩} ∪ (((1...𝑁)
∖ {(𝑗 + 1)}) ×
{0})) |
63 | 1, 62 | axlowdimlem13 28212 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 − 1))) → ({⟨3, -1⟩}
∪ (((1...𝑁) ∖
{3}) × {0})) ≠ ({⟨(𝑗 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑗 + 1)}) × {0}))) |
64 | 63 | necomd 2997 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 − 1))) → ({⟨(𝑗 + 1), 1⟩} ∪
(((1...𝑁) ∖ {(𝑗 + 1)}) × {0})) ≠
({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) ×
{0}))) |
65 | 64 | neneqd 2946 |
. . . . . . . . 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 581 |
. . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑗 ∈ (1...(𝑁 − 1))) → (({⟨(𝑗 + 1), 1⟩} ∪
(((1...𝑁) ∖ {(𝑗 + 1)}) × {0})) =
({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})) → 𝑗 = 𝑘)) |
68 | 67 | adantrr 716 |
. . . . . 6
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑗 ∈ (1...(𝑁 − 1)) ∧ 𝑘 ∈ (1...(𝑁 − 1)))) → (({⟨(𝑗 + 1), 1⟩} ∪
(((1...𝑁) ∖ {(𝑗 + 1)}) × {0})) =
({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})) → 𝑗 = 𝑘)) |
69 | | iffalse 4538 |
. . . . . . . 8
⊢ (¬
𝑗 = 1 → if(𝑗 = 1, ({⟨3, -1⟩} ∪
(((1...𝑁) ∖ {3})
× {0})), ({⟨(𝑗 +
1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑗 + 1)}) × {0}))) = ({⟨(𝑗 + 1), 1⟩} ∪
(((1...𝑁) ∖ {(𝑗 + 1)}) ×
{0}))) |
70 | | iftrue 4535 |
. . . . . . . 8
⊢ (𝑘 = 1 → if(𝑘 = 1, ({⟨3, -1⟩} ∪
(((1...𝑁) ∖ {3})
× {0})), ({⟨(𝑘 +
1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))) = ({⟨3, -1⟩}
∪ (((1...𝑁) ∖
{3}) × {0}))) |
71 | 69, 70 | eqeqan12d 2747 |
. . . . . . 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 342 |
. . . . . 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 | imbitrrid 245 |
. . . . 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 28213 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 − 1)) ∧ 𝑘 ∈ (1...(𝑁 − 1))) → (({⟨(𝑗 + 1), 1⟩} ∪
(((1...𝑁) ∖ {(𝑗 + 1)}) × {0})) =
({⟨(𝑘 + 1), 1⟩}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) × {0}))
→ 𝑗 = 𝑘)) |
75 | 74 | 3expb 1121 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ (𝑗 ∈ (1...(𝑁 − 1)) ∧ 𝑘 ∈ (1...(𝑁 − 1)))) → (({⟨(𝑗 + 1), 1⟩} ∪
(((1...𝑁) ∖ {(𝑗 + 1)}) × {0})) =
({⟨(𝑘 + 1), 1⟩}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) × {0}))
→ 𝑗 = 𝑘)) |
76 | 4, 75 | sylan 581 |
. . . . . 6
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑗 ∈ (1...(𝑁 − 1)) ∧ 𝑘 ∈ (1...(𝑁 − 1)))) → (({⟨(𝑗 + 1), 1⟩} ∪
(((1...𝑁) ∖ {(𝑗 + 1)}) × {0})) =
({⟨(𝑘 + 1), 1⟩}
∪ (((1...𝑁) ∖
{(𝑘 + 1)}) × {0}))
→ 𝑗 = 𝑘)) |
77 | 69, 58 | eqeqan12d 2747 |
. . . . . . 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 342 |
. . . . . 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 | imbitrrid 245 |
. . . . 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 1040 |
. . . 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 239 |
. . 3
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ (𝑗 ∈ (1...(𝑁 − 1)) ∧ 𝑘 ∈ (1...(𝑁 − 1)))) → ((𝐹‘𝑗) = (𝐹‘𝑘) → 𝑗 = 𝑘)) |
82 | 81 | ralrimivva 3201 |
. 2
⊢ (𝑁 ∈
(ℤ≥‘3) → ∀𝑗 ∈ (1...(𝑁 − 1))∀𝑘 ∈ (1...(𝑁 − 1))((𝐹‘𝑗) = (𝐹‘𝑘) → 𝑗 = 𝑘)) |
83 | | dff13 7254 |
. 2
⊢ (𝐹:(1...(𝑁 − 1))–1-1→(𝔼‘𝑁) ↔ (𝐹:(1...(𝑁 − 1))⟶(𝔼‘𝑁) ∧ ∀𝑗 ∈ (1...(𝑁 − 1))∀𝑘 ∈ (1...(𝑁 − 1))((𝐹‘𝑗) = (𝐹‘𝑘) → 𝑗 = 𝑘))) |
84 | 10, 82, 83 | sylanbrc 584 |
1
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝐹:(1...(𝑁 − 1))–1-1→(𝔼‘𝑁)) |