Step | Hyp | Ref
| Expression |
1 | | peano2nn0 12130 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ0) |
2 | | iswwlksn 27922 |
. . 3
⊢ ((𝑁 + 1) ∈ ℕ0
→ (𝑊 ∈ ((𝑁 + 1) WWalksN 𝐺) ↔ (𝑊 ∈ (WWalks‘𝐺) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1)))) |
3 | 1, 2 | syl 17 |
. 2
⊢ (𝑁 ∈ ℕ0
→ (𝑊 ∈ ((𝑁 + 1) WWalksN 𝐺) ↔ (𝑊 ∈ (WWalks‘𝐺) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1)))) |
4 | | eqid 2737 |
. . . . 5
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
5 | | eqid 2737 |
. . . . 5
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
6 | 4, 5 | iswwlks 27920 |
. . . 4
⊢ (𝑊 ∈ (WWalks‘𝐺) ↔ (𝑊 ≠ ∅ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
7 | | simp1 1138 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0) → 𝑊 ∈ Word (Vtx‘𝐺)) |
8 | | nn0p1nn 12129 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ) |
9 | 8 | 3ad2ant3 1137 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0) → (𝑁 + 1) ∈
ℕ) |
10 | 1 | nn0red 12151 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℝ) |
11 | 10 | lep1d 11763 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ≤ ((𝑁 + 1) + 1)) |
12 | 11 | 3ad2ant3 1137 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0) → (𝑁 + 1) ≤ ((𝑁 + 1) + 1)) |
13 | | breq2 5057 |
. . . . . . . . . . . . . 14
⊢
((♯‘𝑊) =
((𝑁 + 1) + 1) →
((𝑁 + 1) ≤
(♯‘𝑊) ↔
(𝑁 + 1) ≤ ((𝑁 + 1) + 1))) |
14 | 13 | 3ad2ant2 1136 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0) → ((𝑁 + 1) ≤ (♯‘𝑊) ↔ (𝑁 + 1) ≤ ((𝑁 + 1) + 1))) |
15 | 12, 14 | mpbird 260 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0) → (𝑁 + 1) ≤ (♯‘𝑊)) |
16 | | pfxn0 14251 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (𝑁 + 1) ∈ ℕ ∧ (𝑁 + 1) ≤ (♯‘𝑊)) → (𝑊 prefix (𝑁 + 1)) ≠ ∅) |
17 | 7, 9, 15, 16 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0) → (𝑊 prefix (𝑁 + 1)) ≠ ∅) |
18 | 17 | 3exp 1121 |
. . . . . . . . . 10
⊢ (𝑊 ∈ Word (Vtx‘𝐺) → ((♯‘𝑊) = ((𝑁 + 1) + 1) → (𝑁 ∈ ℕ0 → (𝑊 prefix (𝑁 + 1)) ≠ ∅))) |
19 | 18 | 3ad2ant2 1136 |
. . . . . . . . 9
⊢ ((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ((♯‘𝑊) = ((𝑁 + 1) + 1) → (𝑁 ∈ ℕ0 → (𝑊 prefix (𝑁 + 1)) ≠ ∅))) |
20 | 19 | imp 410 |
. . . . . . . 8
⊢ (((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1)) → (𝑁 ∈ ℕ0 → (𝑊 prefix (𝑁 + 1)) ≠ ∅)) |
21 | 20 | impcom 411 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑊 ≠ ∅
∧ 𝑊 ∈ Word
(Vtx‘𝐺) ∧
∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1))) → (𝑊 prefix (𝑁 + 1)) ≠ ∅) |
22 | | pfxcl 14242 |
. . . . . . . . . 10
⊢ (𝑊 ∈ Word (Vtx‘𝐺) → (𝑊 prefix (𝑁 + 1)) ∈ Word (Vtx‘𝐺)) |
23 | 22 | 3ad2ant2 1136 |
. . . . . . . . 9
⊢ ((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → (𝑊 prefix (𝑁 + 1)) ∈ Word (Vtx‘𝐺)) |
24 | 23 | adantr 484 |
. . . . . . . 8
⊢ (((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1)) → (𝑊 prefix (𝑁 + 1)) ∈ Word (Vtx‘𝐺)) |
25 | 24 | adantl 485 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑊 ≠ ∅
∧ 𝑊 ∈ Word
(Vtx‘𝐺) ∧
∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1))) → (𝑊 prefix (𝑁 + 1)) ∈ Word (Vtx‘𝐺)) |
26 | | oveq1 7220 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((♯‘𝑊) =
((𝑁 + 1) + 1) →
((♯‘𝑊) −
1) = (((𝑁 + 1) + 1) −
1)) |
27 | 1 | nn0cnd 12152 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℂ) |
28 | | 1cnd 10828 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈ ℕ0
→ 1 ∈ ℂ) |
29 | 27, 28 | pncand 11190 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ0
→ (((𝑁 + 1) + 1)
− 1) = (𝑁 +
1)) |
30 | 26, 29 | sylan9eq 2798 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((♯‘𝑊)
= ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)
→ ((♯‘𝑊)
− 1) = (𝑁 +
1)) |
31 | 30 | oveq2d 7229 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((♯‘𝑊)
= ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)
→ (0..^((♯‘𝑊) − 1)) = (0..^(𝑁 + 1))) |
32 | 31 | raleqdv 3325 |
. . . . . . . . . . . . . . . . . 18
⊢
(((♯‘𝑊)
= ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)
→ (∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^(𝑁 + 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
33 | 32 | adantl 485 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) →
(∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^(𝑁 + 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
34 | | nn0z 12200 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℤ) |
35 | | nn0z 12200 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑁 + 1) ∈ ℕ0
→ (𝑁 + 1) ∈
ℤ) |
36 | 1, 35 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℤ) |
37 | | nn0re 12099 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ) |
38 | 37 | lep1d 11763 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ≤ (𝑁 + 1)) |
39 | 34, 36, 38 | 3jca 1130 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈ ℕ0
→ (𝑁 ∈ ℤ
∧ (𝑁 + 1) ∈
ℤ ∧ 𝑁 ≤ (𝑁 + 1))) |
40 | 39 | ad2antll 729 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) → (𝑁 ∈ ℤ ∧ (𝑁 + 1) ∈ ℤ ∧ 𝑁 ≤ (𝑁 + 1))) |
41 | | eluz2 12444 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 + 1) ∈
(ℤ≥‘𝑁) ↔ (𝑁 ∈ ℤ ∧ (𝑁 + 1) ∈ ℤ ∧ 𝑁 ≤ (𝑁 + 1))) |
42 | 40, 41 | sylibr 237 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) → (𝑁 + 1) ∈
(ℤ≥‘𝑁)) |
43 | | fzoss2 13270 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 + 1) ∈
(ℤ≥‘𝑁) → (0..^𝑁) ⊆ (0..^(𝑁 + 1))) |
44 | 42, 43 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) →
(0..^𝑁) ⊆ (0..^(𝑁 + 1))) |
45 | | ssralv 3967 |
. . . . . . . . . . . . . . . . . . 19
⊢
((0..^𝑁) ⊆
(0..^(𝑁 + 1)) →
(∀𝑖 ∈
(0..^(𝑁 + 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
46 | 44, 45 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) →
(∀𝑖 ∈
(0..^(𝑁 + 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
47 | | simpll 767 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑊 ∈ Word (Vtx‘𝐺)) |
48 | | nn0fz0 13210 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑁 + 1) ∈ ℕ0
↔ (𝑁 + 1) ∈
(0...(𝑁 +
1))) |
49 | 1, 48 | sylib 221 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
(0...(𝑁 +
1))) |
50 | 49 | ad2antll 729 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) → (𝑁 + 1) ∈ (0...(𝑁 + 1))) |
51 | | fzelp1 13164 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑁 + 1) ∈ (0...(𝑁 + 1)) → (𝑁 + 1) ∈ (0...((𝑁 + 1) + 1))) |
52 | 50, 51 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) → (𝑁 + 1) ∈ (0...((𝑁 + 1) + 1))) |
53 | | oveq2 7221 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((♯‘𝑊) =
((𝑁 + 1) + 1) →
(0...(♯‘𝑊)) =
(0...((𝑁 + 1) +
1))) |
54 | 53 | eleq2d 2823 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((♯‘𝑊) =
((𝑁 + 1) + 1) →
((𝑁 + 1) ∈
(0...(♯‘𝑊))
↔ (𝑁 + 1) ∈
(0...((𝑁 + 1) +
1)))) |
55 | 54 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((♯‘𝑊)
= ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)
→ ((𝑁 + 1) ∈
(0...(♯‘𝑊))
↔ (𝑁 + 1) ∈
(0...((𝑁 + 1) +
1)))) |
56 | 55 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) → ((𝑁 + 1) ∈
(0...(♯‘𝑊))
↔ (𝑁 + 1) ∈
(0...((𝑁 + 1) +
1)))) |
57 | 52, 56 | mpbird 260 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) → (𝑁 + 1) ∈
(0...(♯‘𝑊))) |
58 | 57 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑁 + 1) ∈ (0...(♯‘𝑊))) |
59 | | fzossfzop1 13320 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈ ℕ0
→ (0..^𝑁) ⊆
(0..^(𝑁 +
1))) |
60 | 59 | sseld 3900 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ ℕ0
→ (𝑖 ∈ (0..^𝑁) → 𝑖 ∈ (0..^(𝑁 + 1)))) |
61 | 60 | ad2antll 729 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) → (𝑖 ∈ (0..^𝑁) → 𝑖 ∈ (0..^(𝑁 + 1)))) |
62 | 61 | imp 410 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑖 ∈ (0..^(𝑁 + 1))) |
63 | | pfxfv 14247 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (𝑁 + 1) ∈ (0...(♯‘𝑊)) ∧ 𝑖 ∈ (0..^(𝑁 + 1))) → ((𝑊 prefix (𝑁 + 1))‘𝑖) = (𝑊‘𝑖)) |
64 | 47, 58, 62, 63 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑊 prefix (𝑁 + 1))‘𝑖) = (𝑊‘𝑖)) |
65 | 64 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑊‘𝑖) = ((𝑊 prefix (𝑁 + 1))‘𝑖)) |
66 | | fzofzp1 13339 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑖 ∈ (0..^𝑁) → (𝑖 + 1) ∈ (0...𝑁)) |
67 | 66 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑖 + 1) ∈ (0...𝑁)) |
68 | | fzval3 13311 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑁 ∈ ℤ →
(0...𝑁) = (0..^(𝑁 + 1))) |
69 | 68 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑁 ∈ ℤ →
(0..^(𝑁 + 1)) = (0...𝑁)) |
70 | 34, 69 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑁 ∈ ℕ0
→ (0..^(𝑁 + 1)) =
(0...𝑁)) |
71 | 70 | eleq2d 2823 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈ ℕ0
→ ((𝑖 + 1) ∈
(0..^(𝑁 + 1)) ↔ (𝑖 + 1) ∈ (0...𝑁))) |
72 | 71 | ad2antll 729 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) → ((𝑖 + 1) ∈ (0..^(𝑁 + 1)) ↔ (𝑖 + 1) ∈ (0...𝑁))) |
73 | 72 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑖 + 1) ∈ (0..^(𝑁 + 1)) ↔ (𝑖 + 1) ∈ (0...𝑁))) |
74 | 67, 73 | mpbird 260 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑖 + 1) ∈ (0..^(𝑁 + 1))) |
75 | | pfxfv 14247 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (𝑁 + 1) ∈ (0...(♯‘𝑊)) ∧ (𝑖 + 1) ∈ (0..^(𝑁 + 1))) → ((𝑊 prefix (𝑁 + 1))‘(𝑖 + 1)) = (𝑊‘(𝑖 + 1))) |
76 | 47, 58, 74, 75 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑊 prefix (𝑁 + 1))‘(𝑖 + 1)) = (𝑊‘(𝑖 + 1))) |
77 | 76 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑊‘(𝑖 + 1)) = ((𝑊 prefix (𝑁 + 1))‘(𝑖 + 1))) |
78 | 65, 77 | preq12d 4657 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} = {((𝑊 prefix (𝑁 + 1))‘𝑖), ((𝑊 prefix (𝑁 + 1))‘(𝑖 + 1))}) |
79 | 78 | eleq1d 2822 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → ({(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {((𝑊 prefix (𝑁 + 1))‘𝑖), ((𝑊 prefix (𝑁 + 1))‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
80 | 79 | biimpd 232 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → ({(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) → {((𝑊 prefix (𝑁 + 1))‘𝑖), ((𝑊 prefix (𝑁 + 1))‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
81 | 80 | ralimdva 3100 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) →
(∀𝑖 ∈
(0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ (0..^𝑁){((𝑊 prefix (𝑁 + 1))‘𝑖), ((𝑊 prefix (𝑁 + 1))‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
82 | 46, 81 | syld 47 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) →
(∀𝑖 ∈
(0..^(𝑁 + 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ (0..^𝑁){((𝑊 prefix (𝑁 + 1))‘𝑖), ((𝑊 prefix (𝑁 + 1))‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
83 | 33, 82 | sylbid 243 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) →
(∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ (0..^𝑁){((𝑊 prefix (𝑁 + 1))‘𝑖), ((𝑊 prefix (𝑁 + 1))‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
84 | 83 | imp 410 |
. . . . . . . . . . . . . . 15
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧
∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ∀𝑖 ∈ (0..^𝑁){((𝑊 prefix (𝑁 + 1))‘𝑖), ((𝑊 prefix (𝑁 + 1))‘(𝑖 + 1))} ∈ (Edg‘𝐺)) |
85 | | nn0cn 12100 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℂ) |
86 | 85, 28 | pncand 11190 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 + 1) − 1)
= 𝑁) |
87 | 86 | oveq2d 7229 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ0
→ (0..^((𝑁 + 1)
− 1)) = (0..^𝑁)) |
88 | 87 | ad2antll 729 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) →
(0..^((𝑁 + 1) − 1)) =
(0..^𝑁)) |
89 | 88 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧
∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → (0..^((𝑁 + 1) − 1)) = (0..^𝑁)) |
90 | 89 | raleqdv 3325 |
. . . . . . . . . . . . . . 15
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧
∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → (∀𝑖 ∈ (0..^((𝑁 + 1) − 1)){((𝑊 prefix (𝑁 + 1))‘𝑖), ((𝑊 prefix (𝑁 + 1))‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^𝑁){((𝑊 prefix (𝑁 + 1))‘𝑖), ((𝑊 prefix (𝑁 + 1))‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
91 | 84, 90 | mpbird 260 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧
∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ∀𝑖 ∈ (0..^((𝑁 + 1) − 1)){((𝑊 prefix (𝑁 + 1))‘𝑖), ((𝑊 prefix (𝑁 + 1))‘(𝑖 + 1))} ∈ (Edg‘𝐺)) |
92 | | pfxlen 14248 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (𝑁 + 1) ∈ (0...(♯‘𝑊))) → (♯‘(𝑊 prefix (𝑁 + 1))) = (𝑁 + 1)) |
93 | 57, 92 | syldan 594 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) →
(♯‘(𝑊 prefix
(𝑁 + 1))) = (𝑁 + 1)) |
94 | 93 | oveq1d 7228 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) →
((♯‘(𝑊 prefix
(𝑁 + 1))) − 1) =
((𝑁 + 1) −
1)) |
95 | 94 | oveq2d 7229 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) →
(0..^((♯‘(𝑊
prefix (𝑁 + 1))) −
1)) = (0..^((𝑁 + 1) −
1))) |
96 | 95 | raleqdv 3325 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) →
(∀𝑖 ∈
(0..^((♯‘(𝑊
prefix (𝑁 + 1))) −
1)){((𝑊 prefix (𝑁 + 1))‘𝑖), ((𝑊 prefix (𝑁 + 1))‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^((𝑁 + 1) − 1)){((𝑊 prefix (𝑁 + 1))‘𝑖), ((𝑊 prefix (𝑁 + 1))‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
97 | 96 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧
∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → (∀𝑖 ∈ (0..^((♯‘(𝑊 prefix (𝑁 + 1))) − 1)){((𝑊 prefix (𝑁 + 1))‘𝑖), ((𝑊 prefix (𝑁 + 1))‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^((𝑁 + 1) − 1)){((𝑊 prefix (𝑁 + 1))‘𝑖), ((𝑊 prefix (𝑁 + 1))‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
98 | 91, 97 | mpbird 260 |
. . . . . . . . . . . . 13
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧
∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ∀𝑖 ∈ (0..^((♯‘(𝑊 prefix (𝑁 + 1))) − 1)){((𝑊 prefix (𝑁 + 1))‘𝑖), ((𝑊 prefix (𝑁 + 1))‘(𝑖 + 1))} ∈ (Edg‘𝐺)) |
99 | 98 | exp31 423 |
. . . . . . . . . . . 12
⊢ (𝑊 ∈ Word (Vtx‘𝐺) → (((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0) →
(∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ (0..^((♯‘(𝑊 prefix (𝑁 + 1))) − 1)){((𝑊 prefix (𝑁 + 1))‘𝑖), ((𝑊 prefix (𝑁 + 1))‘(𝑖 + 1))} ∈ (Edg‘𝐺)))) |
100 | 99 | com23 86 |
. . . . . . . . . . 11
⊢ (𝑊 ∈ Word (Vtx‘𝐺) → (∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) → (((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0) →
∀𝑖 ∈
(0..^((♯‘(𝑊
prefix (𝑁 + 1))) −
1)){((𝑊 prefix (𝑁 + 1))‘𝑖), ((𝑊 prefix (𝑁 + 1))‘(𝑖 + 1))} ∈ (Edg‘𝐺)))) |
101 | 100 | imp 410 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → (((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0) →
∀𝑖 ∈
(0..^((♯‘(𝑊
prefix (𝑁 + 1))) −
1)){((𝑊 prefix (𝑁 + 1))‘𝑖), ((𝑊 prefix (𝑁 + 1))‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
102 | 101 | 3adant1 1132 |
. . . . . . . . 9
⊢ ((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → (((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0) →
∀𝑖 ∈
(0..^((♯‘(𝑊
prefix (𝑁 + 1))) −
1)){((𝑊 prefix (𝑁 + 1))‘𝑖), ((𝑊 prefix (𝑁 + 1))‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
103 | 102 | expdimp 456 |
. . . . . . . 8
⊢ (((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1)) → (𝑁 ∈ ℕ0 →
∀𝑖 ∈
(0..^((♯‘(𝑊
prefix (𝑁 + 1))) −
1)){((𝑊 prefix (𝑁 + 1))‘𝑖), ((𝑊 prefix (𝑁 + 1))‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
104 | 103 | impcom 411 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑊 ≠ ∅
∧ 𝑊 ∈ Word
(Vtx‘𝐺) ∧
∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1))) → ∀𝑖 ∈
(0..^((♯‘(𝑊
prefix (𝑁 + 1))) −
1)){((𝑊 prefix (𝑁 + 1))‘𝑖), ((𝑊 prefix (𝑁 + 1))‘(𝑖 + 1))} ∈ (Edg‘𝐺)) |
105 | 4, 5 | iswwlks 27920 |
. . . . . . 7
⊢ ((𝑊 prefix (𝑁 + 1)) ∈ (WWalks‘𝐺) ↔ ((𝑊 prefix (𝑁 + 1)) ≠ ∅ ∧ (𝑊 prefix (𝑁 + 1)) ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘(𝑊
prefix (𝑁 + 1))) −
1)){((𝑊 prefix (𝑁 + 1))‘𝑖), ((𝑊 prefix (𝑁 + 1))‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
106 | 21, 25, 104, 105 | syl3anbrc 1345 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑊 ≠ ∅
∧ 𝑊 ∈ Word
(Vtx‘𝐺) ∧
∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1))) → (𝑊 prefix (𝑁 + 1)) ∈ (WWalks‘𝐺)) |
107 | | peano2nn0 12130 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 + 1) ∈ ℕ0
→ ((𝑁 + 1) + 1) ∈
ℕ0) |
108 | 1, 107 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 + 1) + 1) ∈
ℕ0) |
109 | | elfz2nn0 13203 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 + 1) ∈ (0...((𝑁 + 1) + 1)) ↔ ((𝑁 + 1) ∈ ℕ0
∧ ((𝑁 + 1) + 1) ∈
ℕ0 ∧ (𝑁 + 1) ≤ ((𝑁 + 1) + 1))) |
110 | 1, 108, 11, 109 | syl3anbrc 1345 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
(0...((𝑁 + 1) +
1))) |
111 | 110 | adantl 485 |
. . . . . . . . . . . . 13
⊢
(((♯‘𝑊)
= ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)
→ (𝑁 + 1) ∈
(0...((𝑁 + 1) +
1))) |
112 | 111, 55 | mpbird 260 |
. . . . . . . . . . . 12
⊢
(((♯‘𝑊)
= ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)
→ (𝑁 + 1) ∈
(0...(♯‘𝑊))) |
113 | 112 | anim2i 620 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) → (𝑊 ∈ Word (Vtx‘𝐺) ∧ (𝑁 + 1) ∈ (0...(♯‘𝑊)))) |
114 | 113 | exp32 424 |
. . . . . . . . . 10
⊢ (𝑊 ∈ Word (Vtx‘𝐺) → ((♯‘𝑊) = ((𝑁 + 1) + 1) → (𝑁 ∈ ℕ0 → (𝑊 ∈ Word (Vtx‘𝐺) ∧ (𝑁 + 1) ∈ (0...(♯‘𝑊)))))) |
115 | 114 | 3ad2ant2 1136 |
. . . . . . . . 9
⊢ ((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ((♯‘𝑊) = ((𝑁 + 1) + 1) → (𝑁 ∈ ℕ0 → (𝑊 ∈ Word (Vtx‘𝐺) ∧ (𝑁 + 1) ∈ (0...(♯‘𝑊)))))) |
116 | 115 | imp 410 |
. . . . . . . 8
⊢ (((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1)) → (𝑁 ∈ ℕ0 → (𝑊 ∈ Word (Vtx‘𝐺) ∧ (𝑁 + 1) ∈ (0...(♯‘𝑊))))) |
117 | 116 | impcom 411 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑊 ≠ ∅
∧ 𝑊 ∈ Word
(Vtx‘𝐺) ∧
∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1))) → (𝑊 ∈ Word (Vtx‘𝐺) ∧ (𝑁 + 1) ∈ (0...(♯‘𝑊)))) |
118 | 117, 92 | syl 17 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑊 ≠ ∅
∧ 𝑊 ∈ Word
(Vtx‘𝐺) ∧
∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1))) → (♯‘(𝑊 prefix (𝑁 + 1))) = (𝑁 + 1)) |
119 | | iswwlksn 27922 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ ((𝑊 prefix (𝑁 + 1)) ∈ (𝑁 WWalksN 𝐺) ↔ ((𝑊 prefix (𝑁 + 1)) ∈ (WWalks‘𝐺) ∧ (♯‘(𝑊 prefix (𝑁 + 1))) = (𝑁 + 1)))) |
120 | 119 | adantr 484 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑊 ≠ ∅
∧ 𝑊 ∈ Word
(Vtx‘𝐺) ∧
∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1))) → ((𝑊 prefix (𝑁 + 1)) ∈ (𝑁 WWalksN 𝐺) ↔ ((𝑊 prefix (𝑁 + 1)) ∈ (WWalks‘𝐺) ∧ (♯‘(𝑊 prefix (𝑁 + 1))) = (𝑁 + 1)))) |
121 | 106, 118,
120 | mpbir2and 713 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑊 ≠ ∅
∧ 𝑊 ∈ Word
(Vtx‘𝐺) ∧
∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1))) → (𝑊 prefix (𝑁 + 1)) ∈ (𝑁 WWalksN 𝐺)) |
122 | 121 | expcom 417 |
. . . 4
⊢ (((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1)) → (𝑁 ∈ ℕ0 → (𝑊 prefix (𝑁 + 1)) ∈ (𝑁 WWalksN 𝐺))) |
123 | 6, 122 | sylanb 584 |
. . 3
⊢ ((𝑊 ∈ (WWalks‘𝐺) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1)) → (𝑁 ∈ ℕ0 → (𝑊 prefix (𝑁 + 1)) ∈ (𝑁 WWalksN 𝐺))) |
124 | 123 | com12 32 |
. 2
⊢ (𝑁 ∈ ℕ0
→ ((𝑊 ∈
(WWalks‘𝐺) ∧
(♯‘𝑊) = ((𝑁 + 1) + 1)) → (𝑊 prefix (𝑁 + 1)) ∈ (𝑁 WWalksN 𝐺))) |
125 | 3, 124 | sylbid 243 |
1
⊢ (𝑁 ∈ ℕ0
→ (𝑊 ∈ ((𝑁 + 1) WWalksN 𝐺) → (𝑊 prefix (𝑁 + 1)) ∈ (𝑁 WWalksN 𝐺))) |