Theorem wwlksext2clwwlk 30675

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.

Step	Hyp	Ref	Expression
1		wwlknbp1 30460	. . 3 ⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)))
2		clwwlkext2edg.v	. . . . . . . . . . . . 13 ⊢ 𝑉 = (Vtx‘𝐺)
3	2	wrdeqi 14706	. . . . . . . . . . . 12 ⊢ Word 𝑉 = Word (Vtx‘𝐺)
4	3	eleq2i 2856	. . . . . . . . . . 11 ⊢ (𝑊 ∈ Word 𝑉 ↔ 𝑊 ∈ Word (Vtx‘𝐺))
5	4	biimpri 231	. . . . . . . . . 10 ⊢ (𝑊 ∈ Word (Vtx‘𝐺) → 𝑊 ∈ Word 𝑉)
6	5	3ad2ant2 1152	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) → 𝑊 ∈ Word 𝑉)
7	6	ad2antlr 740	. . . . . . . 8 ⊢ (((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) → 𝑊 ∈ Word 𝑉)
8		s1cl 14773	. . . . . . . . 9 ⊢ (𝑍 ∈ 𝑉 → ⟨“𝑍”⟩ ∈ Word 𝑉)
9	8	adantl 487	. . . . . . . 8 ⊢ (((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) → ⟨“𝑍”⟩ ∈ Word 𝑉)
10		ccatcl 14743	. . . . . . . 8 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ⟨“𝑍”⟩ ∈ Word 𝑉) → (𝑊 ++ ⟨“𝑍”⟩) ∈ Word 𝑉)
11	7, 9, 10	syl2anc 596	. . . . . . 7 ⊢ (((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) → (𝑊 ++ ⟨“𝑍”⟩) ∈ Word 𝑉)
12	11	adantr 486	. . . . . 6 ⊢ ((((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) ∧ ({(lastS‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸)) → (𝑊 ++ ⟨“𝑍”⟩) ∈ Word 𝑉)
13		clwwlkext2edg.e	. . . . . . . . . 10 ⊢ 𝐸 = (Edg‘𝐺)
14	2, 13	wwlknp 30459	. . . . . . . . 9 ⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸))
15		simplll 787	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑊 ∈ Word 𝑉)
16	8	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → ⟨“𝑍”⟩ ∈ Word 𝑉)
17	16	ad2antlr 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → ⟨“𝑍”⟩ ∈ Word 𝑉)
18		elfzo0 13859	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑖 ∈ (0..^𝑁) ↔ (𝑖 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝑖 < 𝑁))
19		simp1 1154	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑖 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝑖 < 𝑁) → 𝑖 ∈ ℕ0)
20		peano2nn 12371	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℕ)
21	20	3ad2ant2 1152	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑖 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝑖 < 𝑁) → (𝑁 + 1) ∈ ℕ)
22		nn0re 12639	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑖 ∈ ℕ0 → 𝑖 ∈ ℝ)
23	22	3ad2ant1 1151	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑖 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝑖 < 𝑁) → 𝑖 ∈ ℝ)
24		nnre 12366	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
25	24	3ad2ant2 1152	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑖 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝑖 < 𝑁) → 𝑁 ∈ ℝ)
26		peano2re 11507	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑁 ∈ ℝ → (𝑁 + 1) ∈ ℝ)
27	24, 26	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℝ)
28	27	3ad2ant2 1152	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑖 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝑖 < 𝑁) → (𝑁 + 1) ∈ ℝ)
29		simp3 1156	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑖 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝑖 < 𝑁) → 𝑖 < 𝑁)
30	24	ltp1d 12271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑁 ∈ ℕ → 𝑁 < (𝑁 + 1))
31	30	3ad2ant2 1152	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑖 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝑖 < 𝑁) → 𝑁 < (𝑁 + 1))
32	23, 25, 28, 29, 31	lttrd 11495	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑖 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝑖 < 𝑁) → 𝑖 < (𝑁 + 1))
33		elfzo0 13859	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑖 ∈ (0..^(𝑁 + 1)) ↔ (𝑖 ∈ ℕ0 ∧ (𝑁 + 1) ∈ ℕ ∧ 𝑖 < (𝑁 + 1)))
34	19, 21, 32, 33	syl3anbrc 1362	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑖 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝑖 < 𝑁) → 𝑖 ∈ (0..^(𝑁 + 1)))
35	18, 34	sylbi 220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑖 ∈ (0..^𝑁) → 𝑖 ∈ (0..^(𝑁 + 1)))
36	35	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑖 ∈ (0..^(𝑁 + 1)))
37		oveq2 7448	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((♯‘𝑊) = (𝑁 + 1) → (0..^(♯‘𝑊)) = (0..^(𝑁 + 1)))
38	37	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) → (0..^(♯‘𝑊)) = (0..^(𝑁 + 1)))
39	38	eleq2d 2850	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) → (𝑖 ∈ (0..^(♯‘𝑊)) ↔ 𝑖 ∈ (0..^(𝑁 + 1))))
40	39	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑖 ∈ (0..^(♯‘𝑊)) ↔ 𝑖 ∈ (0..^(𝑁 + 1))))
41	36, 40	mpbird 260	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑖 ∈ (0..^(♯‘𝑊)))
42		ccatval1 14746	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ⟨“𝑍”⟩ ∈ Word 𝑉 ∧ 𝑖 ∈ (0..^(♯‘𝑊))) → ((𝑊 ++ ⟨“𝑍”⟩)‘𝑖) = (𝑊‘𝑖))
43	15, 17, 41, 42	syl3anc 1399	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑊 ++ ⟨“𝑍”⟩)‘𝑖) = (𝑊‘𝑖))
44		fzonn0p1p1 13903	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑖 ∈ (0..^𝑁) → (𝑖 + 1) ∈ (0..^(𝑁 + 1)))
45	44	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑖 + 1) ∈ (0..^(𝑁 + 1)))
46	37	eleq2d 2850	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((♯‘𝑊) = (𝑁 + 1) → ((𝑖 + 1) ∈ (0..^(♯‘𝑊)) ↔ (𝑖 + 1) ∈ (0..^(𝑁 + 1))))
47	46	ad3antlr 744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑖 + 1) ∈ (0..^(♯‘𝑊)) ↔ (𝑖 + 1) ∈ (0..^(𝑁 + 1))))
48	45, 47	mpbird 260	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑖 + 1) ∈ (0..^(♯‘𝑊)))
49		ccatval1 14746	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ⟨“𝑍”⟩ ∈ Word 𝑉 ∧ (𝑖 + 1) ∈ (0..^(♯‘𝑊))) → ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1)) = (𝑊‘(𝑖 + 1)))
50	15, 17, 48, 49	syl3anc 1399	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1)) = (𝑊‘(𝑖 + 1)))
51	43, 50	preq12d 4702	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → {((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} = {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))})
52	51	ex 418	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → (𝑖 ∈ (0..^𝑁) → {((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} = {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))}))
53	52	expcom 419	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) → (𝑖 ∈ (0..^𝑁) → {((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} = {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))})))
54	53	expcom 419	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑁 ∈ ℕ0 → (𝑍 ∈ 𝑉 → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) → (𝑖 ∈ (0..^𝑁) → {((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} = {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))}))))
55	54	3ad2ant1 1151	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) → (𝑍 ∈ 𝑉 → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) → (𝑖 ∈ (0..^𝑁) → {((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} = {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))}))))
56	55	imp 412	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉) → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) → (𝑖 ∈ (0..^𝑁) → {((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} = {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))})))
57	56	expdcom 420	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑊 ∈ Word 𝑉 → ((♯‘𝑊) = (𝑁 + 1) → (((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉) → (𝑖 ∈ (0..^𝑁) → {((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} = {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))}))))
58	57	3imp1 1366	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ 𝑖 ∈ (0..^𝑁)) → {((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} = {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))})
59	58	eleq1d 2849	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ 𝑖 ∈ (0..^𝑁)) → ({((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸))
60	59	ralbidva 3187	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) → (∀𝑖 ∈ (0..^𝑁){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸))
61	60	biimprd 251	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) → (∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 → ∀𝑖 ∈ (0..^𝑁){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸))
62	61	3exp 1137	. . . . . . . . . . . . . . . 16 ⊢ (𝑊 ∈ Word 𝑉 → ((♯‘𝑊) = (𝑁 + 1) → (((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉) → (∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 → ∀𝑖 ∈ (0..^𝑁){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸))))
63	62	com34 92	. . . . . . . . . . . . . . 15 ⊢ (𝑊 ∈ Word 𝑉 → ((♯‘𝑊) = (𝑁 + 1) → (∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 → (((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉) → ∀𝑖 ∈ (0..^𝑁){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸))))
64	63	3imp1 1366	. . . . . . . . . . . . . 14 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) → ∀𝑖 ∈ (0..^𝑁){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸)
65	64	adantr 486	. . . . . . . . . . . . 13 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → ∀𝑖 ∈ (0..^𝑁){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸)
66		simpll 779	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → 𝑊 ∈ Word 𝑉)
67	8	ad2antrl 741	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → ⟨“𝑍”⟩ ∈ Word 𝑉)
68		nn0p1gt0 12659	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑁 ∈ ℕ0 → 0 < (𝑁 + 1))
69	68	ad2antll 742	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → 0 < (𝑁 + 1))
70		breq2 5110	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((♯‘𝑊) = (𝑁 + 1) → (0 < (♯‘𝑊) ↔ 0 < (𝑁 + 1)))
71	70	ad2antlr 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → (0 < (♯‘𝑊) ↔ 0 < (𝑁 + 1)))
72	69, 71	mpbird 260	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → 0 < (♯‘𝑊))
73		hashneq0 14532	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑊 ∈ Word 𝑉 → (0 < (♯‘𝑊) ↔ 𝑊 ≠ ∅))
74	73	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → (0 < (♯‘𝑊) ↔ 𝑊 ≠ ∅))
75	72, 74	mpbid 235	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → 𝑊 ≠ ∅)
76		ccatval1lsw 14754	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ⟨“𝑍”⟩ ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → ((𝑊 ++ ⟨“𝑍”⟩)‘((♯‘𝑊) − 1)) = (lastS‘𝑊))
77	66, 67, 75, 76	syl3anc 1399	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → ((𝑊 ++ ⟨“𝑍”⟩)‘((♯‘𝑊) − 1)) = (lastS‘𝑊))
78		oveq1 7447	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((♯‘𝑊) = (𝑁 + 1) → ((♯‘𝑊) − 1) = ((𝑁 + 1) − 1))
79	78	ad2antlr 740	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → ((♯‘𝑊) − 1) = ((𝑁 + 1) − 1))
80		nn0cn 12640	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ)
81	80	ad2antll 742	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → 𝑁 ∈ ℂ)
82		pncan1 11764	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑁 ∈ ℂ → ((𝑁 + 1) − 1) = 𝑁)
83	81, 82	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → ((𝑁 + 1) − 1) = 𝑁)
84	79, 83	eqtrd 2798	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → ((♯‘𝑊) − 1) = 𝑁)
85	84	fveq2d 6909	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → ((𝑊 ++ ⟨“𝑍”⟩)‘((♯‘𝑊) − 1)) = ((𝑊 ++ ⟨“𝑍”⟩)‘𝑁))
86	77, 85	eqtr3d 2800	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → (lastS‘𝑊) = ((𝑊 ++ ⟨“𝑍”⟩)‘𝑁))
87		ccatws1ls 14806	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉) → ((𝑊 ++ ⟨“𝑍”⟩)‘(♯‘𝑊)) = 𝑍)
88	87	ad2ant2r 760	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → ((𝑊 ++ ⟨“𝑍”⟩)‘(♯‘𝑊)) = 𝑍)
89		fveq2 6905	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((♯‘𝑊) = (𝑁 + 1) → ((𝑊 ++ ⟨“𝑍”⟩)‘(♯‘𝑊)) = ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1)))
90	89	ad2antlr 740	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → ((𝑊 ++ ⟨“𝑍”⟩)‘(♯‘𝑊)) = ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1)))
91	88, 90	eqtr3d 2800	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → 𝑍 = ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1)))
92	86, 91	preq12d 4702	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → {(lastS‘𝑊), 𝑍} = {((𝑊 ++ ⟨“𝑍”⟩)‘𝑁), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1))})
93	92	expcom 419	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) → {(lastS‘𝑊), 𝑍} = {((𝑊 ++ ⟨“𝑍”⟩)‘𝑁), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1))}))
94	93	expcom 419	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ ℕ0 → (𝑍 ∈ 𝑉 → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) → {(lastS‘𝑊), 𝑍} = {((𝑊 ++ ⟨“𝑍”⟩)‘𝑁), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1))})))
95	94	3ad2ant1 1151	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) → (𝑍 ∈ 𝑉 → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) → {(lastS‘𝑊), 𝑍} = {((𝑊 ++ ⟨“𝑍”⟩)‘𝑁), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1))})))
96	95	imp 412	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉) → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) → {(lastS‘𝑊), 𝑍} = {((𝑊 ++ ⟨“𝑍”⟩)‘𝑁), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1))}))
97	96	com12 33	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) → (((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉) → {(lastS‘𝑊), 𝑍} = {((𝑊 ++ ⟨“𝑍”⟩)‘𝑁), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1))}))
98	97	3adant3 1150	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) → (((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉) → {(lastS‘𝑊), 𝑍} = {((𝑊 ++ ⟨“𝑍”⟩)‘𝑁), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1))}))
99	98	imp 412	. . . . . . . . . . . . . . . 16 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) → {(lastS‘𝑊), 𝑍} = {((𝑊 ++ ⟨“𝑍”⟩)‘𝑁), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1))})
100	99	eleq1d 2849	. . . . . . . . . . . . . . 15 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) → ({(lastS‘𝑊), 𝑍} ∈ 𝐸 ↔ {((𝑊 ++ ⟨“𝑍”⟩)‘𝑁), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1))} ∈ 𝐸))
101	100	biimpa 482	. . . . . . . . . . . . . 14 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → {((𝑊 ++ ⟨“𝑍”⟩)‘𝑁), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1))} ∈ 𝐸)
102		simprl1 1237	. . . . . . . . . . . . . . . 16 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) → 𝑁 ∈ ℕ0)
103	102	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → 𝑁 ∈ ℕ0)
104		fveq2 6905	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑁 → ((𝑊 ++ ⟨“𝑍”⟩)‘𝑖) = ((𝑊 ++ ⟨“𝑍”⟩)‘𝑁))
105		fvoveq1 7463	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑁 → ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1)) = ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1)))
106	104, 105	preq12d 4702	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝑁 → {((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} = {((𝑊 ++ ⟨“𝑍”⟩)‘𝑁), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1))})
107	106	eleq1d 2849	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑁 → ({((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ {((𝑊 ++ ⟨“𝑍”⟩)‘𝑁), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1))} ∈ 𝐸))
108	107	ralsng 4636	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ ℕ0 → (∀𝑖 ∈ {𝑁} {((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ {((𝑊 ++ ⟨“𝑍”⟩)‘𝑁), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1))} ∈ 𝐸))
109	103, 108	syl 18	. . . . . . . . . . . . . 14 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → (∀𝑖 ∈ {𝑁} {((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ {((𝑊 ++ ⟨“𝑍”⟩)‘𝑁), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1))} ∈ 𝐸))
110	101, 109	mpbird 260	. . . . . . . . . . . . 13 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → ∀𝑖 ∈ {𝑁} {((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸)
111		ralunb 4198	. . . . . . . . . . . . 13 ⊢ (∀𝑖 ∈ ((0..^𝑁) ∪ {𝑁}){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ (∀𝑖 ∈ (0..^𝑁){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸 ∧ ∀𝑖 ∈ {𝑁} {((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸))
112	65, 110, 111	sylanbrc 595	. . . . . . . . . . . 12 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → ∀𝑖 ∈ ((0..^𝑁) ∪ {𝑁}){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸)
113		elnn0uz 13030	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ ℕ0 ↔ 𝑁 ∈ (ℤ≥‘0))
114	102, 113	sylib 221	. . . . . . . . . . . . . 14 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) → 𝑁 ∈ (ℤ≥‘0))
115	114	adantr 486	. . . . . . . . . . . . 13 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → 𝑁 ∈ (ℤ≥‘0))
116		fzosplitsn 13935	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ (ℤ≥‘0) → (0..^(𝑁 + 1)) = ((0..^𝑁) ∪ {𝑁}))
117	115, 116	syl 18	. . . . . . . . . . . 12 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → (0..^(𝑁 + 1)) = ((0..^𝑁) ∪ {𝑁}))
118	112, 117	raleqtrrdv 3327	. . . . . . . . . . 11 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → ∀𝑖 ∈ (0..^(𝑁 + 1)){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸)
119		ccatws1len 14793	. . . . . . . . . . . . . . . 16 ⊢ (𝑊 ∈ Word 𝑉 → (♯‘(𝑊 ++ ⟨“𝑍”⟩)) = ((♯‘𝑊) + 1))
120	119	3ad2ant1 1151	. . . . . . . . . . . . . . 15 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) → (♯‘(𝑊 ++ ⟨“𝑍”⟩)) = ((♯‘𝑊) + 1))
121	120	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → (♯‘(𝑊 ++ ⟨“𝑍”⟩)) = ((♯‘𝑊) + 1))
122	121	oveq1d 7455	. . . . . . . . . . . . 13 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → ((♯‘(𝑊 ++ ⟨“𝑍”⟩)) − 1) = (((♯‘𝑊) + 1) − 1))
123		oveq1 7447	. . . . . . . . . . . . . . . . 17 ⊢ ((♯‘𝑊) = (𝑁 + 1) → ((♯‘𝑊) + 1) = ((𝑁 + 1) + 1))
124	123	oveq1d 7455	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘𝑊) = (𝑁 + 1) → (((♯‘𝑊) + 1) − 1) = (((𝑁 + 1) + 1) − 1))
125		1cnd 11326	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ∈ ℕ0 → 1 ∈ ℂ)
126	80, 125	addcld 11352	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℂ)
127	126, 125	pncand 11694	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ ℕ0 → (((𝑁 + 1) + 1) − 1) = (𝑁 + 1))
128	127	3ad2ant1 1151	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) → (((𝑁 + 1) + 1) − 1) = (𝑁 + 1))
129	128	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉) → (((𝑁 + 1) + 1) − 1) = (𝑁 + 1))
130	124, 129	sylan9eq 2818	. . . . . . . . . . . . . . 15 ⊢ (((♯‘𝑊) = (𝑁 + 1) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) → (((♯‘𝑊) + 1) − 1) = (𝑁 + 1))
131	130	3ad2antl2 1205	. . . . . . . . . . . . . 14 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) → (((♯‘𝑊) + 1) − 1) = (𝑁 + 1))
132	131	adantr 486	. . . . . . . . . . . . 13 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → (((♯‘𝑊) + 1) − 1) = (𝑁 + 1))
133	122, 132	eqtrd 2798	. . . . . . . . . . . 12 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → ((♯‘(𝑊 ++ ⟨“𝑍”⟩)) − 1) = (𝑁 + 1))
134	133	oveq2d 7456	. . . . . . . . . . 11 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → (0..^((♯‘(𝑊 ++ ⟨“𝑍”⟩)) − 1)) = (0..^(𝑁 + 1)))
135	118, 134	raleqtrrdv 3327	. . . . . . . . . 10 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → ∀𝑖 ∈ (0..^((♯‘(𝑊 ++ ⟨“𝑍”⟩)) − 1)){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸)
136	135	exp42 441	. . . . . . . . 9 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) → ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) → (𝑍 ∈ 𝑉 → ({(lastS‘𝑊), 𝑍} ∈ 𝐸 → ∀𝑖 ∈ (0..^((♯‘(𝑊 ++ ⟨“𝑍”⟩)) − 1)){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸))))
137	14, 136	syl 18	. . . . . . . 8 ⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) → (𝑍 ∈ 𝑉 → ({(lastS‘𝑊), 𝑍} ∈ 𝐸 → ∀𝑖 ∈ (0..^((♯‘(𝑊 ++ ⟨“𝑍”⟩)) − 1)){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸))))
138	137	imp41 431	. . . . . . 7 ⊢ ((((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → ∀𝑖 ∈ (0..^((♯‘(𝑊 ++ ⟨“𝑍”⟩)) − 1)){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸)
139	138	adantrr 730	. . . . . 6 ⊢ ((((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) ∧ ({(lastS‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸)) → ∀𝑖 ∈ (0..^((♯‘(𝑊 ++ ⟨“𝑍”⟩)) − 1)){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸)
140		lswccats1 14807	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉) → (lastS‘(𝑊 ++ ⟨“𝑍”⟩)) = 𝑍)
141	7, 140	sylancom 600	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) → (lastS‘(𝑊 ++ ⟨“𝑍”⟩)) = 𝑍)
142	68	3ad2ant1 1151	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) → 0 < (𝑁 + 1))
143	70	3ad2ant3 1153	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) → (0 < (♯‘𝑊) ↔ 0 < (𝑁 + 1)))
144	142, 143	mpbird 260	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) → 0 < (♯‘𝑊))
145	144	ad2antlr 740	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) → 0 < (♯‘𝑊))
146		ccatfv0 14753	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ⟨“𝑍”⟩ ∈ Word 𝑉 ∧ 0 < (♯‘𝑊)) → ((𝑊 ++ ⟨“𝑍”⟩)‘0) = (𝑊‘0))
147	7, 9, 145, 146	syl3anc 1399	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) → ((𝑊 ++ ⟨“𝑍”⟩)‘0) = (𝑊‘0))
148	141, 147	preq12d 4702	. . . . . . . . . 10 ⊢ (((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) → {(lastS‘(𝑊 ++ ⟨“𝑍”⟩)), ((𝑊 ++ ⟨“𝑍”⟩)‘0)} = {𝑍, (𝑊‘0)})
149	148	eleq1d 2849	. . . . . . . . 9 ⊢ (((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) → ({(lastS‘(𝑊 ++ ⟨“𝑍”⟩)), ((𝑊 ++ ⟨“𝑍”⟩)‘0)} ∈ 𝐸 ↔ {𝑍, (𝑊‘0)} ∈ 𝐸))
150	149	biimprcd 253	. . . . . . . 8 ⊢ ({𝑍, (𝑊‘0)} ∈ 𝐸 → (((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) → {(lastS‘(𝑊 ++ ⟨“𝑍”⟩)), ((𝑊 ++ ⟨“𝑍”⟩)‘0)} ∈ 𝐸))
151	150	adantl 487	. . . . . . 7 ⊢ (({(lastS‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸) → (((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) → {(lastS‘(𝑊 ++ ⟨“𝑍”⟩)), ((𝑊 ++ ⟨“𝑍”⟩)‘0)} ∈ 𝐸))
152	151	impcom 413	. . . . . 6 ⊢ ((((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) ∧ ({(lastS‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸)) → {(lastS‘(𝑊 ++ ⟨“𝑍”⟩)), ((𝑊 ++ ⟨“𝑍”⟩)‘0)} ∈ 𝐸)
153	12, 139, 152	3jca 1146	. . . . 5 ⊢ ((((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) ∧ ({(lastS‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸)) → ((𝑊 ++ ⟨“𝑍”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑊 ++ ⟨“𝑍”⟩)) − 1)){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘(𝑊 ++ ⟨“𝑍”⟩)), ((𝑊 ++ ⟨“𝑍”⟩)‘0)} ∈ 𝐸))
154		ccatws1len 14793	. . . . . . . 8 ⊢ (𝑊 ∈ Word (Vtx‘𝐺) → (♯‘(𝑊 ++ ⟨“𝑍”⟩)) = ((♯‘𝑊) + 1))
155	154	3ad2ant2 1152	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) → (♯‘(𝑊 ++ ⟨“𝑍”⟩)) = ((♯‘𝑊) + 1))
156	123	3ad2ant3 1153	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) → ((♯‘𝑊) + 1) = ((𝑁 + 1) + 1))
157	80, 125, 125	addassd 11355	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → ((𝑁 + 1) + 1) = (𝑁 + (1 + 1)))
158		1p1e2 12490	. . . . . . . . . 10 ⊢ (1 + 1) = 2
159	158	oveq2i 7451	. . . . . . . . 9 ⊢ (𝑁 + (1 + 1)) = (𝑁 + 2)
160	157, 159	eqtrdi 2814	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ0 → ((𝑁 + 1) + 1) = (𝑁 + 2))
161	160	3ad2ant1 1151	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) → ((𝑁 + 1) + 1) = (𝑁 + 2))
162	155, 156, 161	3eqtrd 2802	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) → (♯‘(𝑊 ++ ⟨“𝑍”⟩)) = (𝑁 + 2))
163	162	ad3antlr 744	. . . . 5 ⊢ ((((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) ∧ ({(lastS‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸)) → (♯‘(𝑊 ++ ⟨“𝑍”⟩)) = (𝑁 + 2))
164		2nn 12440	. . . . . . . . 9 ⊢ 2 ∈ ℕ
165		nn0nnaddcl 12661	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 2 ∈ ℕ) → (𝑁 + 2) ∈ ℕ)
166	164, 165	mpan2 704	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ0 → (𝑁 + 2) ∈ ℕ)
167	166	3ad2ant1 1151	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) → (𝑁 + 2) ∈ ℕ)
168	2, 13	isclwwlknx 30654	. . . . . . 7 ⊢ ((𝑁 + 2) ∈ ℕ → ((𝑊 ++ ⟨“𝑍”⟩) ∈ ((𝑁 + 2) ClWWalksN 𝐺) ↔ (((𝑊 ++ ⟨“𝑍”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑊 ++ ⟨“𝑍”⟩)) − 1)){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘(𝑊 ++ ⟨“𝑍”⟩)), ((𝑊 ++ ⟨“𝑍”⟩)‘0)} ∈ 𝐸) ∧ (♯‘(𝑊 ++ ⟨“𝑍”⟩)) = (𝑁 + 2))))
169	167, 168	syl 18	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) → ((𝑊 ++ ⟨“𝑍”⟩) ∈ ((𝑁 + 2) ClWWalksN 𝐺) ↔ (((𝑊 ++ ⟨“𝑍”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑊 ++ ⟨“𝑍”⟩)) − 1)){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘(𝑊 ++ ⟨“𝑍”⟩)), ((𝑊 ++ ⟨“𝑍”⟩)‘0)} ∈ 𝐸) ∧ (♯‘(𝑊 ++ ⟨“𝑍”⟩)) = (𝑁 + 2))))
170	169	ad3antlr 744	. . . . 5 ⊢ ((((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) ∧ ({(lastS‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸)) → ((𝑊 ++ ⟨“𝑍”⟩) ∈ ((𝑁 + 2) ClWWalksN 𝐺) ↔ (((𝑊 ++ ⟨“𝑍”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑊 ++ ⟨“𝑍”⟩)) − 1)){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘(𝑊 ++ ⟨“𝑍”⟩)), ((𝑊 ++ ⟨“𝑍”⟩)‘0)} ∈ 𝐸) ∧ (♯‘(𝑊 ++ ⟨“𝑍”⟩)) = (𝑁 + 2))))
171	153, 163, 170	mpbir2and 726	. . . 4 ⊢ ((((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) ∧ ({(lastS‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸)) → (𝑊 ++ ⟨“𝑍”⟩) ∈ ((𝑁 + 2) ClWWalksN 𝐺))
172	171	exp31 425	. . 3 ⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) → (𝑍 ∈ 𝑉 → (({(lastS‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸) → (𝑊 ++ ⟨“𝑍”⟩) ∈ ((𝑁 + 2) ClWWalksN 𝐺))))
173	1, 172	mpdan 700	. 2 ⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → (𝑍 ∈ 𝑉 → (({(lastS‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸) → (𝑊 ++ ⟨“𝑍”⟩) ∈ ((𝑁 + 2) ClWWalksN 𝐺))))
174	173	imp 412	1 ⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ 𝑍 ∈ 𝑉) → (({(lastS‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸) → (𝑊 ++ ⟨“𝑍”⟩) ∈ ((𝑁 + 2) ClWWalksN 𝐺)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2147   ≠ wne 2959  ∀wral 3080   ∪ cun 4152  ∅c0 4281  {csn 4588  {cpr 4590   class class class wbr 5106  ‘cfv 6555  (class class class)co 7440  ℂcc 11222  ℝcr 11223  0cc0 11224  1c1 11225   + caddc 11227   < clt 11367   − cmin 11565  ℕcn 12359  2c2 12421  ℕ₀cn0 12630  ℤ_≥cuz 12989  ..^cfzo 13812  ♯chash 14498  Word cword 14682  lastSclsw 14731   ++ cconcat 14739  ⟨“cs1 14766  Vtxcvtx 29601  Edgcedg 29652   WWalksN cwwlksn 30442   ClWWalksN cclwwlkn 30642

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5235  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7772  ax-cnex 11280  ax-resscn 11281  ax-1cn 11282  ax-icn 11283  ax-addcl 11284  ax-addrcl 11285  ax-mulcl 11286  ax-mulrcl 11287  ax-mulcom 11288  ax-addass 11289  ax-mulass 11290  ax-distr 11291  ax-i2m1 11292  ax-1ne0 11293  ax-1rid 11294  ax-rnegex 11295  ax-rrecex 11296  ax-cnre 11297  ax-pre-lttri 11298  ax-pre-lttrn 11299  ax-pre-ltadd 11300  ax-pre-mulgt0 11301

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-int 4911  df-iun 4956  df-br 5107  df-opab 5171  df-mpt 5190  df-tr 5216  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6319  df-ord 6380  df-on 6381  df-lim 6382  df-suc 6383  df-iota 6509  df-fun 6557  df-fn 6558  df-f 6559  df-f1 6560  df-fo 6561  df-f1o 6562  df-fv 6563  df-riota 7397  df-ov 7443  df-oprab 7444  df-mpo 7445  df-om 7899  df-1st 8022  df-2nd 8023  df-frecs 8324  df-wrecs 8355  df-recs 8404  df-rdg 8443  df-1o 8501  df-er 8742  df-map 8874  df-en 8999  df-dom 9000  df-sdom 9001  df-fin 9002  df-card 10044  df-pnf 11369  df-mnf 11370  df-xr 11371  df-ltxr 11372  df-le 11373  df-sub 11567  df-neg 11568  df-nn 12360  df-2 12429  df-n0 12631  df-xnn0 12704  df-z 12718  df-uz 12990  df-rp 13145  df-fz 13664  df-fzo 13813  df-hash 14499  df-word 14683  df-lsw 14732  df-concat 14740  df-s1 14767  df-wwlks 30446  df-wwlksn 30447  df-clwwlk 30600  df-clwwlkn 30643

This theorem is used by:  numclwwlk2lem1  31004