Theorem wwlksext2clwwlk 30089

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 29877	. . 3 ⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)))
2		clwwlkext2edg.v	. . . . . . . . . . . . 13 ⊢ 𝑉 = (Vtx‘𝐺)
3	2	wrdeqi 14585	. . . . . . . . . . . 12 ⊢ Word 𝑉 = Word (Vtx‘𝐺)
4	3	eleq2i 2836	. . . . . . . . . . 11 ⊢ (𝑊 ∈ Word 𝑉 ↔ 𝑊 ∈ Word (Vtx‘𝐺))
5	4	biimpri 228	. . . . . . . . . 10 ⊢ (𝑊 ∈ Word (Vtx‘𝐺) → 𝑊 ∈ Word 𝑉)
6	5	3ad2ant2 1134	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) → 𝑊 ∈ Word 𝑉)
7	6	ad2antlr 726	. . . . . . . 8 ⊢ (((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) → 𝑊 ∈ Word 𝑉)
8		s1cl 14650	. . . . . . . . 9 ⊢ (𝑍 ∈ 𝑉 → ⟨“𝑍”⟩ ∈ Word 𝑉)
9	8	adantl 481	. . . . . . . 8 ⊢ (((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) → ⟨“𝑍”⟩ ∈ Word 𝑉)
10		ccatcl 14622	. . . . . . . 8 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ⟨“𝑍”⟩ ∈ Word 𝑉) → (𝑊 ++ ⟨“𝑍”⟩) ∈ Word 𝑉)
11	7, 9, 10	syl2anc 583	. . . . . . 7 ⊢ (((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) → (𝑊 ++ ⟨“𝑍”⟩) ∈ Word 𝑉)
12	11	adantr 480	. . . . . 6 ⊢ ((((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) ∧ ({(lastS‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸)) → (𝑊 ++ ⟨“𝑍”⟩) ∈ Word 𝑉)
13		clwwlkext2edg.e	. . . . . . . . . 10 ⊢ 𝐸 = (Edg‘𝐺)
14	2, 13	wwlknp 29876	. . . . . . . . 9 ⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸))
15		simplll 774	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑊 ∈ Word 𝑉)
16	8	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → ⟨“𝑍”⟩ ∈ Word 𝑉)
17	16	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → ⟨“𝑍”⟩ ∈ Word 𝑉)
18		elfzo0 13757	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑖 ∈ (0..^𝑁) ↔ (𝑖 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝑖 < 𝑁))
19		simp1 1136	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑖 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝑖 < 𝑁) → 𝑖 ∈ ℕ0)
20		peano2nn 12305	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℕ)
21	20	3ad2ant2 1134	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑖 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝑖 < 𝑁) → (𝑁 + 1) ∈ ℕ)
22		nn0re 12562	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑖 ∈ ℕ0 → 𝑖 ∈ ℝ)
23	22	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑖 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝑖 < 𝑁) → 𝑖 ∈ ℝ)
24		nnre 12300	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
25	24	3ad2ant2 1134	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑖 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝑖 < 𝑁) → 𝑁 ∈ ℝ)
26		peano2re 11463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑁 ∈ ℝ → (𝑁 + 1) ∈ ℝ)
27	24, 26	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℝ)
28	27	3ad2ant2 1134	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑖 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝑖 < 𝑁) → (𝑁 + 1) ∈ ℝ)
29		simp3 1138	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑖 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝑖 < 𝑁) → 𝑖 < 𝑁)
30	24	ltp1d 12225	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑁 ∈ ℕ → 𝑁 < (𝑁 + 1))
31	30	3ad2ant2 1134	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑖 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝑖 < 𝑁) → 𝑁 < (𝑁 + 1))
32	23, 25, 28, 29, 31	lttrd 11451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑖 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝑖 < 𝑁) → 𝑖 < (𝑁 + 1))
33		elfzo0 13757	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑖 ∈ (0..^(𝑁 + 1)) ↔ (𝑖 ∈ ℕ0 ∧ (𝑁 + 1) ∈ ℕ ∧ 𝑖 < (𝑁 + 1)))
34	19, 21, 32, 33	syl3anbrc 1343	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑖 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝑖 < 𝑁) → 𝑖 ∈ (0..^(𝑁 + 1)))
35	18, 34	sylbi 217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑖 ∈ (0..^𝑁) → 𝑖 ∈ (0..^(𝑁 + 1)))
36	35	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑖 ∈ (0..^(𝑁 + 1)))
37		oveq2 7456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((♯‘𝑊) = (𝑁 + 1) → (0..^(♯‘𝑊)) = (0..^(𝑁 + 1)))
38	37	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) → (0..^(♯‘𝑊)) = (0..^(𝑁 + 1)))
39	38	eleq2d 2830	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) → (𝑖 ∈ (0..^(♯‘𝑊)) ↔ 𝑖 ∈ (0..^(𝑁 + 1))))
40	39	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑖 ∈ (0..^(♯‘𝑊)) ↔ 𝑖 ∈ (0..^(𝑁 + 1))))
41	36, 40	mpbird 257	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑖 ∈ (0..^(♯‘𝑊)))
42		ccatval1 14625	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ⟨“𝑍”⟩ ∈ Word 𝑉 ∧ 𝑖 ∈ (0..^(♯‘𝑊))) → ((𝑊 ++ ⟨“𝑍”⟩)‘𝑖) = (𝑊‘𝑖))
43	15, 17, 41, 42	syl3anc 1371	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑊 ++ ⟨“𝑍”⟩)‘𝑖) = (𝑊‘𝑖))
44		fzonn0p1p1 13795	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑖 ∈ (0..^𝑁) → (𝑖 + 1) ∈ (0..^(𝑁 + 1)))
45	44	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑖 + 1) ∈ (0..^(𝑁 + 1)))
46	37	eleq2d 2830	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((♯‘𝑊) = (𝑁 + 1) → ((𝑖 + 1) ∈ (0..^(♯‘𝑊)) ↔ (𝑖 + 1) ∈ (0..^(𝑁 + 1))))
47	46	ad3antlr 730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑖 + 1) ∈ (0..^(♯‘𝑊)) ↔ (𝑖 + 1) ∈ (0..^(𝑁 + 1))))
48	45, 47	mpbird 257	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑖 + 1) ∈ (0..^(♯‘𝑊)))
49		ccatval1 14625	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ⟨“𝑍”⟩ ∈ Word 𝑉 ∧ (𝑖 + 1) ∈ (0..^(♯‘𝑊))) → ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1)) = (𝑊‘(𝑖 + 1)))
50	15, 17, 48, 49	syl3anc 1371	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1)) = (𝑊‘(𝑖 + 1)))
51	43, 50	preq12d 4766	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑖 ∈ (0..^𝑁)) → {((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} = {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))})
52	51	ex 412	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → (𝑖 ∈ (0..^𝑁) → {((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} = {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))}))
53	52	expcom 413	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) → (𝑖 ∈ (0..^𝑁) → {((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} = {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))})))
54	53	expcom 413	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑁 ∈ ℕ0 → (𝑍 ∈ 𝑉 → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) → (𝑖 ∈ (0..^𝑁) → {((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} = {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))}))))
55	54	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) → (𝑍 ∈ 𝑉 → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) → (𝑖 ∈ (0..^𝑁) → {((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} = {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))}))))
56	55	imp 406	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉) → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) → (𝑖 ∈ (0..^𝑁) → {((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} = {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))})))
57	56	expdcom 414	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑊 ∈ Word 𝑉 → ((♯‘𝑊) = (𝑁 + 1) → (((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉) → (𝑖 ∈ (0..^𝑁) → {((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} = {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))}))))
58	57	3imp1 1347	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ 𝑖 ∈ (0..^𝑁)) → {((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} = {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))})
59	58	eleq1d 2829	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ 𝑖 ∈ (0..^𝑁)) → ({((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸))
60	59	ralbidva 3182	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) → (∀𝑖 ∈ (0..^𝑁){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸))
61	60	biimprd 248	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) → (∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 → ∀𝑖 ∈ (0..^𝑁){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸))
62	61	3exp 1119	. . . . . . . . . . . . . . . 16 ⊢ (𝑊 ∈ Word 𝑉 → ((♯‘𝑊) = (𝑁 + 1) → (((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉) → (∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 → ∀𝑖 ∈ (0..^𝑁){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸))))
63	62	com34 91	. . . . . . . . . . . . . . 15 ⊢ (𝑊 ∈ Word 𝑉 → ((♯‘𝑊) = (𝑁 + 1) → (∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 → (((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉) → ∀𝑖 ∈ (0..^𝑁){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸))))
64	63	3imp1 1347	. . . . . . . . . . . . . 14 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) → ∀𝑖 ∈ (0..^𝑁){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸)
65	64	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → ∀𝑖 ∈ (0..^𝑁){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸)
66		simpll 766	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → 𝑊 ∈ Word 𝑉)
67	8	ad2antrl 727	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → ⟨“𝑍”⟩ ∈ Word 𝑉)
68		nn0p1gt0 12582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑁 ∈ ℕ0 → 0 < (𝑁 + 1))
69	68	ad2antll 728	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → 0 < (𝑁 + 1))
70		breq2 5170	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((♯‘𝑊) = (𝑁 + 1) → (0 < (♯‘𝑊) ↔ 0 < (𝑁 + 1)))
71	70	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → (0 < (♯‘𝑊) ↔ 0 < (𝑁 + 1)))
72	69, 71	mpbird 257	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → 0 < (♯‘𝑊))
73		hashneq0 14413	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑊 ∈ Word 𝑉 → (0 < (♯‘𝑊) ↔ 𝑊 ≠ ∅))
74	73	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → (0 < (♯‘𝑊) ↔ 𝑊 ≠ ∅))
75	72, 74	mpbid 232	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → 𝑊 ≠ ∅)
76		ccatval1lsw 14632	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ⟨“𝑍”⟩ ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → ((𝑊 ++ ⟨“𝑍”⟩)‘((♯‘𝑊) − 1)) = (lastS‘𝑊))
77	66, 67, 75, 76	syl3anc 1371	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → ((𝑊 ++ ⟨“𝑍”⟩)‘((♯‘𝑊) − 1)) = (lastS‘𝑊))
78		oveq1 7455	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((♯‘𝑊) = (𝑁 + 1) → ((♯‘𝑊) − 1) = ((𝑁 + 1) − 1))
79	78	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → ((♯‘𝑊) − 1) = ((𝑁 + 1) − 1))
80		nn0cn 12563	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ)
81	80	ad2antll 728	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → 𝑁 ∈ ℂ)
82		pncan1 11714	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑁 ∈ ℂ → ((𝑁 + 1) − 1) = 𝑁)
83	81, 82	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → ((𝑁 + 1) − 1) = 𝑁)
84	79, 83	eqtrd 2780	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → ((♯‘𝑊) − 1) = 𝑁)
85	84	fveq2d 6924	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → ((𝑊 ++ ⟨“𝑍”⟩)‘((♯‘𝑊) − 1)) = ((𝑊 ++ ⟨“𝑍”⟩)‘𝑁))
86	77, 85	eqtr3d 2782	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → (lastS‘𝑊) = ((𝑊 ++ ⟨“𝑍”⟩)‘𝑁))
87		ccatws1ls 14681	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉) → ((𝑊 ++ ⟨“𝑍”⟩)‘(♯‘𝑊)) = 𝑍)
88	87	ad2ant2r 746	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → ((𝑊 ++ ⟨“𝑍”⟩)‘(♯‘𝑊)) = 𝑍)
89		fveq2 6920	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((♯‘𝑊) = (𝑁 + 1) → ((𝑊 ++ ⟨“𝑍”⟩)‘(♯‘𝑊)) = ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1)))
90	89	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → ((𝑊 ++ ⟨“𝑍”⟩)‘(♯‘𝑊)) = ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1)))
91	88, 90	eqtr3d 2782	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → 𝑍 = ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1)))
92	86, 91	preq12d 4766	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0)) → {(lastS‘𝑊), 𝑍} = {((𝑊 ++ ⟨“𝑍”⟩)‘𝑁), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1))})
93	92	expcom 413	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) → {(lastS‘𝑊), 𝑍} = {((𝑊 ++ ⟨“𝑍”⟩)‘𝑁), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1))}))
94	93	expcom 413	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ ℕ0 → (𝑍 ∈ 𝑉 → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) → {(lastS‘𝑊), 𝑍} = {((𝑊 ++ ⟨“𝑍”⟩)‘𝑁), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1))})))
95	94	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) → (𝑍 ∈ 𝑉 → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) → {(lastS‘𝑊), 𝑍} = {((𝑊 ++ ⟨“𝑍”⟩)‘𝑁), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1))})))
96	95	imp 406	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉) → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) → {(lastS‘𝑊), 𝑍} = {((𝑊 ++ ⟨“𝑍”⟩)‘𝑁), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1))}))
97	96	com12 32	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) → (((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉) → {(lastS‘𝑊), 𝑍} = {((𝑊 ++ ⟨“𝑍”⟩)‘𝑁), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1))}))
98	97	3adant3 1132	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) → (((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉) → {(lastS‘𝑊), 𝑍} = {((𝑊 ++ ⟨“𝑍”⟩)‘𝑁), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1))}))
99	98	imp 406	. . . . . . . . . . . . . . . 16 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) → {(lastS‘𝑊), 𝑍} = {((𝑊 ++ ⟨“𝑍”⟩)‘𝑁), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1))})
100	99	eleq1d 2829	. . . . . . . . . . . . . . 15 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) → ({(lastS‘𝑊), 𝑍} ∈ 𝐸 ↔ {((𝑊 ++ ⟨“𝑍”⟩)‘𝑁), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1))} ∈ 𝐸))
101	100	biimpa 476	. . . . . . . . . . . . . 14 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → {((𝑊 ++ ⟨“𝑍”⟩)‘𝑁), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1))} ∈ 𝐸)
102		simprl1 1218	. . . . . . . . . . . . . . . 16 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) → 𝑁 ∈ ℕ0)
103	102	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → 𝑁 ∈ ℕ0)
104		fveq2 6920	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑁 → ((𝑊 ++ ⟨“𝑍”⟩)‘𝑖) = ((𝑊 ++ ⟨“𝑍”⟩)‘𝑁))
105		fvoveq1 7471	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑁 → ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1)) = ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1)))
106	104, 105	preq12d 4766	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝑁 → {((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} = {((𝑊 ++ ⟨“𝑍”⟩)‘𝑁), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1))})
107	106	eleq1d 2829	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑁 → ({((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ {((𝑊 ++ ⟨“𝑍”⟩)‘𝑁), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1))} ∈ 𝐸))
108	107	ralsng 4697	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ ℕ0 → (∀𝑖 ∈ {𝑁} {((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ {((𝑊 ++ ⟨“𝑍”⟩)‘𝑁), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1))} ∈ 𝐸))
109	103, 108	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → (∀𝑖 ∈ {𝑁} {((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ {((𝑊 ++ ⟨“𝑍”⟩)‘𝑁), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1))} ∈ 𝐸))
110	101, 109	mpbird 257	. . . . . . . . . . . . 13 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → ∀𝑖 ∈ {𝑁} {((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸)
111		ralunb 4220	. . . . . . . . . . . . 13 ⊢ (∀𝑖 ∈ ((0..^𝑁) ∪ {𝑁}){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ (∀𝑖 ∈ (0..^𝑁){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸 ∧ ∀𝑖 ∈ {𝑁} {((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸))
112	65, 110, 111	sylanbrc 582	. . . . . . . . . . . 12 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → ∀𝑖 ∈ ((0..^𝑁) ∪ {𝑁}){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸)
113		elnn0uz 12948	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ ℕ0 ↔ 𝑁 ∈ (ℤ≥‘0))
114	102, 113	sylib 218	. . . . . . . . . . . . . 14 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) → 𝑁 ∈ (ℤ≥‘0))
115	114	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → 𝑁 ∈ (ℤ≥‘0))
116		fzosplitsn 13825	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ (ℤ≥‘0) → (0..^(𝑁 + 1)) = ((0..^𝑁) ∪ {𝑁}))
117	115, 116	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → (0..^(𝑁 + 1)) = ((0..^𝑁) ∪ {𝑁}))
118	112, 117	raleqtrrdv 3338	. . . . . . . . . . 11 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → ∀𝑖 ∈ (0..^(𝑁 + 1)){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸)
119		ccatws1len 14668	. . . . . . . . . . . . . . . 16 ⊢ (𝑊 ∈ Word 𝑉 → (♯‘(𝑊 ++ ⟨“𝑍”⟩)) = ((♯‘𝑊) + 1))
120	119	3ad2ant1 1133	. . . . . . . . . . . . . . 15 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) → (♯‘(𝑊 ++ ⟨“𝑍”⟩)) = ((♯‘𝑊) + 1))
121	120	ad2antrr 725	. . . . . . . . . . . . . 14 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → (♯‘(𝑊 ++ ⟨“𝑍”⟩)) = ((♯‘𝑊) + 1))
122	121	oveq1d 7463	. . . . . . . . . . . . 13 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → ((♯‘(𝑊 ++ ⟨“𝑍”⟩)) − 1) = (((♯‘𝑊) + 1) − 1))
123		oveq1 7455	. . . . . . . . . . . . . . . . 17 ⊢ ((♯‘𝑊) = (𝑁 + 1) → ((♯‘𝑊) + 1) = ((𝑁 + 1) + 1))
124	123	oveq1d 7463	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘𝑊) = (𝑁 + 1) → (((♯‘𝑊) + 1) − 1) = (((𝑁 + 1) + 1) − 1))
125		1cnd 11285	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ∈ ℕ0 → 1 ∈ ℂ)
126	80, 125	addcld 11309	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℂ)
127	126, 125	pncand 11648	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ ℕ0 → (((𝑁 + 1) + 1) − 1) = (𝑁 + 1))
128	127	3ad2ant1 1133	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) → (((𝑁 + 1) + 1) − 1) = (𝑁 + 1))
129	128	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉) → (((𝑁 + 1) + 1) − 1) = (𝑁 + 1))
130	124, 129	sylan9eq 2800	. . . . . . . . . . . . . . 15 ⊢ (((♯‘𝑊) = (𝑁 + 1) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) → (((♯‘𝑊) + 1) − 1) = (𝑁 + 1))
131	130	3ad2antl2 1186	. . . . . . . . . . . . . 14 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) → (((♯‘𝑊) + 1) − 1) = (𝑁 + 1))
132	131	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → (((♯‘𝑊) + 1) − 1) = (𝑁 + 1))
133	122, 132	eqtrd 2780	. . . . . . . . . . . 12 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → ((♯‘(𝑊 ++ ⟨“𝑍”⟩)) − 1) = (𝑁 + 1))
134	133	oveq2d 7464	. . . . . . . . . . 11 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → (0..^((♯‘(𝑊 ++ ⟨“𝑍”⟩)) − 1)) = (0..^(𝑁 + 1)))
135	118, 134	raleqtrrdv 3338	. . . . . . . . . 10 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → ∀𝑖 ∈ (0..^((♯‘(𝑊 ++ ⟨“𝑍”⟩)) − 1)){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸)
136	135	exp42 435	. . . . . . . . 9 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) → ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) → (𝑍 ∈ 𝑉 → ({(lastS‘𝑊), 𝑍} ∈ 𝐸 → ∀𝑖 ∈ (0..^((♯‘(𝑊 ++ ⟨“𝑍”⟩)) − 1)){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸))))
137	14, 136	syl 17	. . . . . . . 8 ⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) → (𝑍 ∈ 𝑉 → ({(lastS‘𝑊), 𝑍} ∈ 𝐸 → ∀𝑖 ∈ (0..^((♯‘(𝑊 ++ ⟨“𝑍”⟩)) − 1)){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸))))
138	137	imp41 425	. . . . . . 7 ⊢ ((((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → ∀𝑖 ∈ (0..^((♯‘(𝑊 ++ ⟨“𝑍”⟩)) − 1)){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸)
139	138	adantrr 716	. . . . . 6 ⊢ ((((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) ∧ ({(lastS‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸)) → ∀𝑖 ∈ (0..^((♯‘(𝑊 ++ ⟨“𝑍”⟩)) − 1)){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸)
140		lswccats1 14682	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉) → (lastS‘(𝑊 ++ ⟨“𝑍”⟩)) = 𝑍)
141	7, 140	sylancom 587	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) → (lastS‘(𝑊 ++ ⟨“𝑍”⟩)) = 𝑍)
142	68	3ad2ant1 1133	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) → 0 < (𝑁 + 1))
143	70	3ad2ant3 1135	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) → (0 < (♯‘𝑊) ↔ 0 < (𝑁 + 1)))
144	142, 143	mpbird 257	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) → 0 < (♯‘𝑊))
145	144	ad2antlr 726	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) → 0 < (♯‘𝑊))
146		ccatfv0 14631	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ⟨“𝑍”⟩ ∈ Word 𝑉 ∧ 0 < (♯‘𝑊)) → ((𝑊 ++ ⟨“𝑍”⟩)‘0) = (𝑊‘0))
147	7, 9, 145, 146	syl3anc 1371	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) → ((𝑊 ++ ⟨“𝑍”⟩)‘0) = (𝑊‘0))
148	141, 147	preq12d 4766	. . . . . . . . . 10 ⊢ (((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) → {(lastS‘(𝑊 ++ ⟨“𝑍”⟩)), ((𝑊 ++ ⟨“𝑍”⟩)‘0)} = {𝑍, (𝑊‘0)})
149	148	eleq1d 2829	. . . . . . . . 9 ⊢ (((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) → ({(lastS‘(𝑊 ++ ⟨“𝑍”⟩)), ((𝑊 ++ ⟨“𝑍”⟩)‘0)} ∈ 𝐸 ↔ {𝑍, (𝑊‘0)} ∈ 𝐸))
150	149	biimprcd 250	. . . . . . . 8 ⊢ ({𝑍, (𝑊‘0)} ∈ 𝐸 → (((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) → {(lastS‘(𝑊 ++ ⟨“𝑍”⟩)), ((𝑊 ++ ⟨“𝑍”⟩)‘0)} ∈ 𝐸))
151	150	adantl 481	. . . . . . 7 ⊢ (({(lastS‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸) → (((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) → {(lastS‘(𝑊 ++ ⟨“𝑍”⟩)), ((𝑊 ++ ⟨“𝑍”⟩)‘0)} ∈ 𝐸))
152	151	impcom 407	. . . . . 6 ⊢ ((((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) ∧ ({(lastS‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸)) → {(lastS‘(𝑊 ++ ⟨“𝑍”⟩)), ((𝑊 ++ ⟨“𝑍”⟩)‘0)} ∈ 𝐸)
153	12, 139, 152	3jca 1128	. . . . 5 ⊢ ((((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) ∧ ({(lastS‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸)) → ((𝑊 ++ ⟨“𝑍”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑊 ++ ⟨“𝑍”⟩)) − 1)){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘(𝑊 ++ ⟨“𝑍”⟩)), ((𝑊 ++ ⟨“𝑍”⟩)‘0)} ∈ 𝐸))
154		ccatws1len 14668	. . . . . . . 8 ⊢ (𝑊 ∈ Word (Vtx‘𝐺) → (♯‘(𝑊 ++ ⟨“𝑍”⟩)) = ((♯‘𝑊) + 1))
155	154	3ad2ant2 1134	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) → (♯‘(𝑊 ++ ⟨“𝑍”⟩)) = ((♯‘𝑊) + 1))
156	123	3ad2ant3 1135	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) → ((♯‘𝑊) + 1) = ((𝑁 + 1) + 1))
157	80, 125, 125	addassd 11312	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → ((𝑁 + 1) + 1) = (𝑁 + (1 + 1)))
158		1p1e2 12418	. . . . . . . . . 10 ⊢ (1 + 1) = 2
159	158	oveq2i 7459	. . . . . . . . 9 ⊢ (𝑁 + (1 + 1)) = (𝑁 + 2)
160	157, 159	eqtrdi 2796	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ0 → ((𝑁 + 1) + 1) = (𝑁 + 2))
161	160	3ad2ant1 1133	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) → ((𝑁 + 1) + 1) = (𝑁 + 2))
162	155, 156, 161	3eqtrd 2784	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) → (♯‘(𝑊 ++ ⟨“𝑍”⟩)) = (𝑁 + 2))
163	162	ad3antlr 730	. . . . 5 ⊢ ((((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) ∧ ({(lastS‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸)) → (♯‘(𝑊 ++ ⟨“𝑍”⟩)) = (𝑁 + 2))
164		2nn 12366	. . . . . . . . 9 ⊢ 2 ∈ ℕ
165		nn0nnaddcl 12584	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 2 ∈ ℕ) → (𝑁 + 2) ∈ ℕ)
166	164, 165	mpan2 690	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ0 → (𝑁 + 2) ∈ ℕ)
167	166	3ad2ant1 1133	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) → (𝑁 + 2) ∈ ℕ)
168	2, 13	isclwwlknx 30068	. . . . . . 7 ⊢ ((𝑁 + 2) ∈ ℕ → ((𝑊 ++ ⟨“𝑍”⟩) ∈ ((𝑁 + 2) ClWWalksN 𝐺) ↔ (((𝑊 ++ ⟨“𝑍”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑊 ++ ⟨“𝑍”⟩)) − 1)){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘(𝑊 ++ ⟨“𝑍”⟩)), ((𝑊 ++ ⟨“𝑍”⟩)‘0)} ∈ 𝐸) ∧ (♯‘(𝑊 ++ ⟨“𝑍”⟩)) = (𝑁 + 2))))
169	167, 168	syl 17	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) → ((𝑊 ++ ⟨“𝑍”⟩) ∈ ((𝑁 + 2) ClWWalksN 𝐺) ↔ (((𝑊 ++ ⟨“𝑍”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑊 ++ ⟨“𝑍”⟩)) − 1)){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘(𝑊 ++ ⟨“𝑍”⟩)), ((𝑊 ++ ⟨“𝑍”⟩)‘0)} ∈ 𝐸) ∧ (♯‘(𝑊 ++ ⟨“𝑍”⟩)) = (𝑁 + 2))))
170	169	ad3antlr 730	. . . . 5 ⊢ ((((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) ∧ ({(lastS‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸)) → ((𝑊 ++ ⟨“𝑍”⟩) ∈ ((𝑁 + 2) ClWWalksN 𝐺) ↔ (((𝑊 ++ ⟨“𝑍”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑊 ++ ⟨“𝑍”⟩)) − 1)){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘(𝑊 ++ ⟨“𝑍”⟩)), ((𝑊 ++ ⟨“𝑍”⟩)‘0)} ∈ 𝐸) ∧ (♯‘(𝑊 ++ ⟨“𝑍”⟩)) = (𝑁 + 2))))
171	153, 163, 170	mpbir2and 712	. . . 4 ⊢ ((((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) ∧ ({(lastS‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸)) → (𝑊 ++ ⟨“𝑍”⟩) ∈ ((𝑁 + 2) ClWWalksN 𝐺))
172	171	exp31 419	. . 3 ⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) → (𝑍 ∈ 𝑉 → (({(lastS‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸) → (𝑊 ++ ⟨“𝑍”⟩) ∈ ((𝑁 + 2) ClWWalksN 𝐺))))
173	1, 172	mpdan 686	. 2 ⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → (𝑍 ∈ 𝑉 → (({(lastS‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸) → (𝑊 ++ ⟨“𝑍”⟩) ∈ ((𝑁 + 2) ClWWalksN 𝐺))))
174	173	imp 406	1 ⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ 𝑍 ∈ 𝑉) → (({(lastS‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸) → (𝑊 ++ ⟨“𝑍”⟩) ∈ ((𝑁 + 2) ClWWalksN 𝐺)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1537   ∈ wcel 2108   ≠ wne 2946  ∀wral 3067   ∪ cun 3974  ∅c0 4352  {csn 4648  {cpr 4650   class class class wbr 5166  ‘cfv 6573  (class class class)co 7448  ℂcc 11182  ℝcr 11183  0cc0 11184  1c1 11185   + caddc 11187   < clt 11324   − cmin 11520  ℕcn 12293  2c2 12348  ℕ₀cn0 12553  ℤ_≥cuz 12903  ..^cfzo 13711  ♯chash 14379  Word cword 14562  lastSclsw 14610   ++ cconcat 14618  ⟨“cs1 14643  Vtxcvtx 29031  Edgcedg 29082   WWalksN cwwlksn 29859   ClWWalksN cclwwlkn 30056

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-rep 5303  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-cnex 11240  ax-resscn 11241  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-mulcom 11248  ax-addass 11249  ax-mulass 11250  ax-distr 11251  ax-i2m1 11252  ax-1ne0 11253  ax-1rid 11254  ax-rnegex 11255  ax-rrecex 11256  ax-cnre 11257  ax-pre-lttri 11258  ax-pre-lttrn 11259  ax-pre-ltadd 11260  ax-pre-mulgt0 11261

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-int 4971  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-riota 7404  df-ov 7451  df-oprab 7452  df-mpo 7453  df-om 7904  df-1st 8030  df-2nd 8031  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-1o 8522  df-er 8763  df-map 8886  df-en 9004  df-dom 9005  df-sdom 9006  df-fin 9007  df-card 10008  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-sub 11522  df-neg 11523  df-nn 12294  df-2 12356  df-n0 12554  df-xnn0 12626  df-z 12640  df-uz 12904  df-rp 13058  df-fz 13568  df-fzo 13712  df-hash 14380  df-word 14563  df-lsw 14611  df-concat 14619  df-s1 14644  df-wwlks 29863  df-wwlksn 29864  df-clwwlk 30014  df-clwwlkn 30057

This theorem is referenced by:  numclwwlk2lem1  30408