MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  wwlksext2clwwlk Structured version   Visualization version   GIF version

Theorem wwlksext2clwwlk 29854
Description: If a word represents a walk in (in a graph) and there are edges between the last vertex of the word and another vertex and between this other vertex and the first vertex of the word, then the concatenation of the word representing the walk with this other vertex represents a closed walk. (Contributed by Alexander van der Vekens, 3-Oct-2018.) (Revised by AV, 27-Apr-2021.) (Revised by AV, 14-Mar-2022.)
Hypotheses
Ref Expression
clwwlkext2edg.v 𝑉 = (Vtxβ€˜πΊ)
clwwlkext2edg.e 𝐸 = (Edgβ€˜πΊ)
Assertion
Ref Expression
wwlksext2clwwlk ((π‘Š ∈ (𝑁 WWalksN 𝐺) ∧ 𝑍 ∈ 𝑉) β†’ (({(lastSβ€˜π‘Š), 𝑍} ∈ 𝐸 ∧ {𝑍, (π‘Šβ€˜0)} ∈ 𝐸) β†’ (π‘Š ++ βŸ¨β€œπ‘β€βŸ©) ∈ ((𝑁 + 2) ClWWalksN 𝐺)))

Proof of Theorem wwlksext2clwwlk
Dummy variable 𝑖 is distinct from all other variables.
StepHypRef Expression
1 wwlknbp1 29642 . . 3 (π‘Š ∈ (𝑁 WWalksN 𝐺) β†’ (𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1)))
2 clwwlkext2edg.v . . . . . . . . . . . . 13 𝑉 = (Vtxβ€˜πΊ)
32wrdeqi 14511 . . . . . . . . . . . 12 Word 𝑉 = Word (Vtxβ€˜πΊ)
43eleq2i 2820 . . . . . . . . . . 11 (π‘Š ∈ Word 𝑉 ↔ π‘Š ∈ Word (Vtxβ€˜πΊ))
54biimpri 227 . . . . . . . . . 10 (π‘Š ∈ Word (Vtxβ€˜πΊ) β†’ π‘Š ∈ Word 𝑉)
653ad2ant2 1132 . . . . . . . . 9 ((𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) β†’ π‘Š ∈ Word 𝑉)
76ad2antlr 726 . . . . . . . 8 (((π‘Š ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) β†’ π‘Š ∈ Word 𝑉)
8 s1cl 14576 . . . . . . . . 9 (𝑍 ∈ 𝑉 β†’ βŸ¨β€œπ‘β€βŸ© ∈ Word 𝑉)
98adantl 481 . . . . . . . 8 (((π‘Š ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) β†’ βŸ¨β€œπ‘β€βŸ© ∈ Word 𝑉)
10 ccatcl 14548 . . . . . . . 8 ((π‘Š ∈ Word 𝑉 ∧ βŸ¨β€œπ‘β€βŸ© ∈ Word 𝑉) β†’ (π‘Š ++ βŸ¨β€œπ‘β€βŸ©) ∈ Word 𝑉)
117, 9, 10syl2anc 583 . . . . . . 7 (((π‘Š ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) β†’ (π‘Š ++ βŸ¨β€œπ‘β€βŸ©) ∈ Word 𝑉)
1211adantr 480 . . . . . 6 ((((π‘Š ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) ∧ ({(lastSβ€˜π‘Š), 𝑍} ∈ 𝐸 ∧ {𝑍, (π‘Šβ€˜0)} ∈ 𝐸)) β†’ (π‘Š ++ βŸ¨β€œπ‘β€βŸ©) ∈ Word 𝑉)
13 clwwlkext2edg.e . . . . . . . . . 10 𝐸 = (Edgβ€˜πΊ)
142, 13wwlknp 29641 . . . . . . . . 9 (π‘Š ∈ (𝑁 WWalksN 𝐺) β†’ (π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1) ∧ βˆ€π‘– ∈ (0..^𝑁){(π‘Šβ€˜π‘–), (π‘Šβ€˜(𝑖 + 1))} ∈ 𝐸))
15 simplll 774 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ β„•0)) ∧ 𝑖 ∈ (0..^𝑁)) β†’ π‘Š ∈ Word 𝑉)
168adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ β„•0) β†’ βŸ¨β€œπ‘β€βŸ© ∈ Word 𝑉)
1716ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ β„•0)) ∧ 𝑖 ∈ (0..^𝑁)) β†’ βŸ¨β€œπ‘β€βŸ© ∈ Word 𝑉)
18 elfzo0 13697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑖 ∈ (0..^𝑁) ↔ (𝑖 ∈ β„•0 ∧ 𝑁 ∈ β„• ∧ 𝑖 < 𝑁))
19 simp1 1134 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑖 ∈ β„•0 ∧ 𝑁 ∈ β„• ∧ 𝑖 < 𝑁) β†’ 𝑖 ∈ β„•0)
20 peano2nn 12246 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑁 ∈ β„• β†’ (𝑁 + 1) ∈ β„•)
21203ad2ant2 1132 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑖 ∈ β„•0 ∧ 𝑁 ∈ β„• ∧ 𝑖 < 𝑁) β†’ (𝑁 + 1) ∈ β„•)
22 nn0re 12503 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑖 ∈ β„•0 β†’ 𝑖 ∈ ℝ)
23223ad2ant1 1131 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑖 ∈ β„•0 ∧ 𝑁 ∈ β„• ∧ 𝑖 < 𝑁) β†’ 𝑖 ∈ ℝ)
24 nnre 12241 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑁 ∈ β„• β†’ 𝑁 ∈ ℝ)
25243ad2ant2 1132 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑖 ∈ β„•0 ∧ 𝑁 ∈ β„• ∧ 𝑖 < 𝑁) β†’ 𝑁 ∈ ℝ)
26 peano2re 11409 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑁 ∈ ℝ β†’ (𝑁 + 1) ∈ ℝ)
2724, 26syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑁 ∈ β„• β†’ (𝑁 + 1) ∈ ℝ)
28273ad2ant2 1132 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑖 ∈ β„•0 ∧ 𝑁 ∈ β„• ∧ 𝑖 < 𝑁) β†’ (𝑁 + 1) ∈ ℝ)
29 simp3 1136 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑖 ∈ β„•0 ∧ 𝑁 ∈ β„• ∧ 𝑖 < 𝑁) β†’ 𝑖 < 𝑁)
3024ltp1d 12166 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑁 ∈ β„• β†’ 𝑁 < (𝑁 + 1))
31303ad2ant2 1132 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑖 ∈ β„•0 ∧ 𝑁 ∈ β„• ∧ 𝑖 < 𝑁) β†’ 𝑁 < (𝑁 + 1))
3223, 25, 28, 29, 31lttrd 11397 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑖 ∈ β„•0 ∧ 𝑁 ∈ β„• ∧ 𝑖 < 𝑁) β†’ 𝑖 < (𝑁 + 1))
33 elfzo0 13697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑖 ∈ (0..^(𝑁 + 1)) ↔ (𝑖 ∈ β„•0 ∧ (𝑁 + 1) ∈ β„• ∧ 𝑖 < (𝑁 + 1)))
3419, 21, 32, 33syl3anbrc 1341 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑖 ∈ β„•0 ∧ 𝑁 ∈ β„• ∧ 𝑖 < 𝑁) β†’ 𝑖 ∈ (0..^(𝑁 + 1)))
3518, 34sylbi 216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑖 ∈ (0..^𝑁) β†’ 𝑖 ∈ (0..^(𝑁 + 1)))
3635adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ β„•0)) ∧ 𝑖 ∈ (0..^𝑁)) β†’ 𝑖 ∈ (0..^(𝑁 + 1)))
37 oveq2 7422 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((β™―β€˜π‘Š) = (𝑁 + 1) β†’ (0..^(β™―β€˜π‘Š)) = (0..^(𝑁 + 1)))
3837adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) β†’ (0..^(β™―β€˜π‘Š)) = (0..^(𝑁 + 1)))
3938eleq2d 2814 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) β†’ (𝑖 ∈ (0..^(β™―β€˜π‘Š)) ↔ 𝑖 ∈ (0..^(𝑁 + 1))))
4039ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ β„•0)) ∧ 𝑖 ∈ (0..^𝑁)) β†’ (𝑖 ∈ (0..^(β™―β€˜π‘Š)) ↔ 𝑖 ∈ (0..^(𝑁 + 1))))
4136, 40mpbird 257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ β„•0)) ∧ 𝑖 ∈ (0..^𝑁)) β†’ 𝑖 ∈ (0..^(β™―β€˜π‘Š)))
42 ccatval1 14551 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((π‘Š ∈ Word 𝑉 ∧ βŸ¨β€œπ‘β€βŸ© ∈ Word 𝑉 ∧ 𝑖 ∈ (0..^(β™―β€˜π‘Š))) β†’ ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘–) = (π‘Šβ€˜π‘–))
4315, 17, 41, 42syl3anc 1369 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ β„•0)) ∧ 𝑖 ∈ (0..^𝑁)) β†’ ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘–) = (π‘Šβ€˜π‘–))
44 fzonn0p1p1 13735 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑖 ∈ (0..^𝑁) β†’ (𝑖 + 1) ∈ (0..^(𝑁 + 1)))
4544adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ β„•0)) ∧ 𝑖 ∈ (0..^𝑁)) β†’ (𝑖 + 1) ∈ (0..^(𝑁 + 1)))
4637eleq2d 2814 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((β™―β€˜π‘Š) = (𝑁 + 1) β†’ ((𝑖 + 1) ∈ (0..^(β™―β€˜π‘Š)) ↔ (𝑖 + 1) ∈ (0..^(𝑁 + 1))))
4746ad3antlr 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ β„•0)) ∧ 𝑖 ∈ (0..^𝑁)) β†’ ((𝑖 + 1) ∈ (0..^(β™―β€˜π‘Š)) ↔ (𝑖 + 1) ∈ (0..^(𝑁 + 1))))
4845, 47mpbird 257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ β„•0)) ∧ 𝑖 ∈ (0..^𝑁)) β†’ (𝑖 + 1) ∈ (0..^(β™―β€˜π‘Š)))
49 ccatval1 14551 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((π‘Š ∈ Word 𝑉 ∧ βŸ¨β€œπ‘β€βŸ© ∈ Word 𝑉 ∧ (𝑖 + 1) ∈ (0..^(β™―β€˜π‘Š))) β†’ ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑖 + 1)) = (π‘Šβ€˜(𝑖 + 1)))
5015, 17, 48, 49syl3anc 1369 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ β„•0)) ∧ 𝑖 ∈ (0..^𝑁)) β†’ ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑖 + 1)) = (π‘Šβ€˜(𝑖 + 1)))
5143, 50preq12d 4741 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ β„•0)) ∧ 𝑖 ∈ (0..^𝑁)) β†’ {((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘–), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑖 + 1))} = {(π‘Šβ€˜π‘–), (π‘Šβ€˜(𝑖 + 1))})
5251ex 412 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ β„•0)) β†’ (𝑖 ∈ (0..^𝑁) β†’ {((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘–), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑖 + 1))} = {(π‘Šβ€˜π‘–), (π‘Šβ€˜(𝑖 + 1))}))
5352expcom 413 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ β„•0) β†’ ((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) β†’ (𝑖 ∈ (0..^𝑁) β†’ {((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘–), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑖 + 1))} = {(π‘Šβ€˜π‘–), (π‘Šβ€˜(𝑖 + 1))})))
5453expcom 413 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ β„•0 β†’ (𝑍 ∈ 𝑉 β†’ ((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) β†’ (𝑖 ∈ (0..^𝑁) β†’ {((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘–), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑖 + 1))} = {(π‘Šβ€˜π‘–), (π‘Šβ€˜(𝑖 + 1))}))))
55543ad2ant1 1131 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) β†’ (𝑍 ∈ 𝑉 β†’ ((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) β†’ (𝑖 ∈ (0..^𝑁) β†’ {((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘–), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑖 + 1))} = {(π‘Šβ€˜π‘–), (π‘Šβ€˜(𝑖 + 1))}))))
5655imp 406 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉) β†’ ((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) β†’ (𝑖 ∈ (0..^𝑁) β†’ {((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘–), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑖 + 1))} = {(π‘Šβ€˜π‘–), (π‘Šβ€˜(𝑖 + 1))})))
5756expdcom 414 . . . . . . . . . . . . . . . . . . . . 21 (π‘Š ∈ Word 𝑉 β†’ ((β™―β€˜π‘Š) = (𝑁 + 1) β†’ (((𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉) β†’ (𝑖 ∈ (0..^𝑁) β†’ {((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘–), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑖 + 1))} = {(π‘Šβ€˜π‘–), (π‘Šβ€˜(𝑖 + 1))}))))
58573imp1 1345 . . . . . . . . . . . . . . . . . . . 20 (((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1) ∧ ((𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ 𝑖 ∈ (0..^𝑁)) β†’ {((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘–), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑖 + 1))} = {(π‘Šβ€˜π‘–), (π‘Šβ€˜(𝑖 + 1))})
5958eleq1d 2813 . . . . . . . . . . . . . . . . . . 19 (((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1) ∧ ((𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ 𝑖 ∈ (0..^𝑁)) β†’ ({((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘–), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑖 + 1))} ∈ 𝐸 ↔ {(π‘Šβ€˜π‘–), (π‘Šβ€˜(𝑖 + 1))} ∈ 𝐸))
6059ralbidva 3170 . . . . . . . . . . . . . . . . . 18 ((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1) ∧ ((𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) β†’ (βˆ€π‘– ∈ (0..^𝑁){((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘–), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑖 + 1))} ∈ 𝐸 ↔ βˆ€π‘– ∈ (0..^𝑁){(π‘Šβ€˜π‘–), (π‘Šβ€˜(𝑖 + 1))} ∈ 𝐸))
6160biimprd 247 . . . . . . . . . . . . . . . . 17 ((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1) ∧ ((𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) β†’ (βˆ€π‘– ∈ (0..^𝑁){(π‘Šβ€˜π‘–), (π‘Šβ€˜(𝑖 + 1))} ∈ 𝐸 β†’ βˆ€π‘– ∈ (0..^𝑁){((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘–), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑖 + 1))} ∈ 𝐸))
62613exp 1117 . . . . . . . . . . . . . . . 16 (π‘Š ∈ Word 𝑉 β†’ ((β™―β€˜π‘Š) = (𝑁 + 1) β†’ (((𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉) β†’ (βˆ€π‘– ∈ (0..^𝑁){(π‘Šβ€˜π‘–), (π‘Šβ€˜(𝑖 + 1))} ∈ 𝐸 β†’ βˆ€π‘– ∈ (0..^𝑁){((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘–), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑖 + 1))} ∈ 𝐸))))
6362com34 91 . . . . . . . . . . . . . . 15 (π‘Š ∈ Word 𝑉 β†’ ((β™―β€˜π‘Š) = (𝑁 + 1) β†’ (βˆ€π‘– ∈ (0..^𝑁){(π‘Šβ€˜π‘–), (π‘Šβ€˜(𝑖 + 1))} ∈ 𝐸 β†’ (((𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉) β†’ βˆ€π‘– ∈ (0..^𝑁){((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘–), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑖 + 1))} ∈ 𝐸))))
64633imp1 1345 . . . . . . . . . . . . . 14 (((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1) ∧ βˆ€π‘– ∈ (0..^𝑁){(π‘Šβ€˜π‘–), (π‘Šβ€˜(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) β†’ βˆ€π‘– ∈ (0..^𝑁){((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘–), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑖 + 1))} ∈ 𝐸)
6564adantr 480 . . . . . . . . . . . . 13 ((((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1) ∧ βˆ€π‘– ∈ (0..^𝑁){(π‘Šβ€˜π‘–), (π‘Šβ€˜(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastSβ€˜π‘Š), 𝑍} ∈ 𝐸) β†’ βˆ€π‘– ∈ (0..^𝑁){((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘–), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑖 + 1))} ∈ 𝐸)
66 simpll 766 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ β„•0)) β†’ π‘Š ∈ Word 𝑉)
678ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ β„•0)) β†’ βŸ¨β€œπ‘β€βŸ© ∈ Word 𝑉)
68 nn0p1gt0 12523 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑁 ∈ β„•0 β†’ 0 < (𝑁 + 1))
6968ad2antll 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ β„•0)) β†’ 0 < (𝑁 + 1))
70 breq2 5146 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((β™―β€˜π‘Š) = (𝑁 + 1) β†’ (0 < (β™―β€˜π‘Š) ↔ 0 < (𝑁 + 1)))
7170ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ β„•0)) β†’ (0 < (β™―β€˜π‘Š) ↔ 0 < (𝑁 + 1)))
7269, 71mpbird 257 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ β„•0)) β†’ 0 < (β™―β€˜π‘Š))
73 hashneq0 14347 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (π‘Š ∈ Word 𝑉 β†’ (0 < (β™―β€˜π‘Š) ↔ π‘Š β‰  βˆ…))
7473ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ β„•0)) β†’ (0 < (β™―β€˜π‘Š) ↔ π‘Š β‰  βˆ…))
7572, 74mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ β„•0)) β†’ π‘Š β‰  βˆ…)
76 ccatval1lsw 14558 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((π‘Š ∈ Word 𝑉 ∧ βŸ¨β€œπ‘β€βŸ© ∈ Word 𝑉 ∧ π‘Š β‰  βˆ…) β†’ ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜((β™―β€˜π‘Š) βˆ’ 1)) = (lastSβ€˜π‘Š))
7766, 67, 75, 76syl3anc 1369 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ β„•0)) β†’ ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜((β™―β€˜π‘Š) βˆ’ 1)) = (lastSβ€˜π‘Š))
78 oveq1 7421 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((β™―β€˜π‘Š) = (𝑁 + 1) β†’ ((β™―β€˜π‘Š) βˆ’ 1) = ((𝑁 + 1) βˆ’ 1))
7978ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ β„•0)) β†’ ((β™―β€˜π‘Š) βˆ’ 1) = ((𝑁 + 1) βˆ’ 1))
80 nn0cn 12504 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑁 ∈ β„•0 β†’ 𝑁 ∈ β„‚)
8180ad2antll 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ β„•0)) β†’ 𝑁 ∈ β„‚)
82 pncan1 11660 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑁 ∈ β„‚ β†’ ((𝑁 + 1) βˆ’ 1) = 𝑁)
8381, 82syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ β„•0)) β†’ ((𝑁 + 1) βˆ’ 1) = 𝑁)
8479, 83eqtrd 2767 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ β„•0)) β†’ ((β™―β€˜π‘Š) βˆ’ 1) = 𝑁)
8584fveq2d 6895 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ β„•0)) β†’ ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜((β™―β€˜π‘Š) βˆ’ 1)) = ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘))
8677, 85eqtr3d 2769 . . . . . . . . . . . . . . . . . . . . . . . 24 (((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ β„•0)) β†’ (lastSβ€˜π‘Š) = ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘))
87 ccatws1ls 14607 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉) β†’ ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(β™―β€˜π‘Š)) = 𝑍)
8887ad2ant2r 746 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ β„•0)) β†’ ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(β™―β€˜π‘Š)) = 𝑍)
89 fveq2 6891 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((β™―β€˜π‘Š) = (𝑁 + 1) β†’ ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(β™―β€˜π‘Š)) = ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑁 + 1)))
9089ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ β„•0)) β†’ ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(β™―β€˜π‘Š)) = ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑁 + 1)))
9188, 90eqtr3d 2769 . . . . . . . . . . . . . . . . . . . . . . . 24 (((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ β„•0)) β†’ 𝑍 = ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑁 + 1)))
9286, 91preq12d 4741 . . . . . . . . . . . . . . . . . . . . . . 23 (((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ β„•0)) β†’ {(lastSβ€˜π‘Š), 𝑍} = {((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑁 + 1))})
9392expcom 413 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ β„•0) β†’ ((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) β†’ {(lastSβ€˜π‘Š), 𝑍} = {((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑁 + 1))}))
9493expcom 413 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ β„•0 β†’ (𝑍 ∈ 𝑉 β†’ ((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) β†’ {(lastSβ€˜π‘Š), 𝑍} = {((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑁 + 1))})))
95943ad2ant1 1131 . . . . . . . . . . . . . . . . . . . 20 ((𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) β†’ (𝑍 ∈ 𝑉 β†’ ((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) β†’ {(lastSβ€˜π‘Š), 𝑍} = {((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑁 + 1))})))
9695imp 406 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉) β†’ ((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) β†’ {(lastSβ€˜π‘Š), 𝑍} = {((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑁 + 1))}))
9796com12 32 . . . . . . . . . . . . . . . . . 18 ((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) β†’ (((𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉) β†’ {(lastSβ€˜π‘Š), 𝑍} = {((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑁 + 1))}))
98973adant3 1130 . . . . . . . . . . . . . . . . 17 ((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1) ∧ βˆ€π‘– ∈ (0..^𝑁){(π‘Šβ€˜π‘–), (π‘Šβ€˜(𝑖 + 1))} ∈ 𝐸) β†’ (((𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉) β†’ {(lastSβ€˜π‘Š), 𝑍} = {((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑁 + 1))}))
9998imp 406 . . . . . . . . . . . . . . . 16 (((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1) ∧ βˆ€π‘– ∈ (0..^𝑁){(π‘Šβ€˜π‘–), (π‘Šβ€˜(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) β†’ {(lastSβ€˜π‘Š), 𝑍} = {((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑁 + 1))})
10099eleq1d 2813 . . . . . . . . . . . . . . 15 (((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1) ∧ βˆ€π‘– ∈ (0..^𝑁){(π‘Šβ€˜π‘–), (π‘Šβ€˜(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) β†’ ({(lastSβ€˜π‘Š), 𝑍} ∈ 𝐸 ↔ {((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑁 + 1))} ∈ 𝐸))
101100biimpa 476 . . . . . . . . . . . . . 14 ((((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1) ∧ βˆ€π‘– ∈ (0..^𝑁){(π‘Šβ€˜π‘–), (π‘Šβ€˜(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastSβ€˜π‘Š), 𝑍} ∈ 𝐸) β†’ {((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑁 + 1))} ∈ 𝐸)
102 simprl1 1216 . . . . . . . . . . . . . . . 16 (((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1) ∧ βˆ€π‘– ∈ (0..^𝑁){(π‘Šβ€˜π‘–), (π‘Šβ€˜(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) β†’ 𝑁 ∈ β„•0)
103102adantr 480 . . . . . . . . . . . . . . 15 ((((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1) ∧ βˆ€π‘– ∈ (0..^𝑁){(π‘Šβ€˜π‘–), (π‘Šβ€˜(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastSβ€˜π‘Š), 𝑍} ∈ 𝐸) β†’ 𝑁 ∈ β„•0)
104 fveq2 6891 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑁 β†’ ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘–) = ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘))
105 fvoveq1 7437 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑁 β†’ ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑖 + 1)) = ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑁 + 1)))
106104, 105preq12d 4741 . . . . . . . . . . . . . . . . 17 (𝑖 = 𝑁 β†’ {((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘–), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑖 + 1))} = {((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑁 + 1))})
107106eleq1d 2813 . . . . . . . . . . . . . . . 16 (𝑖 = 𝑁 β†’ ({((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘–), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑖 + 1))} ∈ 𝐸 ↔ {((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑁 + 1))} ∈ 𝐸))
108107ralsng 4673 . . . . . . . . . . . . . . 15 (𝑁 ∈ β„•0 β†’ (βˆ€π‘– ∈ {𝑁} {((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘–), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑖 + 1))} ∈ 𝐸 ↔ {((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑁 + 1))} ∈ 𝐸))
109103, 108syl 17 . . . . . . . . . . . . . 14 ((((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1) ∧ βˆ€π‘– ∈ (0..^𝑁){(π‘Šβ€˜π‘–), (π‘Šβ€˜(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastSβ€˜π‘Š), 𝑍} ∈ 𝐸) β†’ (βˆ€π‘– ∈ {𝑁} {((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘–), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑖 + 1))} ∈ 𝐸 ↔ {((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑁 + 1))} ∈ 𝐸))
110101, 109mpbird 257 . . . . . . . . . . . . 13 ((((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1) ∧ βˆ€π‘– ∈ (0..^𝑁){(π‘Šβ€˜π‘–), (π‘Šβ€˜(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastSβ€˜π‘Š), 𝑍} ∈ 𝐸) β†’ βˆ€π‘– ∈ {𝑁} {((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘–), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑖 + 1))} ∈ 𝐸)
111 ralunb 4187 . . . . . . . . . . . . 13 (βˆ€π‘– ∈ ((0..^𝑁) βˆͺ {𝑁}){((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘–), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑖 + 1))} ∈ 𝐸 ↔ (βˆ€π‘– ∈ (0..^𝑁){((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘–), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑖 + 1))} ∈ 𝐸 ∧ βˆ€π‘– ∈ {𝑁} {((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘–), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑖 + 1))} ∈ 𝐸))
11265, 110, 111sylanbrc 582 . . . . . . . . . . . 12 ((((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1) ∧ βˆ€π‘– ∈ (0..^𝑁){(π‘Šβ€˜π‘–), (π‘Šβ€˜(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastSβ€˜π‘Š), 𝑍} ∈ 𝐸) β†’ βˆ€π‘– ∈ ((0..^𝑁) βˆͺ {𝑁}){((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘–), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑖 + 1))} ∈ 𝐸)
113 elnn0uz 12889 . . . . . . . . . . . . . . . 16 (𝑁 ∈ β„•0 ↔ 𝑁 ∈ (β„€β‰₯β€˜0))
114102, 113sylib 217 . . . . . . . . . . . . . . 15 (((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1) ∧ βˆ€π‘– ∈ (0..^𝑁){(π‘Šβ€˜π‘–), (π‘Šβ€˜(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) β†’ 𝑁 ∈ (β„€β‰₯β€˜0))
115114adantr 480 . . . . . . . . . . . . . 14 ((((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1) ∧ βˆ€π‘– ∈ (0..^𝑁){(π‘Šβ€˜π‘–), (π‘Šβ€˜(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastSβ€˜π‘Š), 𝑍} ∈ 𝐸) β†’ 𝑁 ∈ (β„€β‰₯β€˜0))
116 fzosplitsn 13764 . . . . . . . . . . . . . 14 (𝑁 ∈ (β„€β‰₯β€˜0) β†’ (0..^(𝑁 + 1)) = ((0..^𝑁) βˆͺ {𝑁}))
117115, 116syl 17 . . . . . . . . . . . . 13 ((((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1) ∧ βˆ€π‘– ∈ (0..^𝑁){(π‘Šβ€˜π‘–), (π‘Šβ€˜(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastSβ€˜π‘Š), 𝑍} ∈ 𝐸) β†’ (0..^(𝑁 + 1)) = ((0..^𝑁) βˆͺ {𝑁}))
118117raleqdv 3320 . . . . . . . . . . . 12 ((((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1) ∧ βˆ€π‘– ∈ (0..^𝑁){(π‘Šβ€˜π‘–), (π‘Šβ€˜(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastSβ€˜π‘Š), 𝑍} ∈ 𝐸) β†’ (βˆ€π‘– ∈ (0..^(𝑁 + 1)){((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘–), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑖 + 1))} ∈ 𝐸 ↔ βˆ€π‘– ∈ ((0..^𝑁) βˆͺ {𝑁}){((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘–), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑖 + 1))} ∈ 𝐸))
119112, 118mpbird 257 . . . . . . . . . . 11 ((((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1) ∧ βˆ€π‘– ∈ (0..^𝑁){(π‘Šβ€˜π‘–), (π‘Šβ€˜(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastSβ€˜π‘Š), 𝑍} ∈ 𝐸) β†’ βˆ€π‘– ∈ (0..^(𝑁 + 1)){((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘–), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑖 + 1))} ∈ 𝐸)
120 ccatws1len 14594 . . . . . . . . . . . . . . . . 17 (π‘Š ∈ Word 𝑉 β†’ (β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) = ((β™―β€˜π‘Š) + 1))
1211203ad2ant1 1131 . . . . . . . . . . . . . . . 16 ((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1) ∧ βˆ€π‘– ∈ (0..^𝑁){(π‘Šβ€˜π‘–), (π‘Šβ€˜(𝑖 + 1))} ∈ 𝐸) β†’ (β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) = ((β™―β€˜π‘Š) + 1))
122121ad2antrr 725 . . . . . . . . . . . . . . 15 ((((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1) ∧ βˆ€π‘– ∈ (0..^𝑁){(π‘Šβ€˜π‘–), (π‘Šβ€˜(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastSβ€˜π‘Š), 𝑍} ∈ 𝐸) β†’ (β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) = ((β™―β€˜π‘Š) + 1))
123122oveq1d 7429 . . . . . . . . . . . . . 14 ((((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1) ∧ βˆ€π‘– ∈ (0..^𝑁){(π‘Šβ€˜π‘–), (π‘Šβ€˜(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastSβ€˜π‘Š), 𝑍} ∈ 𝐸) β†’ ((β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) βˆ’ 1) = (((β™―β€˜π‘Š) + 1) βˆ’ 1))
124 oveq1 7421 . . . . . . . . . . . . . . . . . 18 ((β™―β€˜π‘Š) = (𝑁 + 1) β†’ ((β™―β€˜π‘Š) + 1) = ((𝑁 + 1) + 1))
125124oveq1d 7429 . . . . . . . . . . . . . . . . 17 ((β™―β€˜π‘Š) = (𝑁 + 1) β†’ (((β™―β€˜π‘Š) + 1) βˆ’ 1) = (((𝑁 + 1) + 1) βˆ’ 1))
126 1cnd 11231 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ β„•0 β†’ 1 ∈ β„‚)
12780, 126addcld 11255 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ β„•0 β†’ (𝑁 + 1) ∈ β„‚)
128127, 126pncand 11594 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ β„•0 β†’ (((𝑁 + 1) + 1) βˆ’ 1) = (𝑁 + 1))
1291283ad2ant1 1131 . . . . . . . . . . . . . . . . . 18 ((𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) β†’ (((𝑁 + 1) + 1) βˆ’ 1) = (𝑁 + 1))
130129adantr 480 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉) β†’ (((𝑁 + 1) + 1) βˆ’ 1) = (𝑁 + 1))
131125, 130sylan9eq 2787 . . . . . . . . . . . . . . . 16 (((β™―β€˜π‘Š) = (𝑁 + 1) ∧ ((𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) β†’ (((β™―β€˜π‘Š) + 1) βˆ’ 1) = (𝑁 + 1))
1321313ad2antl2 1184 . . . . . . . . . . . . . . 15 (((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1) ∧ βˆ€π‘– ∈ (0..^𝑁){(π‘Šβ€˜π‘–), (π‘Šβ€˜(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) β†’ (((β™―β€˜π‘Š) + 1) βˆ’ 1) = (𝑁 + 1))
133132adantr 480 . . . . . . . . . . . . . 14 ((((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1) ∧ βˆ€π‘– ∈ (0..^𝑁){(π‘Šβ€˜π‘–), (π‘Šβ€˜(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastSβ€˜π‘Š), 𝑍} ∈ 𝐸) β†’ (((β™―β€˜π‘Š) + 1) βˆ’ 1) = (𝑁 + 1))
134123, 133eqtrd 2767 . . . . . . . . . . . . 13 ((((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1) ∧ βˆ€π‘– ∈ (0..^𝑁){(π‘Šβ€˜π‘–), (π‘Šβ€˜(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastSβ€˜π‘Š), 𝑍} ∈ 𝐸) β†’ ((β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) βˆ’ 1) = (𝑁 + 1))
135134oveq2d 7430 . . . . . . . . . . . 12 ((((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1) ∧ βˆ€π‘– ∈ (0..^𝑁){(π‘Šβ€˜π‘–), (π‘Šβ€˜(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastSβ€˜π‘Š), 𝑍} ∈ 𝐸) β†’ (0..^((β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) βˆ’ 1)) = (0..^(𝑁 + 1)))
136135raleqdv 3320 . . . . . . . . . . 11 ((((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1) ∧ βˆ€π‘– ∈ (0..^𝑁){(π‘Šβ€˜π‘–), (π‘Šβ€˜(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastSβ€˜π‘Š), 𝑍} ∈ 𝐸) β†’ (βˆ€π‘– ∈ (0..^((β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) βˆ’ 1)){((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘–), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑖 + 1))} ∈ 𝐸 ↔ βˆ€π‘– ∈ (0..^(𝑁 + 1)){((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘–), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑖 + 1))} ∈ 𝐸))
137119, 136mpbird 257 . . . . . . . . . 10 ((((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1) ∧ βˆ€π‘– ∈ (0..^𝑁){(π‘Šβ€˜π‘–), (π‘Šβ€˜(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastSβ€˜π‘Š), 𝑍} ∈ 𝐸) β†’ βˆ€π‘– ∈ (0..^((β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) βˆ’ 1)){((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘–), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑖 + 1))} ∈ 𝐸)
138137exp42 435 . . . . . . . . 9 ((π‘Š ∈ Word 𝑉 ∧ (β™―β€˜π‘Š) = (𝑁 + 1) ∧ βˆ€π‘– ∈ (0..^𝑁){(π‘Šβ€˜π‘–), (π‘Šβ€˜(𝑖 + 1))} ∈ 𝐸) β†’ ((𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) β†’ (𝑍 ∈ 𝑉 β†’ ({(lastSβ€˜π‘Š), 𝑍} ∈ 𝐸 β†’ βˆ€π‘– ∈ (0..^((β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) βˆ’ 1)){((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘–), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑖 + 1))} ∈ 𝐸))))
13914, 138syl 17 . . . . . . . 8 (π‘Š ∈ (𝑁 WWalksN 𝐺) β†’ ((𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) β†’ (𝑍 ∈ 𝑉 β†’ ({(lastSβ€˜π‘Š), 𝑍} ∈ 𝐸 β†’ βˆ€π‘– ∈ (0..^((β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) βˆ’ 1)){((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘–), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑖 + 1))} ∈ 𝐸))))
140139imp41 425 . . . . . . 7 ((((π‘Š ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) ∧ {(lastSβ€˜π‘Š), 𝑍} ∈ 𝐸) β†’ βˆ€π‘– ∈ (0..^((β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) βˆ’ 1)){((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘–), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑖 + 1))} ∈ 𝐸)
141140adantrr 716 . . . . . 6 ((((π‘Š ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) ∧ ({(lastSβ€˜π‘Š), 𝑍} ∈ 𝐸 ∧ {𝑍, (π‘Šβ€˜0)} ∈ 𝐸)) β†’ βˆ€π‘– ∈ (0..^((β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) βˆ’ 1)){((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘–), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑖 + 1))} ∈ 𝐸)
142 lswccats1 14608 . . . . . . . . . . . 12 ((π‘Š ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉) β†’ (lastSβ€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) = 𝑍)
1437, 142sylancom 587 . . . . . . . . . . 11 (((π‘Š ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) β†’ (lastSβ€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) = 𝑍)
144683ad2ant1 1131 . . . . . . . . . . . . . 14 ((𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) β†’ 0 < (𝑁 + 1))
145703ad2ant3 1133 . . . . . . . . . . . . . 14 ((𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) β†’ (0 < (β™―β€˜π‘Š) ↔ 0 < (𝑁 + 1)))
146144, 145mpbird 257 . . . . . . . . . . . . 13 ((𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) β†’ 0 < (β™―β€˜π‘Š))
147146ad2antlr 726 . . . . . . . . . . . 12 (((π‘Š ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) β†’ 0 < (β™―β€˜π‘Š))
148 ccatfv0 14557 . . . . . . . . . . . 12 ((π‘Š ∈ Word 𝑉 ∧ βŸ¨β€œπ‘β€βŸ© ∈ Word 𝑉 ∧ 0 < (β™―β€˜π‘Š)) β†’ ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜0) = (π‘Šβ€˜0))
1497, 9, 147, 148syl3anc 1369 . . . . . . . . . . 11 (((π‘Š ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) β†’ ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜0) = (π‘Šβ€˜0))
150143, 149preq12d 4741 . . . . . . . . . 10 (((π‘Š ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) β†’ {(lastSβ€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜0)} = {𝑍, (π‘Šβ€˜0)})
151150eleq1d 2813 . . . . . . . . 9 (((π‘Š ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) β†’ ({(lastSβ€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜0)} ∈ 𝐸 ↔ {𝑍, (π‘Šβ€˜0)} ∈ 𝐸))
152151biimprcd 249 . . . . . . . 8 ({𝑍, (π‘Šβ€˜0)} ∈ 𝐸 β†’ (((π‘Š ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) β†’ {(lastSβ€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜0)} ∈ 𝐸))
153152adantl 481 . . . . . . 7 (({(lastSβ€˜π‘Š), 𝑍} ∈ 𝐸 ∧ {𝑍, (π‘Šβ€˜0)} ∈ 𝐸) β†’ (((π‘Š ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) β†’ {(lastSβ€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜0)} ∈ 𝐸))
154153impcom 407 . . . . . 6 ((((π‘Š ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) ∧ ({(lastSβ€˜π‘Š), 𝑍} ∈ 𝐸 ∧ {𝑍, (π‘Šβ€˜0)} ∈ 𝐸)) β†’ {(lastSβ€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜0)} ∈ 𝐸)
15512, 141, 1543jca 1126 . . . . 5 ((((π‘Š ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) ∧ ({(lastSβ€˜π‘Š), 𝑍} ∈ 𝐸 ∧ {𝑍, (π‘Šβ€˜0)} ∈ 𝐸)) β†’ ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©) ∈ Word 𝑉 ∧ βˆ€π‘– ∈ (0..^((β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) βˆ’ 1)){((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘–), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑖 + 1))} ∈ 𝐸 ∧ {(lastSβ€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜0)} ∈ 𝐸))
156 ccatws1len 14594 . . . . . . . 8 (π‘Š ∈ Word (Vtxβ€˜πΊ) β†’ (β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) = ((β™―β€˜π‘Š) + 1))
1571563ad2ant2 1132 . . . . . . 7 ((𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) β†’ (β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) = ((β™―β€˜π‘Š) + 1))
1581243ad2ant3 1133 . . . . . . 7 ((𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) β†’ ((β™―β€˜π‘Š) + 1) = ((𝑁 + 1) + 1))
15980, 126, 126addassd 11258 . . . . . . . . 9 (𝑁 ∈ β„•0 β†’ ((𝑁 + 1) + 1) = (𝑁 + (1 + 1)))
160 1p1e2 12359 . . . . . . . . . 10 (1 + 1) = 2
161160oveq2i 7425 . . . . . . . . 9 (𝑁 + (1 + 1)) = (𝑁 + 2)
162159, 161eqtrdi 2783 . . . . . . . 8 (𝑁 ∈ β„•0 β†’ ((𝑁 + 1) + 1) = (𝑁 + 2))
1631623ad2ant1 1131 . . . . . . 7 ((𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) β†’ ((𝑁 + 1) + 1) = (𝑁 + 2))
164157, 158, 1633eqtrd 2771 . . . . . 6 ((𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) β†’ (β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) = (𝑁 + 2))
165164ad3antlr 730 . . . . 5 ((((π‘Š ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) ∧ ({(lastSβ€˜π‘Š), 𝑍} ∈ 𝐸 ∧ {𝑍, (π‘Šβ€˜0)} ∈ 𝐸)) β†’ (β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) = (𝑁 + 2))
166 2nn 12307 . . . . . . . . 9 2 ∈ β„•
167 nn0nnaddcl 12525 . . . . . . . . 9 ((𝑁 ∈ β„•0 ∧ 2 ∈ β„•) β†’ (𝑁 + 2) ∈ β„•)
168166, 167mpan2 690 . . . . . . . 8 (𝑁 ∈ β„•0 β†’ (𝑁 + 2) ∈ β„•)
1691683ad2ant1 1131 . . . . . . 7 ((𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) β†’ (𝑁 + 2) ∈ β„•)
1702, 13isclwwlknx 29833 . . . . . . 7 ((𝑁 + 2) ∈ β„• β†’ ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©) ∈ ((𝑁 + 2) ClWWalksN 𝐺) ↔ (((π‘Š ++ βŸ¨β€œπ‘β€βŸ©) ∈ Word 𝑉 ∧ βˆ€π‘– ∈ (0..^((β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) βˆ’ 1)){((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘–), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑖 + 1))} ∈ 𝐸 ∧ {(lastSβ€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜0)} ∈ 𝐸) ∧ (β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) = (𝑁 + 2))))
171169, 170syl 17 . . . . . 6 ((𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1)) β†’ ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©) ∈ ((𝑁 + 2) ClWWalksN 𝐺) ↔ (((π‘Š ++ βŸ¨β€œπ‘β€βŸ©) ∈ Word 𝑉 ∧ βˆ€π‘– ∈ (0..^((β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) βˆ’ 1)){((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘–), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑖 + 1))} ∈ 𝐸 ∧ {(lastSβ€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜0)} ∈ 𝐸) ∧ (β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) = (𝑁 + 2))))
172171ad3antlr 730 . . . . 5 ((((π‘Š ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) ∧ ({(lastSβ€˜π‘Š), 𝑍} ∈ 𝐸 ∧ {𝑍, (π‘Šβ€˜0)} ∈ 𝐸)) β†’ ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©) ∈ ((𝑁 + 2) ClWWalksN 𝐺) ↔ (((π‘Š ++ βŸ¨β€œπ‘β€βŸ©) ∈ Word 𝑉 ∧ βˆ€π‘– ∈ (0..^((β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) βˆ’ 1)){((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜π‘–), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜(𝑖 + 1))} ∈ 𝐸 ∧ {(lastSβ€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)), ((π‘Š ++ βŸ¨β€œπ‘β€βŸ©)β€˜0)} ∈ 𝐸) ∧ (β™―β€˜(π‘Š ++ βŸ¨β€œπ‘β€βŸ©)) = (𝑁 + 2))))
173155, 165, 172mpbir2and 712 . . . 4 ((((π‘Š ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) ∧ ({(lastSβ€˜π‘Š), 𝑍} ∈ 𝐸 ∧ {𝑍, (π‘Šβ€˜0)} ∈ 𝐸)) β†’ (π‘Š ++ βŸ¨β€œπ‘β€βŸ©) ∈ ((𝑁 + 2) ClWWalksN 𝐺))
174173exp31 419 . . 3 ((π‘Š ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ β„•0 ∧ π‘Š ∈ Word (Vtxβ€˜πΊ) ∧ (β™―β€˜π‘Š) = (𝑁 + 1))) β†’ (𝑍 ∈ 𝑉 β†’ (({(lastSβ€˜π‘Š), 𝑍} ∈ 𝐸 ∧ {𝑍, (π‘Šβ€˜0)} ∈ 𝐸) β†’ (π‘Š ++ βŸ¨β€œπ‘β€βŸ©) ∈ ((𝑁 + 2) ClWWalksN 𝐺))))
1751, 174mpdan 686 . 2 (π‘Š ∈ (𝑁 WWalksN 𝐺) β†’ (𝑍 ∈ 𝑉 β†’ (({(lastSβ€˜π‘Š), 𝑍} ∈ 𝐸 ∧ {𝑍, (π‘Šβ€˜0)} ∈ 𝐸) β†’ (π‘Š ++ βŸ¨β€œπ‘β€βŸ©) ∈ ((𝑁 + 2) ClWWalksN 𝐺))))
176175imp 406 1 ((π‘Š ∈ (𝑁 WWalksN 𝐺) ∧ 𝑍 ∈ 𝑉) β†’ (({(lastSβ€˜π‘Š), 𝑍} ∈ 𝐸 ∧ {𝑍, (π‘Šβ€˜0)} ∈ 𝐸) β†’ (π‘Š ++ βŸ¨β€œπ‘β€βŸ©) ∈ ((𝑁 + 2) ClWWalksN 𝐺)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1085   = wceq 1534   ∈ wcel 2099   β‰  wne 2935  βˆ€wral 3056   βˆͺ cun 3942  βˆ…c0 4318  {csn 4624  {cpr 4626   class class class wbr 5142  β€˜cfv 6542  (class class class)co 7414  β„‚cc 11128  β„cr 11129  0cc0 11130  1c1 11131   + caddc 11133   < clt 11270   βˆ’ cmin 11466  β„•cn 12234  2c2 12289  β„•0cn0 12494  β„€β‰₯cuz 12844  ..^cfzo 13651  β™―chash 14313  Word cword 14488  lastSclsw 14536   ++ cconcat 14544  βŸ¨β€œcs1 14569  Vtxcvtx 28796  Edgcedg 28847   WWalksN cwwlksn 29624   ClWWalksN cclwwlkn 29821
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734  ax-cnex 11186  ax-resscn 11187  ax-1cn 11188  ax-icn 11189  ax-addcl 11190  ax-addrcl 11191  ax-mulcl 11192  ax-mulrcl 11193  ax-mulcom 11194  ax-addass 11195  ax-mulass 11196  ax-distr 11197  ax-i2m1 11198  ax-1ne0 11199  ax-1rid 11200  ax-rnegex 11201  ax-rrecex 11202  ax-cnre 11203  ax-pre-lttri 11204  ax-pre-lttrn 11205  ax-pre-ltadd 11206  ax-pre-mulgt0 11207
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-nel 3042  df-ral 3057  df-rex 3066  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-int 4945  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7370  df-ov 7417  df-oprab 7418  df-mpo 7419  df-om 7865  df-1st 7987  df-2nd 7988  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-1o 8480  df-er 8718  df-map 8838  df-en 8956  df-dom 8957  df-sdom 8958  df-fin 8959  df-card 9954  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276  df-sub 11468  df-neg 11469  df-nn 12235  df-2 12297  df-n0 12495  df-xnn0 12567  df-z 12581  df-uz 12845  df-rp 12999  df-fz 13509  df-fzo 13652  df-hash 14314  df-word 14489  df-lsw 14537  df-concat 14545  df-s1 14570  df-wwlks 29628  df-wwlksn 29629  df-clwwlk 29779  df-clwwlkn 29822
This theorem is referenced by:  numclwwlk2lem1  30173
  Copyright terms: Public domain W3C validator