Step | Hyp | Ref
| Expression |
1 | | numclwwlk.c |
. . 3
⊢ 𝐶 = (𝑛 ∈ ℕ0 ↦ ((𝑉 ClWWalksN 𝐸)‘𝑛)) |
2 | | numclwwlk.f |
. . 3
⊢ 𝐹 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝐶‘𝑛) ∣ (𝑤‘0) = 𝑣}) |
3 | | numclwwlk.g |
. . 3
⊢ 𝐺 = (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2)
↦ {𝑤 ∈ (𝐶‘𝑛) ∣ ((𝑤‘0) = 𝑣 ∧ (𝑤‘(𝑛 − 2)) = (𝑤‘0))}) |
4 | | numclwwlk.t |
. . 3
⊢ 𝑇 = (𝑤 ∈ (𝑋𝐺𝑁) ↦ 〈(𝑤 substr 〈0, (𝑁 − 2)〉), (𝑤‘(𝑁 − 1))〉) |
5 | 1, 2, 3, 4 | numclwlk1lem2f 26619 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ 𝑇:(𝑋𝐺𝑁)⟶((𝑋𝐹(𝑁 − 2)) × (〈𝑉, 𝐸〉 Neighbors 𝑋))) |
6 | | elxp 5055 |
. . . . 5
⊢ (𝑝 ∈ ((𝑋𝐹(𝑁 − 2)) × (〈𝑉, 𝐸〉 Neighbors 𝑋)) ↔ ∃𝑎∃𝑏(𝑝 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ (𝑋𝐹(𝑁 − 2)) ∧ 𝑏 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋)))) |
7 | 1, 2, 3 | numclwlk1lem2foa 26618 |
. . . . . . . . . . 11
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ((𝑎 ∈ (𝑋𝐹(𝑁 − 2)) ∧ 𝑏 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋)) → ((𝑎 ++ 〈“𝑋”〉) ++ 〈“𝑏”〉) ∈ (𝑋𝐺𝑁))) |
8 | 7 | com12 32 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ (𝑋𝐹(𝑁 − 2)) ∧ 𝑏 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋)) → ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ((𝑎 ++
〈“𝑋”〉) ++ 〈“𝑏”〉) ∈ (𝑋𝐺𝑁))) |
9 | 8 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑝 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ (𝑋𝐹(𝑁 − 2)) ∧ 𝑏 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋))) → ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ((𝑎 ++
〈“𝑋”〉) ++ 〈“𝑏”〉) ∈ (𝑋𝐺𝑁))) |
10 | 9 | imp 444 |
. . . . . . . 8
⊢ (((𝑝 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ (𝑋𝐹(𝑁 − 2)) ∧ 𝑏 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋))) ∧ (𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ ((𝑎 ++
〈“𝑋”〉) ++ 〈“𝑏”〉) ∈ (𝑋𝐺𝑁)) |
11 | | simpl 472 |
. . . . . . . . 9
⊢ ((((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉) ∈ (𝑋𝐺𝑁) ∧ ((𝑝 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ (𝑋𝐹(𝑁 − 2)) ∧ 𝑏 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋))) ∧ (𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))))
→ ((𝑎 ++
〈“𝑋”〉) ++ 〈“𝑏”〉) ∈ (𝑋𝐺𝑁)) |
12 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑥 = ((𝑎 ++ 〈“𝑋”〉) ++ 〈“𝑏”〉) → (𝑇‘𝑥) = (𝑇‘((𝑎 ++ 〈“𝑋”〉) ++ 〈“𝑏”〉))) |
13 | 12 | eqeq2d 2620 |
. . . . . . . . . 10
⊢ (𝑥 = ((𝑎 ++ 〈“𝑋”〉) ++ 〈“𝑏”〉) → (𝑝 = (𝑇‘𝑥) ↔ 𝑝 = (𝑇‘((𝑎 ++ 〈“𝑋”〉) ++ 〈“𝑏”〉)))) |
14 | | simprr 792 |
. . . . . . . . . . . 12
⊢ ((((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉) ∈ (𝑋𝐺𝑁) ∧ ((𝑝 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ (𝑋𝐹(𝑁 − 2)) ∧ 𝑏 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋))) ∧ (𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))))
→ (𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈
(ℤ≥‘3))) |
15 | 1, 2, 3, 4 | numclwlk1lem2fv 26620 |
. . . . . . . . . . . 12
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (((𝑎 ++
〈“𝑋”〉) ++ 〈“𝑏”〉) ∈ (𝑋𝐺𝑁) → (𝑇‘((𝑎 ++ 〈“𝑋”〉) ++ 〈“𝑏”〉)) = 〈(((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉) substr 〈0, (𝑁 − 2)〉), (((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)‘(𝑁 − 1))〉)) |
16 | 14, 11, 15 | sylc 63 |
. . . . . . . . . . 11
⊢ ((((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉) ∈ (𝑋𝐺𝑁) ∧ ((𝑝 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ (𝑋𝐹(𝑁 − 2)) ∧ 𝑏 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋))) ∧ (𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))))
→ (𝑇‘((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)) = 〈(((𝑎 ++ 〈“𝑋”〉) ++ 〈“𝑏”〉) substr 〈0,
(𝑁 − 2)〉),
(((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)‘(𝑁 − 1))〉) |
17 | 16 | eqeq2d 2620 |
. . . . . . . . . 10
⊢ ((((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉) ∈ (𝑋𝐺𝑁) ∧ ((𝑝 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ (𝑋𝐹(𝑁 − 2)) ∧ 𝑏 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋))) ∧ (𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))))
→ (𝑝 = (𝑇‘((𝑎 ++ 〈“𝑋”〉) ++ 〈“𝑏”〉)) ↔ 𝑝 = 〈(((𝑎 ++ 〈“𝑋”〉) ++ 〈“𝑏”〉) substr 〈0,
(𝑁 − 2)〉),
(((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)‘(𝑁 − 1))〉)) |
18 | 13, 17 | sylan9bbr 733 |
. . . . . . . . 9
⊢
(((((𝑎 ++
〈“𝑋”〉) ++ 〈“𝑏”〉) ∈ (𝑋𝐺𝑁) ∧ ((𝑝 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ (𝑋𝐹(𝑁 − 2)) ∧ 𝑏 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋))) ∧ (𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))))
∧ 𝑥 = ((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)) → (𝑝 = (𝑇‘𝑥) ↔ 𝑝 = 〈(((𝑎 ++ 〈“𝑋”〉) ++ 〈“𝑏”〉) substr 〈0,
(𝑁 − 2)〉),
(((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)‘(𝑁 − 1))〉)) |
19 | | simprll 798 |
. . . . . . . . . 10
⊢ ((((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉) ∈ (𝑋𝐺𝑁) ∧ ((𝑝 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ (𝑋𝐹(𝑁 − 2)) ∧ 𝑏 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋))) ∧ (𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))))
→ 𝑝 = 〈𝑎, 𝑏〉) |
20 | | nbgraisvtx 25960 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑉 USGrph 𝐸 → (𝑏 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋) → 𝑏 ∈ 𝑉)) |
21 | 20 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑏 ∈
(〈𝑉, 𝐸〉 Neighbors 𝑋) → 𝑏 ∈ 𝑉)) |
22 | | simp1 1054 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ 𝑉 USGrph 𝐸) |
23 | | uzuzle23 11605 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈
(ℤ≥‘2)) |
24 | | uznn0sub 11595 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈
(ℤ≥‘2) → (𝑁 − 2) ∈
ℕ0) |
25 | 23, 24 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈
(ℤ≥‘3) → (𝑁 − 2) ∈
ℕ0) |
26 | 25 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑁 − 2) ∈
ℕ0) |
27 | | simp2 1055 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ 𝑋 ∈ 𝑉) |
28 | 1, 2 | numclwwlkovfel2 26610 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑉 USGrph 𝐸 ∧ (𝑁 − 2) ∈ ℕ0 ∧
𝑋 ∈ 𝑉) → (𝑎 ∈ (𝑋𝐹(𝑁 − 2)) ↔ ((𝑎 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑎) − 1)){(𝑎‘𝑖), (𝑎‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑎), (𝑎‘0)} ∈ ran 𝐸) ∧ (#‘𝑎) = (𝑁 − 2) ∧ (𝑎‘0) = 𝑋))) |
29 | 22, 26, 27, 28 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑎 ∈ (𝑋𝐹(𝑁 − 2)) ↔ ((𝑎 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑎) − 1)){(𝑎‘𝑖), (𝑎‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑎), (𝑎‘0)} ∈ ran 𝐸) ∧ (#‘𝑎) = (𝑁 − 2) ∧ (𝑎‘0) = 𝑋))) |
30 | | df-3an 1033 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑎 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑎) − 1)){(𝑎‘𝑖), (𝑎‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑎), (𝑎‘0)} ∈ ran 𝐸) ∧ (#‘𝑎) = (𝑁 − 2) ∧ (𝑎‘0) = 𝑋) ↔ (((𝑎 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑎) − 1)){(𝑎‘𝑖), (𝑎‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑎), (𝑎‘0)} ∈ ran 𝐸) ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑎‘0) = 𝑋)) |
31 | 29, 30 | syl6bb 275 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑎 ∈ (𝑋𝐹(𝑁 − 2)) ↔ (((𝑎 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑎) − 1)){(𝑎‘𝑖), (𝑎‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑎), (𝑎‘0)} ∈ ran 𝐸) ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑎‘0) = 𝑋))) |
32 | | simplll 794 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑏 ∈ 𝑉) → 𝑎 ∈ Word 𝑉) |
33 | | s1cl 13235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑋 ∈ 𝑉 → 〈“𝑋”〉 ∈ Word 𝑉) |
34 | 33 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ 〈“𝑋”〉 ∈ Word 𝑉) |
35 | 34 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ 〈“𝑋”〉 ∈ Word 𝑉) |
36 | 35 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑏 ∈ 𝑉) → 〈“𝑋”〉 ∈ Word 𝑉) |
37 | | s1cl 13235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑏 ∈ 𝑉 → 〈“𝑏”〉 ∈ Word 𝑉) |
38 | 37 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑏 ∈ 𝑉) → 〈“𝑏”〉 ∈ Word 𝑉) |
39 | | ccatass 13224 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑎 ∈ Word 𝑉 ∧ 〈“𝑋”〉 ∈ Word 𝑉 ∧ 〈“𝑏”〉 ∈ Word 𝑉) → ((𝑎 ++ 〈“𝑋”〉) ++ 〈“𝑏”〉) = (𝑎 ++ (〈“𝑋”〉 ++
〈“𝑏”〉))) |
40 | 39 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑎 ∈ Word 𝑉 ∧ 〈“𝑋”〉 ∈ Word 𝑉 ∧ 〈“𝑏”〉 ∈ Word 𝑉) → (((𝑎 ++ 〈“𝑋”〉) ++ 〈“𝑏”〉) substr 〈0,
(𝑁 − 2)〉) =
((𝑎 ++ (〈“𝑋”〉 ++
〈“𝑏”〉)) substr 〈0, (𝑁 −
2)〉)) |
41 | 32, 36, 38, 40 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑏 ∈ 𝑉) → (((𝑎 ++ 〈“𝑋”〉) ++ 〈“𝑏”〉) substr 〈0,
(𝑁 − 2)〉) =
((𝑎 ++ (〈“𝑋”〉 ++
〈“𝑏”〉)) substr 〈0, (𝑁 −
2)〉)) |
42 | | ccatcl 13212 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((〈“𝑋”〉 ∈ Word 𝑉 ∧ 〈“𝑏”〉 ∈ Word 𝑉) → (〈“𝑋”〉 ++ 〈“𝑏”〉) ∈ Word 𝑉) |
43 | 35, 37, 42 | syl2an 493 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑏 ∈ 𝑉) → (〈“𝑋”〉 ++
〈“𝑏”〉) ∈ Word 𝑉) |
44 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) → (#‘𝑎) = (𝑁 − 2)) |
45 | 44 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) → (𝑁 − 2) = (#‘𝑎)) |
46 | 45 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (𝑁 − 2) =
(#‘𝑎)) |
47 | 46 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑏 ∈ 𝑉) → (𝑁 − 2) = (#‘𝑎)) |
48 | | swrdccatid 13348 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑎 ∈ Word 𝑉 ∧ (〈“𝑋”〉 ++ 〈“𝑏”〉) ∈ Word 𝑉 ∧ (𝑁 − 2) = (#‘𝑎)) → ((𝑎 ++ (〈“𝑋”〉 ++ 〈“𝑏”〉)) substr 〈0,
(𝑁 − 2)〉) =
𝑎) |
49 | 32, 43, 47, 48 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑏 ∈ 𝑉) → ((𝑎 ++ (〈“𝑋”〉 ++ 〈“𝑏”〉)) substr 〈0,
(𝑁 − 2)〉) =
𝑎) |
50 | 41, 49 | eqtr2d 2645 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑏 ∈ 𝑉) → 𝑎 = (((𝑎 ++ 〈“𝑋”〉) ++ 〈“𝑏”〉) substr 〈0,
(𝑁 −
2)〉)) |
51 | | ovex 6577 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉) ∈ V |
52 | | lsw 13204 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉) ∈ V → ( lastS
‘((𝑎 ++
〈“𝑋”〉) ++ 〈“𝑏”〉)) = (((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)‘((#‘((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)) − 1))) |
53 | 51, 52 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ( lastS
‘((𝑎 ++
〈“𝑋”〉) ++ 〈“𝑏”〉)) = (((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)‘((#‘((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)) − 1)) |
54 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) → 𝑎 ∈ Word 𝑉) |
55 | | ccatcl 13212 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑎 ∈ Word 𝑉 ∧ 〈“𝑋”〉 ∈ Word 𝑉) → (𝑎 ++ 〈“𝑋”〉) ∈ Word 𝑉) |
56 | 54, 34, 55 | syl2an 493 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (𝑎 ++
〈“𝑋”〉) ∈ Word 𝑉) |
57 | | lswccats1 13263 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑎 ++ 〈“𝑋”〉) ∈ Word 𝑉 ∧ 𝑏 ∈ 𝑉) → ( lastS ‘((𝑎 ++ 〈“𝑋”〉) ++ 〈“𝑏”〉)) = 𝑏) |
58 | 56, 57 | sylan 487 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑏 ∈ 𝑉) → ( lastS ‘((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)) = 𝑏) |
59 | | ccatlen 13213 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑎 ++ 〈“𝑋”〉) ∈ Word 𝑉 ∧ 〈“𝑏”〉 ∈ Word 𝑉) → (#‘((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)) = ((#‘(𝑎 ++ 〈“𝑋”〉)) +
(#‘〈“𝑏”〉))) |
60 | 56, 37, 59 | syl2an 493 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑏 ∈ 𝑉) → (#‘((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)) = ((#‘(𝑎 ++ 〈“𝑋”〉)) +
(#‘〈“𝑏”〉))) |
61 | 54, 34 | anim12i 588 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (𝑎 ∈ Word 𝑉 ∧ 〈“𝑋”〉 ∈ Word 𝑉)) |
62 | 61 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑏 ∈ 𝑉) → (𝑎 ∈ Word 𝑉 ∧ 〈“𝑋”〉 ∈ Word 𝑉)) |
63 | | ccatlen 13213 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑎 ∈ Word 𝑉 ∧ 〈“𝑋”〉 ∈ Word 𝑉) → (#‘(𝑎 ++ 〈“𝑋”〉)) = ((#‘𝑎) + (#‘〈“𝑋”〉))) |
64 | 62, 63 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑏 ∈ 𝑉) → (#‘(𝑎 ++ 〈“𝑋”〉)) =
((#‘𝑎) +
(#‘〈“𝑋”〉))) |
65 | | s1len 13238 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(#‘〈“𝑏”〉) = 1 |
66 | 65 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑏 ∈ 𝑉) →
(#‘〈“𝑏”〉) = 1) |
67 | 64, 66 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑏 ∈ 𝑉) → ((#‘(𝑎 ++ 〈“𝑋”〉)) +
(#‘〈“𝑏”〉)) = (((#‘𝑎) + (#‘〈“𝑋”〉)) +
1)) |
68 | | s1len 13238 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(#‘〈“𝑋”〉) = 1 |
69 | 68 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (#‘〈“𝑋”〉) = 1) |
70 | 44, 69 | oveqan12d 6568 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ ((#‘𝑎) +
(#‘〈“𝑋”〉)) = ((𝑁 − 2) + 1)) |
71 | 70 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (((#‘𝑎) +
(#‘〈“𝑋”〉)) + 1) = (((𝑁 − 2) + 1) + 1)) |
72 | | eluzelcn 11575 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈ ℂ) |
73 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑁 ∈ ℂ → 𝑁 ∈
ℂ) |
74 | | 2cnd 10970 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑁 ∈ ℂ → 2 ∈
ℂ) |
75 | 73, 74 | subcld 10271 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑁 ∈ ℂ → (𝑁 − 2) ∈
ℂ) |
76 | | 1cnd 9935 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑁 ∈ ℂ → 1 ∈
ℂ) |
77 | 75, 76, 76 | addassd 9941 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑁 ∈ ℂ → (((𝑁 − 2) + 1) + 1) = ((𝑁 − 2) + (1 +
1))) |
78 | | 1p1e2 11011 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (1 + 1) =
2 |
79 | 78 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑁 ∈ ℂ → (1 + 1) =
2) |
80 | 79 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑁 ∈ ℂ → ((𝑁 − 2) + (1 + 1)) = ((𝑁 − 2) +
2)) |
81 | 77, 80 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑁 ∈ ℂ → (((𝑁 − 2) + 1) + 1) = ((𝑁 − 2) +
2)) |
82 | 72, 81 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑁 ∈
(ℤ≥‘3) → (((𝑁 − 2) + 1) + 1) = ((𝑁 − 2) + 2)) |
83 | | 2cnd 10970 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑁 ∈
(ℤ≥‘3) → 2 ∈ ℂ) |
84 | 72, 83 | npcand 10275 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑁 ∈
(ℤ≥‘3) → ((𝑁 − 2) + 2) = 𝑁) |
85 | 82, 84 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑁 ∈
(ℤ≥‘3) → (((𝑁 − 2) + 1) + 1) = 𝑁) |
86 | 85 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (((𝑁 − 2) + 1)
+ 1) = 𝑁) |
87 | 86 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (((𝑁 − 2) + 1)
+ 1) = 𝑁) |
88 | 71, 87 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ (((#‘𝑎) +
(#‘〈“𝑋”〉)) + 1) = 𝑁) |
89 | 88 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑏 ∈ 𝑉) → (((#‘𝑎) + (#‘〈“𝑋”〉)) + 1) = 𝑁) |
90 | 60, 67, 89 | 3eqtrd 2648 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑏 ∈ 𝑉) → (#‘((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)) = 𝑁) |
91 | 90 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑏 ∈ 𝑉) → ((#‘((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)) − 1) = (𝑁 − 1)) |
92 | 91 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑏 ∈ 𝑉) → (((𝑎 ++ 〈“𝑋”〉) ++ 〈“𝑏”〉)‘((#‘((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)) − 1)) = (((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)‘(𝑁 − 1))) |
93 | 53, 58, 92 | 3eqtr3a 2668 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑏 ∈ 𝑉) → 𝑏 = (((𝑎 ++ 〈“𝑋”〉) ++ 〈“𝑏”〉)‘(𝑁 − 1))) |
94 | 50, 93 | opeq12d 4348 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
∧ 𝑏 ∈ 𝑉) → 〈𝑎, 𝑏〉 = 〈(((𝑎 ++ 〈“𝑋”〉) ++ 〈“𝑏”〉) substr 〈0,
(𝑁 − 2)〉),
(((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)‘(𝑁 − 1))〉) |
95 | 94 | exp31 628 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑎 ∈ Word 𝑉 ∧ (#‘𝑎) = (𝑁 − 2)) → ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑏 ∈ 𝑉 → 〈𝑎, 𝑏〉 = 〈(((𝑎 ++ 〈“𝑋”〉) ++ 〈“𝑏”〉) substr 〈0,
(𝑁 − 2)〉),
(((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)‘(𝑁 − 1))〉))) |
96 | 95 | 3ad2antl1 1216 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑎 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑎) − 1)){(𝑎‘𝑖), (𝑎‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑎), (𝑎‘0)} ∈ ran 𝐸) ∧ (#‘𝑎) = (𝑁 − 2)) → ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑏 ∈ 𝑉 → 〈𝑎, 𝑏〉 = 〈(((𝑎 ++ 〈“𝑋”〉) ++ 〈“𝑏”〉) substr 〈0,
(𝑁 − 2)〉),
(((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)‘(𝑁 − 1))〉))) |
97 | 96 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑎 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑎) − 1)){(𝑎‘𝑖), (𝑎‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑎), (𝑎‘0)} ∈ ran 𝐸) ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑎‘0) = 𝑋) → ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑏 ∈ 𝑉 → 〈𝑎, 𝑏〉 = 〈(((𝑎 ++ 〈“𝑋”〉) ++ 〈“𝑏”〉) substr 〈0,
(𝑁 − 2)〉),
(((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)‘(𝑁 − 1))〉))) |
98 | 97 | com12 32 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ((((𝑎 ∈ Word
𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑎) − 1)){(𝑎‘𝑖), (𝑎‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑎), (𝑎‘0)} ∈ ran 𝐸) ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑎‘0) = 𝑋) → (𝑏 ∈ 𝑉 → 〈𝑎, 𝑏〉 = 〈(((𝑎 ++ 〈“𝑋”〉) ++ 〈“𝑏”〉) substr 〈0,
(𝑁 − 2)〉),
(((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)‘(𝑁 − 1))〉))) |
99 | 98 | 3adant1 1072 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ((((𝑎 ∈ Word
𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑎) − 1)){(𝑎‘𝑖), (𝑎‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑎), (𝑎‘0)} ∈ ran 𝐸) ∧ (#‘𝑎) = (𝑁 − 2)) ∧ (𝑎‘0) = 𝑋) → (𝑏 ∈ 𝑉 → 〈𝑎, 𝑏〉 = 〈(((𝑎 ++ 〈“𝑋”〉) ++ 〈“𝑏”〉) substr 〈0,
(𝑁 − 2)〉),
(((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)‘(𝑁 − 1))〉))) |
100 | 31, 99 | sylbid 229 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑎 ∈ (𝑋𝐹(𝑁 − 2)) → (𝑏 ∈ 𝑉 → 〈𝑎, 𝑏〉 = 〈(((𝑎 ++ 〈“𝑋”〉) ++ 〈“𝑏”〉) substr 〈0,
(𝑁 − 2)〉),
(((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)‘(𝑁 − 1))〉))) |
101 | 100 | com23 84 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑏 ∈ 𝑉 → (𝑎 ∈ (𝑋𝐹(𝑁 − 2)) → 〈𝑎, 𝑏〉 = 〈(((𝑎 ++ 〈“𝑋”〉) ++ 〈“𝑏”〉) substr 〈0,
(𝑁 − 2)〉),
(((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)‘(𝑁 − 1))〉))) |
102 | 21, 101 | syld 46 |
. . . . . . . . . . . . . . 15
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ (𝑏 ∈
(〈𝑉, 𝐸〉 Neighbors 𝑋) → (𝑎 ∈ (𝑋𝐹(𝑁 − 2)) → 〈𝑎, 𝑏〉 = 〈(((𝑎 ++ 〈“𝑋”〉) ++ 〈“𝑏”〉) substr 〈0,
(𝑁 − 2)〉),
(((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)‘(𝑁 − 1))〉))) |
103 | 102 | com13 86 |
. . . . . . . . . . . . . 14
⊢ (𝑎 ∈ (𝑋𝐹(𝑁 − 2)) → (𝑏 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋) → ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ 〈𝑎, 𝑏〉 = 〈(((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉) substr 〈0, (𝑁 − 2)〉), (((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)‘(𝑁 − 1))〉))) |
104 | 103 | imp 444 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ (𝑋𝐹(𝑁 − 2)) ∧ 𝑏 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋)) → ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ 〈𝑎, 𝑏〉 = 〈(((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉) substr 〈0, (𝑁 − 2)〉), (((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)‘(𝑁 − 1))〉)) |
105 | 104 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑝 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ (𝑋𝐹(𝑁 − 2)) ∧ 𝑏 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋))) → ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ 〈𝑎, 𝑏〉 = 〈(((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉) substr 〈0, (𝑁 − 2)〉), (((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)‘(𝑁 − 1))〉)) |
106 | 105 | imp 444 |
. . . . . . . . . . 11
⊢ (((𝑝 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ (𝑋𝐹(𝑁 − 2)) ∧ 𝑏 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋))) ∧ (𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ 〈𝑎, 𝑏〉 = 〈(((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉) substr 〈0, (𝑁 − 2)〉), (((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)‘(𝑁 − 1))〉) |
107 | 106 | adantl 481 |
. . . . . . . . . 10
⊢ ((((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉) ∈ (𝑋𝐺𝑁) ∧ ((𝑝 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ (𝑋𝐹(𝑁 − 2)) ∧ 𝑏 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋))) ∧ (𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))))
→ 〈𝑎, 𝑏〉 = 〈(((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉) substr 〈0, (𝑁 − 2)〉), (((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)‘(𝑁 − 1))〉) |
108 | 19, 107 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉) ∈ (𝑋𝐺𝑁) ∧ ((𝑝 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ (𝑋𝐹(𝑁 − 2)) ∧ 𝑏 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋))) ∧ (𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))))
→ 𝑝 = 〈(((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉) substr 〈0, (𝑁 − 2)〉), (((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉)‘(𝑁 − 1))〉) |
109 | 11, 18, 108 | rspcedvd 3289 |
. . . . . . . 8
⊢ ((((𝑎 ++ 〈“𝑋”〉) ++
〈“𝑏”〉) ∈ (𝑋𝐺𝑁) ∧ ((𝑝 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ (𝑋𝐹(𝑁 − 2)) ∧ 𝑏 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋))) ∧ (𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))))
→ ∃𝑥 ∈
(𝑋𝐺𝑁)𝑝 = (𝑇‘𝑥)) |
110 | 10, 109 | mpancom 700 |
. . . . . . 7
⊢ (((𝑝 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ (𝑋𝐹(𝑁 − 2)) ∧ 𝑏 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋))) ∧ (𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)))
→ ∃𝑥 ∈
(𝑋𝐺𝑁)𝑝 = (𝑇‘𝑥)) |
111 | 110 | ex 449 |
. . . . . 6
⊢ ((𝑝 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ (𝑋𝐹(𝑁 − 2)) ∧ 𝑏 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋))) → ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ∃𝑥 ∈
(𝑋𝐺𝑁)𝑝 = (𝑇‘𝑥))) |
112 | 111 | exlimivv 1847 |
. . . . 5
⊢
(∃𝑎∃𝑏(𝑝 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ (𝑋𝐹(𝑁 − 2)) ∧ 𝑏 ∈ (〈𝑉, 𝐸〉 Neighbors 𝑋))) → ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ∃𝑥 ∈
(𝑋𝐺𝑁)𝑝 = (𝑇‘𝑥))) |
113 | 6, 112 | sylbi 206 |
. . . 4
⊢ (𝑝 ∈ ((𝑋𝐹(𝑁 − 2)) × (〈𝑉, 𝐸〉 Neighbors 𝑋)) → ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ∃𝑥 ∈
(𝑋𝐺𝑁)𝑝 = (𝑇‘𝑥))) |
114 | 113 | impcom 445 |
. . 3
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
∧ 𝑝 ∈ ((𝑋𝐹(𝑁 − 2)) × (〈𝑉, 𝐸〉 Neighbors 𝑋))) → ∃𝑥 ∈ (𝑋𝐺𝑁)𝑝 = (𝑇‘𝑥)) |
115 | 114 | ralrimiva 2949 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ ∀𝑝 ∈
((𝑋𝐹(𝑁 − 2)) × (〈𝑉, 𝐸〉 Neighbors 𝑋))∃𝑥 ∈ (𝑋𝐺𝑁)𝑝 = (𝑇‘𝑥)) |
116 | | dffo3 6282 |
. 2
⊢ (𝑇:(𝑋𝐺𝑁)–onto→((𝑋𝐹(𝑁 − 2)) × (〈𝑉, 𝐸〉 Neighbors 𝑋)) ↔ (𝑇:(𝑋𝐺𝑁)⟶((𝑋𝐹(𝑁 − 2)) × (〈𝑉, 𝐸〉 Neighbors 𝑋)) ∧ ∀𝑝 ∈ ((𝑋𝐹(𝑁 − 2)) × (〈𝑉, 𝐸〉 Neighbors 𝑋))∃𝑥 ∈ (𝑋𝐺𝑁)𝑝 = (𝑇‘𝑥))) |
117 | 5, 115, 116 | sylanbrc 695 |
1
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))
→ 𝑇:(𝑋𝐺𝑁)–onto→((𝑋𝐹(𝑁 − 2)) × (〈𝑉, 𝐸〉 Neighbors 𝑋))) |