| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | wwlknbp1 29865 | . . 3
⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) | 
| 2 |  | clwwlkext2edg.v | . . . . . . . . . . . . 13
⊢ 𝑉 = (Vtx‘𝐺) | 
| 3 | 2 | wrdeqi 14576 | . . . . . . . . . . . 12
⊢ Word
𝑉 = Word (Vtx‘𝐺) | 
| 4 | 3 | eleq2i 2832 | . . . . . . . . . . 11
⊢ (𝑊 ∈ Word 𝑉 ↔ 𝑊 ∈ Word (Vtx‘𝐺)) | 
| 5 | 4 | biimpri 228 | . . . . . . . . . 10
⊢ (𝑊 ∈ Word (Vtx‘𝐺) → 𝑊 ∈ Word 𝑉) | 
| 6 | 5 | 3ad2ant2 1134 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑊 ∈ Word
(Vtx‘𝐺) ∧
(♯‘𝑊) = (𝑁 + 1)) → 𝑊 ∈ Word 𝑉) | 
| 7 | 6 | ad2antlr 727 | . . . . . . . 8
⊢ (((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) → 𝑊 ∈ Word 𝑉) | 
| 8 |  | s1cl 14641 | . . . . . . . . 9
⊢ (𝑍 ∈ 𝑉 → 〈“𝑍”〉 ∈ Word 𝑉) | 
| 9 | 8 | adantl 481 | . . . . . . . 8
⊢ (((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) → 〈“𝑍”〉 ∈ Word 𝑉) | 
| 10 |  | ccatcl 14613 | . . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 〈“𝑍”〉 ∈ Word 𝑉) → (𝑊 ++ 〈“𝑍”〉) ∈ Word 𝑉) | 
| 11 | 7, 9, 10 | syl2anc 584 | . . . . . . 7
⊢ (((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) → (𝑊 ++ 〈“𝑍”〉) ∈ Word 𝑉) | 
| 12 | 11 | adantr 480 | . . . . . 6
⊢ ((((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) ∧ ({(lastS‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸)) → (𝑊 ++ 〈“𝑍”〉) ∈ Word 𝑉) | 
| 13 |  | clwwlkext2edg.e | . . . . . . . . . 10
⊢ 𝐸 = (Edg‘𝐺) | 
| 14 | 2, 13 | wwlknp 29864 | . . . . . . . . 9
⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸)) | 
| 15 |  | simplll 774 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑊 ∈ Word 𝑉) | 
| 16 | 8 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) →
〈“𝑍”〉
∈ Word 𝑉) | 
| 17 | 16 | ad2antlr 727 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → 〈“𝑍”〉 ∈ Word 𝑉) | 
| 18 |  | elfzo0 13741 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑖 ∈ (0..^𝑁) ↔ (𝑖 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝑖 < 𝑁)) | 
| 19 |  | simp1 1136 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑖 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝑖 < 𝑁) → 𝑖 ∈ ℕ0) | 
| 20 |  | peano2nn 12279 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈
ℕ) | 
| 21 | 20 | 3ad2ant2 1134 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑖 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝑖 < 𝑁) → (𝑁 + 1) ∈ ℕ) | 
| 22 |  | nn0re 12537 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑖 ∈ ℕ0
→ 𝑖 ∈
ℝ) | 
| 23 | 22 | 3ad2ant1 1133 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑖 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝑖 < 𝑁) → 𝑖 ∈ ℝ) | 
| 24 |  | nnre 12274 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) | 
| 25 | 24 | 3ad2ant2 1134 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑖 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝑖 < 𝑁) → 𝑁 ∈ ℝ) | 
| 26 |  | peano2re 11435 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑁 ∈ ℝ → (𝑁 + 1) ∈
ℝ) | 
| 27 | 24, 26 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈
ℝ) | 
| 28 | 27 | 3ad2ant2 1134 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑖 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝑖 < 𝑁) → (𝑁 + 1) ∈ ℝ) | 
| 29 |  | simp3 1138 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑖 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝑖 < 𝑁) → 𝑖 < 𝑁) | 
| 30 | 24 | ltp1d 12199 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑁 ∈ ℕ → 𝑁 < (𝑁 + 1)) | 
| 31 | 30 | 3ad2ant2 1134 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑖 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝑖 < 𝑁) → 𝑁 < (𝑁 + 1)) | 
| 32 | 23, 25, 28, 29, 31 | lttrd 11423 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑖 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝑖 < 𝑁) → 𝑖 < (𝑁 + 1)) | 
| 33 |  | elfzo0 13741 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑖 ∈ (0..^(𝑁 + 1)) ↔ (𝑖 ∈ ℕ0 ∧ (𝑁 + 1) ∈ ℕ ∧ 𝑖 < (𝑁 + 1))) | 
| 34 | 19, 21, 32, 33 | syl3anbrc 1343 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑖 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝑖 < 𝑁) → 𝑖 ∈ (0..^(𝑁 + 1))) | 
| 35 | 18, 34 | sylbi 217 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑖 ∈ (0..^𝑁) → 𝑖 ∈ (0..^(𝑁 + 1))) | 
| 36 | 35 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑖 ∈ (0..^(𝑁 + 1))) | 
| 37 |  | oveq2 7440 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
((♯‘𝑊) =
(𝑁 + 1) →
(0..^(♯‘𝑊)) =
(0..^(𝑁 +
1))) | 
| 38 | 37 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) → (0..^(♯‘𝑊)) = (0..^(𝑁 + 1))) | 
| 39 | 38 | eleq2d 2826 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) → (𝑖 ∈ (0..^(♯‘𝑊)) ↔ 𝑖 ∈ (0..^(𝑁 + 1)))) | 
| 40 | 39 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑖 ∈ (0..^(♯‘𝑊)) ↔ 𝑖 ∈ (0..^(𝑁 + 1)))) | 
| 41 | 36, 40 | mpbird 257 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑖 ∈ (0..^(♯‘𝑊))) | 
| 42 |  | ccatval1 14616 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑊 ∈ Word 𝑉 ∧ 〈“𝑍”〉 ∈ Word 𝑉 ∧ 𝑖 ∈ (0..^(♯‘𝑊))) → ((𝑊 ++ 〈“𝑍”〉)‘𝑖) = (𝑊‘𝑖)) | 
| 43 | 15, 17, 41, 42 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑊 ++ 〈“𝑍”〉)‘𝑖) = (𝑊‘𝑖)) | 
| 44 |  | fzonn0p1p1 13784 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑖 ∈ (0..^𝑁) → (𝑖 + 1) ∈ (0..^(𝑁 + 1))) | 
| 45 | 44 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑖 + 1) ∈ (0..^(𝑁 + 1))) | 
| 46 | 37 | eleq2d 2826 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((♯‘𝑊) =
(𝑁 + 1) → ((𝑖 + 1) ∈
(0..^(♯‘𝑊))
↔ (𝑖 + 1) ∈
(0..^(𝑁 +
1)))) | 
| 47 | 46 | ad3antlr 731 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑖 + 1) ∈ (0..^(♯‘𝑊)) ↔ (𝑖 + 1) ∈ (0..^(𝑁 + 1)))) | 
| 48 | 45, 47 | mpbird 257 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑖 + 1) ∈ (0..^(♯‘𝑊))) | 
| 49 |  | ccatval1 14616 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑊 ∈ Word 𝑉 ∧ 〈“𝑍”〉 ∈ Word 𝑉 ∧ (𝑖 + 1) ∈ (0..^(♯‘𝑊))) → ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1)) = (𝑊‘(𝑖 + 1))) | 
| 50 | 15, 17, 48, 49 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1)) = (𝑊‘(𝑖 + 1))) | 
| 51 | 43, 50 | preq12d 4740 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → {((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} = {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))}) | 
| 52 | 51 | ex 412 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → (𝑖 ∈ (0..^𝑁) → {((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} = {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))})) | 
| 53 | 52 | expcom 413 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) → (𝑖 ∈ (0..^𝑁) → {((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} = {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))}))) | 
| 54 | 53 | expcom 413 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ ℕ0
→ (𝑍 ∈ 𝑉 → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) → (𝑖 ∈ (0..^𝑁) → {((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} = {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))})))) | 
| 55 | 54 | 3ad2ant1 1133 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑁 ∈ ℕ0
∧ 𝑊 ∈ Word
(Vtx‘𝐺) ∧
(♯‘𝑊) = (𝑁 + 1)) → (𝑍 ∈ 𝑉 → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) → (𝑖 ∈ (0..^𝑁) → {((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} = {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))})))) | 
| 56 | 55 | imp 406 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑁 ∈ ℕ0
∧ 𝑊 ∈ Word
(Vtx‘𝐺) ∧
(♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉) → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) → (𝑖 ∈ (0..^𝑁) → {((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} = {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))}))) | 
| 57 | 56 | expdcom 414 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑊 ∈ Word 𝑉 → ((♯‘𝑊) = (𝑁 + 1) → (((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉) → (𝑖 ∈ (0..^𝑁) → {((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} = {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))})))) | 
| 58 | 57 | 3imp1 1347 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ 𝑖 ∈ (0..^𝑁)) → {((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} = {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))}) | 
| 59 | 58 | eleq1d 2825 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ 𝑖 ∈ (0..^𝑁)) → ({((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸 ↔ {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸)) | 
| 60 | 59 | ralbidva 3175 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) → (∀𝑖 ∈ (0..^𝑁){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸 ↔ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸)) | 
| 61 | 60 | biimprd 248 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) → (∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 → ∀𝑖 ∈ (0..^𝑁){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸)) | 
| 62 | 61 | 3exp 1119 | . . . . . . . . . . . . . . . 16
⊢ (𝑊 ∈ Word 𝑉 → ((♯‘𝑊) = (𝑁 + 1) → (((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉) → (∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 → ∀𝑖 ∈ (0..^𝑁){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸)))) | 
| 63 | 62 | com34 91 | . . . . . . . . . . . . . . 15
⊢ (𝑊 ∈ Word 𝑉 → ((♯‘𝑊) = (𝑁 + 1) → (∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 → (((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉) → ∀𝑖 ∈ (0..^𝑁){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸)))) | 
| 64 | 63 | 3imp1 1347 | . . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) → ∀𝑖 ∈ (0..^𝑁){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸) | 
| 65 | 64 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → ∀𝑖 ∈ (0..^𝑁){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸) | 
| 66 |  | simpll 766 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → 𝑊 ∈ Word 𝑉) | 
| 67 | 8 | ad2antrl 728 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) →
〈“𝑍”〉
∈ Word 𝑉) | 
| 68 |  | nn0p1gt0 12557 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑁 ∈ ℕ0
→ 0 < (𝑁 +
1)) | 
| 69 | 68 | ad2antll 729 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → 0 <
(𝑁 + 1)) | 
| 70 |  | breq2 5146 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((♯‘𝑊) =
(𝑁 + 1) → (0 <
(♯‘𝑊) ↔ 0
< (𝑁 +
1))) | 
| 71 | 70 | ad2antlr 727 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → (0 <
(♯‘𝑊) ↔ 0
< (𝑁 +
1))) | 
| 72 | 69, 71 | mpbird 257 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → 0 <
(♯‘𝑊)) | 
| 73 |  | hashneq0 14404 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑊 ∈ Word 𝑉 → (0 < (♯‘𝑊) ↔ 𝑊 ≠ ∅)) | 
| 74 | 73 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → (0 <
(♯‘𝑊) ↔
𝑊 ≠
∅)) | 
| 75 | 72, 74 | mpbid 232 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → 𝑊 ≠ ∅) | 
| 76 |  | ccatval1lsw 14623 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑊 ∈ Word 𝑉 ∧ 〈“𝑍”〉 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → ((𝑊 ++ 〈“𝑍”〉)‘((♯‘𝑊) − 1)) =
(lastS‘𝑊)) | 
| 77 | 66, 67, 75, 76 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → ((𝑊 ++ 〈“𝑍”〉)‘((♯‘𝑊) − 1)) =
(lastS‘𝑊)) | 
| 78 |  | oveq1 7439 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((♯‘𝑊) =
(𝑁 + 1) →
((♯‘𝑊) −
1) = ((𝑁 + 1) −
1)) | 
| 79 | 78 | ad2antlr 727 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) →
((♯‘𝑊) −
1) = ((𝑁 + 1) −
1)) | 
| 80 |  | nn0cn 12538 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℂ) | 
| 81 | 80 | ad2antll 729 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → 𝑁 ∈
ℂ) | 
| 82 |  | pncan1 11688 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑁 ∈ ℂ → ((𝑁 + 1) − 1) = 𝑁) | 
| 83 | 81, 82 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → ((𝑁 + 1) − 1) = 𝑁) | 
| 84 | 79, 83 | eqtrd 2776 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) →
((♯‘𝑊) −
1) = 𝑁) | 
| 85 | 84 | fveq2d 6909 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → ((𝑊 ++ 〈“𝑍”〉)‘((♯‘𝑊) − 1)) = ((𝑊 ++ 〈“𝑍”〉)‘𝑁)) | 
| 86 | 77, 85 | eqtr3d 2778 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) →
(lastS‘𝑊) = ((𝑊 ++ 〈“𝑍”〉)‘𝑁)) | 
| 87 |  | ccatws1ls 14672 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉) → ((𝑊 ++ 〈“𝑍”〉)‘(♯‘𝑊)) = 𝑍) | 
| 88 | 87 | ad2ant2r 747 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → ((𝑊 ++ 〈“𝑍”〉)‘(♯‘𝑊)) = 𝑍) | 
| 89 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((♯‘𝑊) =
(𝑁 + 1) → ((𝑊 ++ 〈“𝑍”〉)‘(♯‘𝑊)) = ((𝑊 ++ 〈“𝑍”〉)‘(𝑁 + 1))) | 
| 90 | 89 | ad2antlr 727 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → ((𝑊 ++ 〈“𝑍”〉)‘(♯‘𝑊)) = ((𝑊 ++ 〈“𝑍”〉)‘(𝑁 + 1))) | 
| 91 | 88, 90 | eqtr3d 2778 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → 𝑍 = ((𝑊 ++ 〈“𝑍”〉)‘(𝑁 + 1))) | 
| 92 | 86, 91 | preq12d 4740 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) →
{(lastS‘𝑊), 𝑍} = {((𝑊 ++ 〈“𝑍”〉)‘𝑁), ((𝑊 ++ 〈“𝑍”〉)‘(𝑁 + 1))}) | 
| 93 | 92 | expcom 413 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) → {(lastS‘𝑊), 𝑍} = {((𝑊 ++ 〈“𝑍”〉)‘𝑁), ((𝑊 ++ 〈“𝑍”〉)‘(𝑁 + 1))})) | 
| 94 | 93 | expcom 413 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ0
→ (𝑍 ∈ 𝑉 → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) → {(lastS‘𝑊), 𝑍} = {((𝑊 ++ 〈“𝑍”〉)‘𝑁), ((𝑊 ++ 〈“𝑍”〉)‘(𝑁 + 1))}))) | 
| 95 | 94 | 3ad2ant1 1133 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈ ℕ0
∧ 𝑊 ∈ Word
(Vtx‘𝐺) ∧
(♯‘𝑊) = (𝑁 + 1)) → (𝑍 ∈ 𝑉 → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) → {(lastS‘𝑊), 𝑍} = {((𝑊 ++ 〈“𝑍”〉)‘𝑁), ((𝑊 ++ 〈“𝑍”〉)‘(𝑁 + 1))}))) | 
| 96 | 95 | imp 406 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ℕ0
∧ 𝑊 ∈ Word
(Vtx‘𝐺) ∧
(♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉) → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) → {(lastS‘𝑊), 𝑍} = {((𝑊 ++ 〈“𝑍”〉)‘𝑁), ((𝑊 ++ 〈“𝑍”〉)‘(𝑁 + 1))})) | 
| 97 | 96 | com12 32 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) → (((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉) → {(lastS‘𝑊), 𝑍} = {((𝑊 ++ 〈“𝑍”〉)‘𝑁), ((𝑊 ++ 〈“𝑍”〉)‘(𝑁 + 1))})) | 
| 98 | 97 | 3adant3 1132 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) → (((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉) → {(lastS‘𝑊), 𝑍} = {((𝑊 ++ 〈“𝑍”〉)‘𝑁), ((𝑊 ++ 〈“𝑍”〉)‘(𝑁 + 1))})) | 
| 99 | 98 | imp 406 | . . . . . . . . . . . . . . . 16
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) → {(lastS‘𝑊), 𝑍} = {((𝑊 ++ 〈“𝑍”〉)‘𝑁), ((𝑊 ++ 〈“𝑍”〉)‘(𝑁 + 1))}) | 
| 100 | 99 | eleq1d 2825 | . . . . . . . . . . . . . . 15
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) → ({(lastS‘𝑊), 𝑍} ∈ 𝐸 ↔ {((𝑊 ++ 〈“𝑍”〉)‘𝑁), ((𝑊 ++ 〈“𝑍”〉)‘(𝑁 + 1))} ∈ 𝐸)) | 
| 101 | 100 | biimpa 476 | . . . . . . . . . . . . . 14
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → {((𝑊 ++ 〈“𝑍”〉)‘𝑁), ((𝑊 ++ 〈“𝑍”〉)‘(𝑁 + 1))} ∈ 𝐸) | 
| 102 |  | simprl1 1218 | . . . . . . . . . . . . . . . 16
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) → 𝑁 ∈
ℕ0) | 
| 103 | 102 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → 𝑁 ∈
ℕ0) | 
| 104 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑖 = 𝑁 → ((𝑊 ++ 〈“𝑍”〉)‘𝑖) = ((𝑊 ++ 〈“𝑍”〉)‘𝑁)) | 
| 105 |  | fvoveq1 7455 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑖 = 𝑁 → ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1)) = ((𝑊 ++ 〈“𝑍”〉)‘(𝑁 + 1))) | 
| 106 | 104, 105 | preq12d 4740 | . . . . . . . . . . . . . . . . 17
⊢ (𝑖 = 𝑁 → {((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} = {((𝑊 ++ 〈“𝑍”〉)‘𝑁), ((𝑊 ++ 〈“𝑍”〉)‘(𝑁 + 1))}) | 
| 107 | 106 | eleq1d 2825 | . . . . . . . . . . . . . . . 16
⊢ (𝑖 = 𝑁 → ({((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸 ↔ {((𝑊 ++ 〈“𝑍”〉)‘𝑁), ((𝑊 ++ 〈“𝑍”〉)‘(𝑁 + 1))} ∈ 𝐸)) | 
| 108 | 107 | ralsng 4674 | . . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ0
→ (∀𝑖 ∈
{𝑁} {((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸 ↔ {((𝑊 ++ 〈“𝑍”〉)‘𝑁), ((𝑊 ++ 〈“𝑍”〉)‘(𝑁 + 1))} ∈ 𝐸)) | 
| 109 | 103, 108 | syl 17 | . . . . . . . . . . . . . 14
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → (∀𝑖 ∈ {𝑁} {((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸 ↔ {((𝑊 ++ 〈“𝑍”〉)‘𝑁), ((𝑊 ++ 〈“𝑍”〉)‘(𝑁 + 1))} ∈ 𝐸)) | 
| 110 | 101, 109 | mpbird 257 | . . . . . . . . . . . . 13
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → ∀𝑖 ∈ {𝑁} {((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸) | 
| 111 |  | ralunb 4196 | . . . . . . . . . . . . 13
⊢
(∀𝑖 ∈
((0..^𝑁) ∪ {𝑁}){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸 ↔ (∀𝑖 ∈ (0..^𝑁){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸 ∧ ∀𝑖 ∈ {𝑁} {((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸)) | 
| 112 | 65, 110, 111 | sylanbrc 583 | . . . . . . . . . . . 12
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → ∀𝑖 ∈ ((0..^𝑁) ∪ {𝑁}){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸) | 
| 113 |  | elnn0uz 12924 | . . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ0
↔ 𝑁 ∈
(ℤ≥‘0)) | 
| 114 | 102, 113 | sylib 218 | . . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) → 𝑁 ∈
(ℤ≥‘0)) | 
| 115 | 114 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → 𝑁 ∈
(ℤ≥‘0)) | 
| 116 |  | fzosplitsn 13815 | . . . . . . . . . . . . 13
⊢ (𝑁 ∈
(ℤ≥‘0) → (0..^(𝑁 + 1)) = ((0..^𝑁) ∪ {𝑁})) | 
| 117 | 115, 116 | syl 17 | . . . . . . . . . . . 12
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → (0..^(𝑁 + 1)) = ((0..^𝑁) ∪ {𝑁})) | 
| 118 | 112, 117 | raleqtrrdv 3329 | . . . . . . . . . . 11
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → ∀𝑖 ∈ (0..^(𝑁 + 1)){((𝑊 ++ 〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸) | 
| 119 |  | ccatws1len 14659 | . . . . . . . . . . . . . . . 16
⊢ (𝑊 ∈ Word 𝑉 → (♯‘(𝑊 ++ 〈“𝑍”〉)) = ((♯‘𝑊) + 1)) | 
| 120 | 119 | 3ad2ant1 1133 | . . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) → (♯‘(𝑊 ++ 〈“𝑍”〉)) = ((♯‘𝑊) + 1)) | 
| 121 | 120 | ad2antrr 726 | . . . . . . . . . . . . . 14
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → (♯‘(𝑊 ++ 〈“𝑍”〉)) = ((♯‘𝑊) + 1)) | 
| 122 | 121 | oveq1d 7447 | . . . . . . . . . . . . 13
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → ((♯‘(𝑊 ++ 〈“𝑍”〉)) − 1) =
(((♯‘𝑊) + 1)
− 1)) | 
| 123 |  | oveq1 7439 | . . . . . . . . . . . . . . . . 17
⊢
((♯‘𝑊) =
(𝑁 + 1) →
((♯‘𝑊) + 1) =
((𝑁 + 1) +
1)) | 
| 124 | 123 | oveq1d 7447 | . . . . . . . . . . . . . . . 16
⊢
((♯‘𝑊) =
(𝑁 + 1) →
(((♯‘𝑊) + 1)
− 1) = (((𝑁 + 1) + 1)
− 1)) | 
| 125 |  | 1cnd 11257 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ0
→ 1 ∈ ℂ) | 
| 126 | 80, 125 | addcld 11281 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℂ) | 
| 127 | 126, 125 | pncand 11622 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ0
→ (((𝑁 + 1) + 1)
− 1) = (𝑁 +
1)) | 
| 128 | 127 | 3ad2ant1 1133 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℕ0
∧ 𝑊 ∈ Word
(Vtx‘𝐺) ∧
(♯‘𝑊) = (𝑁 + 1)) → (((𝑁 + 1) + 1) − 1) = (𝑁 + 1)) | 
| 129 | 128 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ0
∧ 𝑊 ∈ Word
(Vtx‘𝐺) ∧
(♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉) → (((𝑁 + 1) + 1) − 1) = (𝑁 + 1)) | 
| 130 | 124, 129 | sylan9eq 2796 | . . . . . . . . . . . . . . 15
⊢
(((♯‘𝑊)
= (𝑁 + 1) ∧ ((𝑁 ∈ ℕ0
∧ 𝑊 ∈ Word
(Vtx‘𝐺) ∧
(♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) → (((♯‘𝑊) + 1) − 1) = (𝑁 + 1)) | 
| 131 | 130 | 3ad2antl2 1186 | . . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) → (((♯‘𝑊) + 1) − 1) = (𝑁 + 1)) | 
| 132 | 131 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → (((♯‘𝑊) + 1) − 1) = (𝑁 + 1)) | 
| 133 | 122, 132 | eqtrd 2776 | . . . . . . . . . . . 12
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → ((♯‘(𝑊 ++ 〈“𝑍”〉)) − 1) = (𝑁 + 1)) | 
| 134 | 133 | oveq2d 7448 | . . . . . . . . . . 11
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → (0..^((♯‘(𝑊 ++ 〈“𝑍”〉)) − 1)) =
(0..^(𝑁 +
1))) | 
| 135 | 118, 134 | raleqtrrdv 3329 | . . . . . . . . . 10
⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → ∀𝑖 ∈ (0..^((♯‘(𝑊 ++ 〈“𝑍”〉)) −
1)){((𝑊 ++
〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸) | 
| 136 | 135 | exp42 435 | . . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) → ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) → (𝑍 ∈ 𝑉 → ({(lastS‘𝑊), 𝑍} ∈ 𝐸 → ∀𝑖 ∈ (0..^((♯‘(𝑊 ++ 〈“𝑍”〉)) −
1)){((𝑊 ++
〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸)))) | 
| 137 | 14, 136 | syl 17 | . . . . . . . 8
⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) → (𝑍 ∈ 𝑉 → ({(lastS‘𝑊), 𝑍} ∈ 𝐸 → ∀𝑖 ∈ (0..^((♯‘(𝑊 ++ 〈“𝑍”〉)) −
1)){((𝑊 ++
〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸)))) | 
| 138 | 137 | imp41 425 | . . . . . . 7
⊢ ((((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → ∀𝑖 ∈ (0..^((♯‘(𝑊 ++ 〈“𝑍”〉)) −
1)){((𝑊 ++
〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸) | 
| 139 | 138 | adantrr 717 | . . . . . 6
⊢ ((((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) ∧ ({(lastS‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸)) → ∀𝑖 ∈ (0..^((♯‘(𝑊 ++ 〈“𝑍”〉)) −
1)){((𝑊 ++
〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸) | 
| 140 |  | lswccats1 14673 | . . . . . . . . . . . 12
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉) → (lastS‘(𝑊 ++ 〈“𝑍”〉)) = 𝑍) | 
| 141 | 7, 140 | sylancom 588 | . . . . . . . . . . 11
⊢ (((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) → (lastS‘(𝑊 ++ 〈“𝑍”〉)) = 𝑍) | 
| 142 | 68 | 3ad2ant1 1133 | . . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ0
∧ 𝑊 ∈ Word
(Vtx‘𝐺) ∧
(♯‘𝑊) = (𝑁 + 1)) → 0 < (𝑁 + 1)) | 
| 143 | 70 | 3ad2ant3 1135 | . . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ0
∧ 𝑊 ∈ Word
(Vtx‘𝐺) ∧
(♯‘𝑊) = (𝑁 + 1)) → (0 <
(♯‘𝑊) ↔ 0
< (𝑁 +
1))) | 
| 144 | 142, 143 | mpbird 257 | . . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ 𝑊 ∈ Word
(Vtx‘𝐺) ∧
(♯‘𝑊) = (𝑁 + 1)) → 0 <
(♯‘𝑊)) | 
| 145 | 144 | ad2antlr 727 | . . . . . . . . . . . 12
⊢ (((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) → 0 < (♯‘𝑊)) | 
| 146 |  | ccatfv0 14622 | . . . . . . . . . . . 12
⊢ ((𝑊 ∈ Word 𝑉 ∧ 〈“𝑍”〉 ∈ Word 𝑉 ∧ 0 < (♯‘𝑊)) → ((𝑊 ++ 〈“𝑍”〉)‘0) = (𝑊‘0)) | 
| 147 | 7, 9, 145, 146 | syl3anc 1372 | . . . . . . . . . . 11
⊢ (((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) → ((𝑊 ++ 〈“𝑍”〉)‘0) = (𝑊‘0)) | 
| 148 | 141, 147 | preq12d 4740 | . . . . . . . . . 10
⊢ (((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) → {(lastS‘(𝑊 ++ 〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)} = {𝑍, (𝑊‘0)}) | 
| 149 | 148 | eleq1d 2825 | . . . . . . . . 9
⊢ (((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) → ({(lastS‘(𝑊 ++ 〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)} ∈ 𝐸 ↔ {𝑍, (𝑊‘0)} ∈ 𝐸)) | 
| 150 | 149 | biimprcd 250 | . . . . . . . 8
⊢ ({𝑍, (𝑊‘0)} ∈ 𝐸 → (((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) → {(lastS‘(𝑊 ++ 〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)} ∈ 𝐸)) | 
| 151 | 150 | adantl 481 | . . . . . . 7
⊢
(({(lastS‘𝑊),
𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸) → (((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) → {(lastS‘(𝑊 ++ 〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)} ∈ 𝐸)) | 
| 152 | 151 | impcom 407 | . . . . . 6
⊢ ((((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) ∧ ({(lastS‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸)) → {(lastS‘(𝑊 ++ 〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)} ∈ 𝐸) | 
| 153 | 12, 139, 152 | 3jca 1128 | . . . . 5
⊢ ((((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) ∧ ({(lastS‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸)) → ((𝑊 ++ 〈“𝑍”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑊 ++ 〈“𝑍”〉)) −
1)){((𝑊 ++
〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘(𝑊 ++ 〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)} ∈ 𝐸)) | 
| 154 |  | ccatws1len 14659 | . . . . . . . 8
⊢ (𝑊 ∈ Word (Vtx‘𝐺) → (♯‘(𝑊 ++ 〈“𝑍”〉)) =
((♯‘𝑊) +
1)) | 
| 155 | 154 | 3ad2ant2 1134 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑊 ∈ Word
(Vtx‘𝐺) ∧
(♯‘𝑊) = (𝑁 + 1)) →
(♯‘(𝑊 ++
〈“𝑍”〉)) = ((♯‘𝑊) + 1)) | 
| 156 | 123 | 3ad2ant3 1135 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑊 ∈ Word
(Vtx‘𝐺) ∧
(♯‘𝑊) = (𝑁 + 1)) →
((♯‘𝑊) + 1) =
((𝑁 + 1) +
1)) | 
| 157 | 80, 125, 125 | addassd 11284 | . . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 + 1) + 1) =
(𝑁 + (1 +
1))) | 
| 158 |  | 1p1e2 12392 | . . . . . . . . . 10
⊢ (1 + 1) =
2 | 
| 159 | 158 | oveq2i 7443 | . . . . . . . . 9
⊢ (𝑁 + (1 + 1)) = (𝑁 + 2) | 
| 160 | 157, 159 | eqtrdi 2792 | . . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 + 1) + 1) =
(𝑁 + 2)) | 
| 161 | 160 | 3ad2ant1 1133 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑊 ∈ Word
(Vtx‘𝐺) ∧
(♯‘𝑊) = (𝑁 + 1)) → ((𝑁 + 1) + 1) = (𝑁 + 2)) | 
| 162 | 155, 156,
161 | 3eqtrd 2780 | . . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑊 ∈ Word
(Vtx‘𝐺) ∧
(♯‘𝑊) = (𝑁 + 1)) →
(♯‘(𝑊 ++
〈“𝑍”〉)) = (𝑁 + 2)) | 
| 163 | 162 | ad3antlr 731 | . . . . 5
⊢ ((((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) ∧ ({(lastS‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸)) → (♯‘(𝑊 ++ 〈“𝑍”〉)) = (𝑁 + 2)) | 
| 164 |  | 2nn 12340 | . . . . . . . . 9
⊢ 2 ∈
ℕ | 
| 165 |  | nn0nnaddcl 12559 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 2 ∈ ℕ) → (𝑁 + 2) ∈ ℕ) | 
| 166 | 164, 165 | mpan2 691 | . . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 2) ∈
ℕ) | 
| 167 | 166 | 3ad2ant1 1133 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑊 ∈ Word
(Vtx‘𝐺) ∧
(♯‘𝑊) = (𝑁 + 1)) → (𝑁 + 2) ∈ ℕ) | 
| 168 | 2, 13 | isclwwlknx 30056 | . . . . . . 7
⊢ ((𝑁 + 2) ∈ ℕ →
((𝑊 ++ 〈“𝑍”〉) ∈ ((𝑁 + 2) ClWWalksN 𝐺) ↔ (((𝑊 ++ 〈“𝑍”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑊 ++ 〈“𝑍”〉)) −
1)){((𝑊 ++
〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘(𝑊 ++ 〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)} ∈ 𝐸) ∧ (♯‘(𝑊 ++ 〈“𝑍”〉)) = (𝑁 + 2)))) | 
| 169 | 167, 168 | syl 17 | . . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑊 ∈ Word
(Vtx‘𝐺) ∧
(♯‘𝑊) = (𝑁 + 1)) → ((𝑊 ++ 〈“𝑍”〉) ∈ ((𝑁 + 2) ClWWalksN 𝐺) ↔ (((𝑊 ++ 〈“𝑍”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑊 ++ 〈“𝑍”〉)) −
1)){((𝑊 ++
〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘(𝑊 ++ 〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)} ∈ 𝐸) ∧ (♯‘(𝑊 ++ 〈“𝑍”〉)) = (𝑁 + 2)))) | 
| 170 | 169 | ad3antlr 731 | . . . . 5
⊢ ((((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) ∧ ({(lastS‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸)) → ((𝑊 ++ 〈“𝑍”〉) ∈ ((𝑁 + 2) ClWWalksN 𝐺) ↔ (((𝑊 ++ 〈“𝑍”〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑊 ++ 〈“𝑍”〉)) −
1)){((𝑊 ++
〈“𝑍”〉)‘𝑖), ((𝑊 ++ 〈“𝑍”〉)‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘(𝑊 ++ 〈“𝑍”〉)), ((𝑊 ++ 〈“𝑍”〉)‘0)} ∈ 𝐸) ∧ (♯‘(𝑊 ++ 〈“𝑍”〉)) = (𝑁 + 2)))) | 
| 171 | 153, 163,
170 | mpbir2and 713 | . . . 4
⊢ ((((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) ∧ ({(lastS‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸)) → (𝑊 ++ 〈“𝑍”〉) ∈ ((𝑁 + 2) ClWWalksN 𝐺)) | 
| 172 | 171 | exp31 419 | . . 3
⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) → (𝑍 ∈ 𝑉 → (({(lastS‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸) → (𝑊 ++ 〈“𝑍”〉) ∈ ((𝑁 + 2) ClWWalksN 𝐺)))) | 
| 173 | 1, 172 | mpdan 687 | . 2
⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → (𝑍 ∈ 𝑉 → (({(lastS‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸) → (𝑊 ++ 〈“𝑍”〉) ∈ ((𝑁 + 2) ClWWalksN 𝐺)))) | 
| 174 | 173 | imp 406 | 1
⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ 𝑍 ∈ 𝑉) → (({(lastS‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸) → (𝑊 ++ 〈“𝑍”〉) ∈ ((𝑁 + 2) ClWWalksN 𝐺))) |