| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | peano2nn0 12566 | . . 3
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ0) | 
| 2 |  | iswwlksn 29858 | . . 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 29856 | . . . 4
⊢ (𝑊 ∈ (WWalks‘𝐺) ↔ (𝑊 ≠ ∅ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺))) | 
| 7 |  | simp1 1137 | . . . . . . . . . . . 12
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0) → 𝑊 ∈ Word (Vtx‘𝐺)) | 
| 8 |  | nn0p1nn 12565 | . . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ) | 
| 9 | 8 | 3ad2ant3 1136 | . . . . . . . . . . . 12
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0) → (𝑁 + 1) ∈
ℕ) | 
| 10 | 1 | nn0red 12588 | . . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℝ) | 
| 11 | 10 | lep1d 12199 | . . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ≤ ((𝑁 + 1) + 1)) | 
| 12 | 11 | 3ad2ant3 1136 | . . . . . . . . . . . . 13
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0) → (𝑁 + 1) ≤ ((𝑁 + 1) + 1)) | 
| 13 |  | breq2 5147 | . . . . . . . . . . . . . 14
⊢
((♯‘𝑊) =
((𝑁 + 1) + 1) →
((𝑁 + 1) ≤
(♯‘𝑊) ↔
(𝑁 + 1) ≤ ((𝑁 + 1) + 1))) | 
| 14 | 13 | 3ad2ant2 1135 | . . . . . . . . . . . . 13
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0) → ((𝑁 + 1) ≤ (♯‘𝑊) ↔ (𝑁 + 1) ≤ ((𝑁 + 1) + 1))) | 
| 15 | 12, 14 | mpbird 257 | . . . . . . . . . . . 12
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0) → (𝑁 + 1) ≤ (♯‘𝑊)) | 
| 16 |  | pfxn0 14724 | . . . . . . . . . . . 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 1120 | . . . . . . . . . 10
⊢ (𝑊 ∈ Word (Vtx‘𝐺) → ((♯‘𝑊) = ((𝑁 + 1) + 1) → (𝑁 ∈ ℕ0 → (𝑊 prefix (𝑁 + 1)) ≠ ∅))) | 
| 19 | 18 | 3ad2ant2 1135 | . . . . . . . . 9
⊢ ((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ((♯‘𝑊) = ((𝑁 + 1) + 1) → (𝑁 ∈ ℕ0 → (𝑊 prefix (𝑁 + 1)) ≠ ∅))) | 
| 20 | 19 | imp 406 | . . . . . . . 8
⊢ (((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1)) → (𝑁 ∈ ℕ0 → (𝑊 prefix (𝑁 + 1)) ≠ ∅)) | 
| 21 | 20 | impcom 407 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑊 ≠ ∅
∧ 𝑊 ∈ Word
(Vtx‘𝐺) ∧
∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1))) → (𝑊 prefix (𝑁 + 1)) ≠ ∅) | 
| 22 |  | pfxcl 14715 | . . . . . . . . . 10
⊢ (𝑊 ∈ Word (Vtx‘𝐺) → (𝑊 prefix (𝑁 + 1)) ∈ Word (Vtx‘𝐺)) | 
| 23 | 22 | 3ad2ant2 1135 | . . . . . . . . 9
⊢ ((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → (𝑊 prefix (𝑁 + 1)) ∈ Word (Vtx‘𝐺)) | 
| 24 | 23 | adantr 480 | . . . . . . . 8
⊢ (((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1)) → (𝑊 prefix (𝑁 + 1)) ∈ Word (Vtx‘𝐺)) | 
| 25 | 24 | adantl 481 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑊 ≠ ∅
∧ 𝑊 ∈ Word
(Vtx‘𝐺) ∧
∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1))) → (𝑊 prefix (𝑁 + 1)) ∈ Word (Vtx‘𝐺)) | 
| 26 |  | oveq1 7438 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((♯‘𝑊) =
((𝑁 + 1) + 1) →
((♯‘𝑊) −
1) = (((𝑁 + 1) + 1) −
1)) | 
| 27 | 1 | nn0cnd 12589 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℂ) | 
| 28 |  | 1cnd 11256 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈ ℕ0
→ 1 ∈ ℂ) | 
| 29 | 27, 28 | pncand 11621 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ0
→ (((𝑁 + 1) + 1)
− 1) = (𝑁 +
1)) | 
| 30 | 26, 29 | sylan9eq 2797 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((♯‘𝑊)
= ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)
→ ((♯‘𝑊)
− 1) = (𝑁 +
1)) | 
| 31 | 30 | oveq2d 7447 | . . . . . . . . . . . . . . . . . . 19
⊢
(((♯‘𝑊)
= ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)
→ (0..^((♯‘𝑊) − 1)) = (0..^(𝑁 + 1))) | 
| 32 | 31 | raleqdv 3326 | . . . . . . . . . . . . . . . . . 18
⊢
(((♯‘𝑊)
= ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)
→ (∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^(𝑁 + 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺))) | 
| 33 | 32 | adantl 481 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) →
(∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^(𝑁 + 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺))) | 
| 34 |  | nn0z 12638 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℤ) | 
| 35 |  | nn0z 12638 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑁 + 1) ∈ ℕ0
→ (𝑁 + 1) ∈
ℤ) | 
| 36 | 1, 35 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℤ) | 
| 37 |  | nn0re 12535 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ) | 
| 38 | 37 | lep1d 12199 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ≤ (𝑁 + 1)) | 
| 39 | 34, 36, 38 | 3jca 1129 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈ ℕ0
→ (𝑁 ∈ ℤ
∧ (𝑁 + 1) ∈
ℤ ∧ 𝑁 ≤ (𝑁 + 1))) | 
| 40 | 39 | ad2antll 729 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) → (𝑁 ∈ ℤ ∧ (𝑁 + 1) ∈ ℤ ∧ 𝑁 ≤ (𝑁 + 1))) | 
| 41 |  | eluz2 12884 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 + 1) ∈
(ℤ≥‘𝑁) ↔ (𝑁 ∈ ℤ ∧ (𝑁 + 1) ∈ ℤ ∧ 𝑁 ≤ (𝑁 + 1))) | 
| 42 | 40, 41 | sylibr 234 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) → (𝑁 + 1) ∈
(ℤ≥‘𝑁)) | 
| 43 |  | fzoss2 13727 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 + 1) ∈
(ℤ≥‘𝑁) → (0..^𝑁) ⊆ (0..^(𝑁 + 1))) | 
| 44 | 42, 43 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) →
(0..^𝑁) ⊆ (0..^(𝑁 + 1))) | 
| 45 |  | ssralv 4052 | . . . . . . . . . . . . . . . . . . 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 13665 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑁 + 1) ∈ ℕ0
↔ (𝑁 + 1) ∈
(0...(𝑁 +
1))) | 
| 49 | 1, 48 | sylib 218 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
(0...(𝑁 +
1))) | 
| 50 | 49 | ad2antll 729 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) → (𝑁 + 1) ∈ (0...(𝑁 + 1))) | 
| 51 |  | fzelp1 13616 | . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7439 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((♯‘𝑊) =
((𝑁 + 1) + 1) →
(0...(♯‘𝑊)) =
(0...((𝑁 + 1) +
1))) | 
| 54 | 53 | eleq2d 2827 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((♯‘𝑊) =
((𝑁 + 1) + 1) →
((𝑁 + 1) ∈
(0...(♯‘𝑊))
↔ (𝑁 + 1) ∈
(0...((𝑁 + 1) +
1)))) | 
| 55 | 54 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((♯‘𝑊)
= ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)
→ ((𝑁 + 1) ∈
(0...(♯‘𝑊))
↔ (𝑁 + 1) ∈
(0...((𝑁 + 1) +
1)))) | 
| 56 | 55 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) → ((𝑁 + 1) ∈
(0...(♯‘𝑊))
↔ (𝑁 + 1) ∈
(0...((𝑁 + 1) +
1)))) | 
| 57 | 52, 56 | mpbird 257 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) → (𝑁 + 1) ∈
(0...(♯‘𝑊))) | 
| 58 | 57 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑁 + 1) ∈ (0...(♯‘𝑊))) | 
| 59 |  | fzossfzop1 13782 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈ ℕ0
→ (0..^𝑁) ⊆
(0..^(𝑁 +
1))) | 
| 60 | 59 | sseld 3982 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ ℕ0
→ (𝑖 ∈ (0..^𝑁) → 𝑖 ∈ (0..^(𝑁 + 1)))) | 
| 61 | 60 | ad2antll 729 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) → (𝑖 ∈ (0..^𝑁) → 𝑖 ∈ (0..^(𝑁 + 1)))) | 
| 62 | 61 | imp 406 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑖 ∈ (0..^(𝑁 + 1))) | 
| 63 |  | pfxfv 14720 | . . . . . . . . . . . . . . . . . . . . . . . 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 13803 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑖 ∈ (0..^𝑁) → (𝑖 + 1) ∈ (0...𝑁)) | 
| 67 | 66 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑖 + 1) ∈ (0...𝑁)) | 
| 68 |  | fzval3 13773 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
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 2827 | . . . . . . . . . . . . . . . . . . . . . . . . . . 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 480 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑖 + 1) ∈ (0..^(𝑁 + 1)) ↔ (𝑖 + 1) ∈ (0...𝑁))) | 
| 74 | 67, 73 | mpbird 257 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑖 + 1) ∈ (0..^(𝑁 + 1))) | 
| 75 |  | pfxfv 14720 | . . . . . . . . . . . . . . . . . . . . . . . 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 4741 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} = {((𝑊 prefix (𝑁 + 1))‘𝑖), ((𝑊 prefix (𝑁 + 1))‘(𝑖 + 1))}) | 
| 79 | 78 | eleq1d 2826 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → ({(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {((𝑊 prefix (𝑁 + 1))‘𝑖), ((𝑊 prefix (𝑁 + 1))‘(𝑖 + 1))} ∈ (Edg‘𝐺))) | 
| 80 | 79 | biimpd 229 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → ({(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) → {((𝑊 prefix (𝑁 + 1))‘𝑖), ((𝑊 prefix (𝑁 + 1))‘(𝑖 + 1))} ∈ (Edg‘𝐺))) | 
| 81 | 80 | ralimdva 3167 | . . . . . . . . . . . . . . . . . 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 240 | . . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) →
(∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ (0..^𝑁){((𝑊 prefix (𝑁 + 1))‘𝑖), ((𝑊 prefix (𝑁 + 1))‘(𝑖 + 1))} ∈ (Edg‘𝐺))) | 
| 84 | 83 | imp 406 | . . . . . . . . . . . . . . 15
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧
∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ∀𝑖 ∈ (0..^𝑁){((𝑊 prefix (𝑁 + 1))‘𝑖), ((𝑊 prefix (𝑁 + 1))‘(𝑖 + 1))} ∈ (Edg‘𝐺)) | 
| 85 |  | nn0cn 12536 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℂ) | 
| 86 | 85, 28 | pncand 11621 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 + 1) − 1)
= 𝑁) | 
| 87 | 86 | oveq2d 7447 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ0
→ (0..^((𝑁 + 1)
− 1)) = (0..^𝑁)) | 
| 88 | 87 | ad2antll 729 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) →
(0..^((𝑁 + 1) − 1)) =
(0..^𝑁)) | 
| 89 | 88 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧
∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → (0..^((𝑁 + 1) − 1)) = (0..^𝑁)) | 
| 90 | 89 | raleqdv 3326 | . . . . . . . . . . . . . . 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 257 | . . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧
∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ∀𝑖 ∈ (0..^((𝑁 + 1) − 1)){((𝑊 prefix (𝑁 + 1))‘𝑖), ((𝑊 prefix (𝑁 + 1))‘(𝑖 + 1))} ∈ (Edg‘𝐺)) | 
| 92 |  | pfxlen 14721 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (𝑁 + 1) ∈ (0...(♯‘𝑊))) → (♯‘(𝑊 prefix (𝑁 + 1))) = (𝑁 + 1)) | 
| 93 | 57, 92 | syldan 591 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) →
(♯‘(𝑊 prefix
(𝑁 + 1))) = (𝑁 + 1)) | 
| 94 | 93 | oveq1d 7446 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) →
((♯‘(𝑊 prefix
(𝑁 + 1))) − 1) =
((𝑁 + 1) −
1)) | 
| 95 | 94 | oveq2d 7447 | . . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) →
(0..^((♯‘(𝑊
prefix (𝑁 + 1))) −
1)) = (0..^((𝑁 + 1) −
1))) | 
| 96 | 95 | raleqdv 3326 | . . . . . . . . . . . . . . 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 480 | . . . . . . . . . . . . . 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 257 | . . . . . . . . . . . . 13
⊢ (((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) ∧
∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ∀𝑖 ∈ (0..^((♯‘(𝑊 prefix (𝑁 + 1))) − 1)){((𝑊 prefix (𝑁 + 1))‘𝑖), ((𝑊 prefix (𝑁 + 1))‘(𝑖 + 1))} ∈ (Edg‘𝐺)) | 
| 99 | 98 | exp31 419 | . . . . . . . . . . . 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 406 | . . . . . . . . . 10
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → (((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0) →
∀𝑖 ∈
(0..^((♯‘(𝑊
prefix (𝑁 + 1))) −
1)){((𝑊 prefix (𝑁 + 1))‘𝑖), ((𝑊 prefix (𝑁 + 1))‘(𝑖 + 1))} ∈ (Edg‘𝐺))) | 
| 102 | 101 | 3adant1 1131 | . . . . . . . . 9
⊢ ((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → (((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0) →
∀𝑖 ∈
(0..^((♯‘(𝑊
prefix (𝑁 + 1))) −
1)){((𝑊 prefix (𝑁 + 1))‘𝑖), ((𝑊 prefix (𝑁 + 1))‘(𝑖 + 1))} ∈ (Edg‘𝐺))) | 
| 103 | 102 | expdimp 452 | . . . . . . . 8
⊢ (((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1)) → (𝑁 ∈ ℕ0 →
∀𝑖 ∈
(0..^((♯‘(𝑊
prefix (𝑁 + 1))) −
1)){((𝑊 prefix (𝑁 + 1))‘𝑖), ((𝑊 prefix (𝑁 + 1))‘(𝑖 + 1))} ∈ (Edg‘𝐺))) | 
| 104 | 103 | impcom 407 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑊 ≠ ∅
∧ 𝑊 ∈ Word
(Vtx‘𝐺) ∧
∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1))) → ∀𝑖 ∈
(0..^((♯‘(𝑊
prefix (𝑁 + 1))) −
1)){((𝑊 prefix (𝑁 + 1))‘𝑖), ((𝑊 prefix (𝑁 + 1))‘(𝑖 + 1))} ∈ (Edg‘𝐺)) | 
| 105 | 4, 5 | iswwlks 29856 | . . . . . . 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 1344 | . . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ ((𝑊 ≠ ∅
∧ 𝑊 ∈ Word
(Vtx‘𝐺) ∧
∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1))) → (𝑊 prefix (𝑁 + 1)) ∈ (WWalks‘𝐺)) | 
| 107 |  | peano2nn0 12566 | . . . . . . . . . . . . . . . 16
⊢ ((𝑁 + 1) ∈ ℕ0
→ ((𝑁 + 1) + 1) ∈
ℕ0) | 
| 108 | 1, 107 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 + 1) + 1) ∈
ℕ0) | 
| 109 |  | elfz2nn0 13658 | . . . . . . . . . . . . . . 15
⊢ ((𝑁 + 1) ∈ (0...((𝑁 + 1) + 1)) ↔ ((𝑁 + 1) ∈ ℕ0
∧ ((𝑁 + 1) + 1) ∈
ℕ0 ∧ (𝑁 + 1) ≤ ((𝑁 + 1) + 1))) | 
| 110 | 1, 108, 11, 109 | syl3anbrc 1344 | . . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
(0...((𝑁 + 1) +
1))) | 
| 111 | 110 | adantl 481 | . . . . . . . . . . . . 13
⊢
(((♯‘𝑊)
= ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)
→ (𝑁 + 1) ∈
(0...((𝑁 + 1) +
1))) | 
| 112 | 111, 55 | mpbird 257 | . . . . . . . . . . . 12
⊢
(((♯‘𝑊)
= ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)
→ (𝑁 + 1) ∈
(0...(♯‘𝑊))) | 
| 113 | 112 | anim2i 617 | . . . . . . . . . . 11
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ ((♯‘𝑊) = ((𝑁 + 1) + 1) ∧ 𝑁 ∈ ℕ0)) → (𝑊 ∈ Word (Vtx‘𝐺) ∧ (𝑁 + 1) ∈ (0...(♯‘𝑊)))) | 
| 114 | 113 | exp32 420 | . . . . . . . . . 10
⊢ (𝑊 ∈ Word (Vtx‘𝐺) → ((♯‘𝑊) = ((𝑁 + 1) + 1) → (𝑁 ∈ ℕ0 → (𝑊 ∈ Word (Vtx‘𝐺) ∧ (𝑁 + 1) ∈ (0...(♯‘𝑊)))))) | 
| 115 | 114 | 3ad2ant2 1135 | . . . . . . . . 9
⊢ ((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ((♯‘𝑊) = ((𝑁 + 1) + 1) → (𝑁 ∈ ℕ0 → (𝑊 ∈ Word (Vtx‘𝐺) ∧ (𝑁 + 1) ∈ (0...(♯‘𝑊)))))) | 
| 116 | 115 | imp 406 | . . . . . . . 8
⊢ (((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1)) → (𝑁 ∈ ℕ0 → (𝑊 ∈ Word (Vtx‘𝐺) ∧ (𝑁 + 1) ∈ (0...(♯‘𝑊))))) | 
| 117 | 116 | impcom 407 | . . . . . . 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 29858 | . . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ ((𝑊 prefix (𝑁 + 1)) ∈ (𝑁 WWalksN 𝐺) ↔ ((𝑊 prefix (𝑁 + 1)) ∈ (WWalks‘𝐺) ∧ (♯‘(𝑊 prefix (𝑁 + 1))) = (𝑁 + 1)))) | 
| 120 | 119 | adantr 480 | . . . . . 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 413 | . . . 4
⊢ (((𝑊 ≠ ∅ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈
(0..^((♯‘𝑊)
− 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1)) → (𝑁 ∈ ℕ0 → (𝑊 prefix (𝑁 + 1)) ∈ (𝑁 WWalksN 𝐺))) | 
| 123 | 6, 122 | sylanb 581 | . . 3
⊢ ((𝑊 ∈ (WWalks‘𝐺) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1)) → (𝑁 ∈ ℕ0 → (𝑊 prefix (𝑁 + 1)) ∈ (𝑁 WWalksN 𝐺))) | 
| 124 | 123 | com12 32 | . 2
⊢ (𝑁 ∈ ℕ0
→ ((𝑊 ∈
(WWalks‘𝐺) ∧
(♯‘𝑊) = ((𝑁 + 1) + 1)) → (𝑊 prefix (𝑁 + 1)) ∈ (𝑁 WWalksN 𝐺))) | 
| 125 | 3, 124 | sylbid 240 | 1
⊢ (𝑁 ∈ ℕ0
→ (𝑊 ∈ ((𝑁 + 1) WWalksN 𝐺) → (𝑊 prefix (𝑁 + 1)) ∈ (𝑁 WWalksN 𝐺))) |