Theorem wwlksext2clwwlk 30511

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 30296	. . 3 ⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)))
2		clwwlkext2edg.v	. . . . . . . . . . . . 13 ⊢ 𝑉 = (Vtx‘𝐺)
3	2	wrdeqi 14602	. . . . . . . . . . . 12 ⊢ Word 𝑉 = Word (Vtx‘𝐺)
4	3	eleq2i 2854	. . . . . . . . . . 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 14669	. . . . . . . . 9 ⊢ (𝑍 ∈ 𝑉 → ⟨“𝑍”⟩ ∈ Word 𝑉)
9	8	adantl 487	. . . . . . . 8 ⊢ (((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) → ⟨“𝑍”⟩ ∈ Word 𝑉)
10		ccatcl 14639	. . . . . . . 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 30295	. . . . . . . . 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 13756	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑖 ∈ (0..^𝑁) ↔ (𝑖 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝑖 < 𝑁))
19		simp1 1154	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑖 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝑖 < 𝑁) → 𝑖 ∈ ℕ0)
20		peano2nn 12270	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℕ)
21	20	3ad2ant2 1152	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑖 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝑖 < 𝑁) → (𝑁 + 1) ∈ ℕ)
22		nn0re 12538	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑖 ∈ ℕ0 → 𝑖 ∈ ℝ)
23	22	3ad2ant1 1151	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑖 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝑖 < 𝑁) → 𝑖 ∈ ℝ)
24		nnre 12265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
25	24	3ad2ant2 1152	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑖 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝑖 < 𝑁) → 𝑁 ∈ ℝ)
26		peano2re 11408	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑁 ∈ ℝ → (𝑁 + 1) ∈ ℝ)
27	24, 26	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℝ)
28	27	3ad2ant2 1152	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑖 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝑖 < 𝑁) → (𝑁 + 1) ∈ ℝ)
29		simp3 1156	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑖 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝑖 < 𝑁) → 𝑖 < 𝑁)
30	24	ltp1d 12170	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑁 ∈ ℕ → 𝑁 < (𝑁 + 1))
31	30	3ad2ant2 1152	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑖 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝑖 < 𝑁) → 𝑁 < (𝑁 + 1))
32	23, 25, 28, 29, 31	lttrd 11396	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑖 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝑖 < 𝑁) → 𝑖 < (𝑁 + 1))
33		elfzo0 13756	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((♯‘𝑊) = (𝑁 + 1) → (0..^(♯‘𝑊)) = (0..^(𝑁 + 1)))
38	37	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) → (0..^(♯‘𝑊)) = (0..^(𝑁 + 1)))
39	38	eleq2d 2848	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 14642	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ⟨“𝑍”⟩ ∈ Word 𝑉 ∧ 𝑖 ∈ (0..^(♯‘𝑊))) → ((𝑊 ++ ⟨“𝑍”⟩)‘𝑖) = (𝑊‘𝑖))
43	15, 17, 41, 42	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑊 ++ ⟨“𝑍”⟩)‘𝑖) = (𝑊‘𝑖))
44		fzonn0p1p1 13800	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑖 ∈ (0..^𝑁) → (𝑖 + 1) ∈ (0..^(𝑁 + 1)))
45	44	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑖 + 1) ∈ (0..^(𝑁 + 1)))
46	37	eleq2d 2848	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 14642	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ⟨“𝑍”⟩ ∈ Word 𝑉 ∧ (𝑖 + 1) ∈ (0..^(♯‘𝑊))) → ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1)) = (𝑊‘(𝑖 + 1)))
50	15, 17, 48, 49	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1)) = (𝑊‘(𝑖 + 1)))
51	43, 50	preq12d 4705	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 2847	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ 𝑖 ∈ (0..^𝑁)) → ({((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸))
60	59	ralbidva 3185	. . . . . . . . . . . . . . . . . 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 12558	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑁 ∈ ℕ0 → 0 < (𝑁 + 1))
69	68	ad2antll 742	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → 0 < (𝑁 + 1))
70		breq2 5111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 14428	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑊 ∈ Word 𝑉 → (0 < (♯‘𝑊) ↔ 𝑊 ≠ ∅))
74	73	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → (0 < (♯‘𝑊) ↔ 𝑊 ≠ ∅))
75	72, 74	mpbid 235	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → 𝑊 ≠ ∅)
76		ccatval1lsw 14650	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ⟨“𝑍”⟩ ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → ((𝑊 ++ ⟨“𝑍”⟩)‘((♯‘𝑊) − 1)) = (lastS‘𝑊))
77	66, 67, 75, 76	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → ((𝑊 ++ ⟨“𝑍”⟩)‘((♯‘𝑊) − 1)) = (lastS‘𝑊))
78		oveq1 7423	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((♯‘𝑊) = (𝑁 + 1) → ((♯‘𝑊) − 1) = ((𝑁 + 1) − 1))
79	78	ad2antlr 740	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → ((♯‘𝑊) − 1) = ((𝑁 + 1) − 1))
80		nn0cn 12539	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ)
81	80	ad2antll 742	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → 𝑁 ∈ ℂ)
82		pncan1 11663	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑁 ∈ ℂ → ((𝑁 + 1) − 1) = 𝑁)
83	81, 82	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → ((𝑁 + 1) − 1) = 𝑁)
84	79, 83	eqtrd 2797	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → ((♯‘𝑊) − 1) = 𝑁)
85	84	fveq2d 6886	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → ((𝑊 ++ ⟨“𝑍”⟩)‘((♯‘𝑊) − 1)) = ((𝑊 ++ ⟨“𝑍”⟩)‘𝑁))
86	77, 85	eqtr3d 2799	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → (lastS‘𝑊) = ((𝑊 ++ ⟨“𝑍”⟩)‘𝑁))
87		ccatws1ls 14701	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉) → ((𝑊 ++ ⟨“𝑍”⟩)‘(♯‘𝑊)) = 𝑍)
88	87	ad2ant2r 760	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → ((𝑊 ++ ⟨“𝑍”⟩)‘(♯‘𝑊)) = 𝑍)
89		fveq2 6882	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((♯‘𝑊) = (𝑁 + 1) → ((𝑊 ++ ⟨“𝑍”⟩)‘(♯‘𝑊)) = ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1)))
90	89	ad2antlr 740	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → ((𝑊 ++ ⟨“𝑍”⟩)‘(♯‘𝑊)) = ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1)))
91	88, 90	eqtr3d 2799	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → 𝑍 = ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1)))
92	86, 91	preq12d 4705	. . . . . . . . . . . . . . . . . . . . . . 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 2847	. . . . . . . . . . . . . . 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 6882	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑁 → ((𝑊 ++ ⟨“𝑍”⟩)‘𝑖) = ((𝑊 ++ ⟨“𝑍”⟩)‘𝑁))
105		fvoveq1 7439	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑁 → ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1)) = ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1)))
106	104, 105	preq12d 4705	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝑁 → {((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} = {((𝑊 ++ ⟨“𝑍”⟩)‘𝑁), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1))})
107	106	eleq1d 2847	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑁 → ({((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ {((𝑊 ++ ⟨“𝑍”⟩)‘𝑁), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1))} ∈ 𝐸))
108	107	ralsng 4639	. . . . . . . . . . . . . . 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 4146	. . . . . . . . . . . . 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 12929	. . . . . . . . . . . . . . 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 13832	. . . . . . . . . . . . 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 3325	. . . . . . . . . . 11 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → ∀𝑖 ∈ (0..^(𝑁 + 1)){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸)
119		ccatws1len 14688	. . . . . . . . . . . . . . . 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 7431	. . . . . . . . . . . . 13 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → ((♯‘(𝑊 ++ ⟨“𝑍”⟩)) − 1) = (((♯‘𝑊) + 1) − 1))
123		oveq1 7423	. . . . . . . . . . . . . . . . 17 ⊢ ((♯‘𝑊) = (𝑁 + 1) → ((♯‘𝑊) + 1) = ((𝑁 + 1) + 1))
124	123	oveq1d 7431	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘𝑊) = (𝑁 + 1) → (((♯‘𝑊) + 1) − 1) = (((𝑁 + 1) + 1) − 1))
125		1cnd 11227	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ∈ ℕ0 → 1 ∈ ℂ)
126	80, 125	addcld 11253	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℂ)
127	126, 125	pncand 11595	. . . . . . . . . . . . . . . . . 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 2817	. . . . . . . . . . . . . . 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 2797	. . . . . . . . . . . 12 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → ((♯‘(𝑊 ++ ⟨“𝑍”⟩)) − 1) = (𝑁 + 1))
134	133	oveq2d 7432	. . . . . . . . . . 11 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → (0..^((♯‘(𝑊 ++ ⟨“𝑍”⟩)) − 1)) = (0..^(𝑁 + 1)))
135	118, 134	raleqtrrdv 3325	. . . . . . . . . 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 14702	. . . . . . . . . . . 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 14649	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ⟨“𝑍”⟩ ∈ Word 𝑉 ∧ 0 < (♯‘𝑊)) → ((𝑊 ++ ⟨“𝑍”⟩)‘0) = (𝑊‘0))
147	7, 9, 145, 146	syl3anc 1398	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) → ((𝑊 ++ ⟨“𝑍”⟩)‘0) = (𝑊‘0))
148	141, 147	preq12d 4705	. . . . . . . . . 10 ⊢ (((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) → {(lastS‘(𝑊 ++ ⟨“𝑍”⟩)), ((𝑊 ++ ⟨“𝑍”⟩)‘0)} = {𝑍, (𝑊‘0)})
149	148	eleq1d 2847	. . . . . . . . 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 14688	. . . . . . . 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 11256	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → ((𝑁 + 1) + 1) = (𝑁 + (1 + 1)))
158		1p1e2 12389	. . . . . . . . . 10 ⊢ (1 + 1) = 2
159	158	oveq2i 7427	. . . . . . . . 9 ⊢ (𝑁 + (1 + 1)) = (𝑁 + 2)
160	157, 159	eqtrdi 2813	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ0 → ((𝑁 + 1) + 1) = (𝑁 + 2))
161	160	3ad2ant1 1151	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) → ((𝑁 + 1) + 1) = (𝑁 + 2))
162	155, 156, 161	3eqtrd 2801	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) → (♯‘(𝑊 ++ ⟨“𝑍”⟩)) = (𝑁 + 2))
163	162	ad3antlr 744	. . . . 5 ⊢ ((((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) ∧ ({(lastS‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸)) → (♯‘(𝑊 ++ ⟨“𝑍”⟩)) = (𝑁 + 2))
164		2nn 12339	. . . . . . . . 9 ⊢ 2 ∈ ℕ
165		nn0nnaddcl 12560	. . . . . . . . 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 30490	. . . . . . 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 2145   ≠ wne 2957  ∀wral 3078   ∪ cun 3900  ∅c0 4282  {csn 4587  {cpr 4589   class class class wbr 5107  ‘cfv 6537  (class class class)co 7416  ℂcc 11123  ℝcr 11124  0cc0 11125  1c1 11126   + caddc 11128   < clt 11268   − cmin 11466  ℕcn 12258  2c2 12320  ℕ₀cn0 12529  ℤ_≥cuz 12888  ..^cfzo 13709  ♯chash 14394  Word cword 14578  lastSclsw 14627   ++ cconcat 14635  ⟨“cs1 14662  Vtxcvtx 29437  Edgcedg 29488   WWalksN cwwlksn 30278   ClWWalksN cclwwlkn 30478

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-rep 5236  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7739  ax-cnex 11181  ax-resscn 11182  ax-1cn 11183  ax-icn 11184  ax-addcl 11185  ax-addrcl 11186  ax-mulcl 11187  ax-mulrcl 11188  ax-mulcom 11189  ax-addass 11190  ax-mulass 11191  ax-distr 11192  ax-i2m1 11193  ax-1ne0 11194  ax-1rid 11195  ax-rnegex 11196  ax-rrecex 11197  ax-cnre 11198  ax-pre-lttri 11199  ax-pre-lttrn 11200  ax-pre-ltadd 11201  ax-pre-mulgt0 11202

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 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-int 4911  df-iun 4956  df-br 5108  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7373  df-ov 7419  df-oprab 7420  df-mpo 7421  df-om 7866  df-1st 7989  df-2nd 7990  df-frecs 8283  df-wrecs 8314  df-recs 8363  df-rdg 8402  df-1o 8458  df-er 8699  df-map 8831  df-en 8956  df-dom 8957  df-sdom 8958  df-fin 8959  df-card 9947  df-pnf 11270  df-mnf 11271  df-xr 11272  df-ltxr 11273  df-le 11274  df-sub 11468  df-neg 11469  df-nn 12259  df-2 12328  df-n0 12530  df-xnn0 12603  df-z 12617  df-uz 12889  df-rp 13043  df-fz 13562  df-fzo 13710  df-hash 14395  df-word 14579  df-lsw 14628  df-concat 14636  df-s1 14663  df-wwlks 30282  df-wwlksn 30283  df-clwwlk 30436  df-clwwlkn 30479

This theorem is used by:  numclwwlk2lem1  30840