wwlksext2clwwlk - Metamath Proof Explorer

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

Theorem wwlksext2clwwlk 29923

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 29711	. . 3 ⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → (𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)))
2		clwwlkext2edg.v	. . . . . . . . . . . . 13 ⊢ 𝑉 = (Vtx‘𝐺)
3	2	wrdeqi 14519	. . . . . . . . . . . 12 ⊢ Word 𝑉 = Word (Vtx‘𝐺)
4	3	eleq2i 2817	. . . . . . . . . . 11 ⊢ (𝑊 ∈ Word 𝑉 ↔ 𝑊 ∈ Word (Vtx‘𝐺))
5	4	biimpri 227	. . . . . . . . . 10 ⊢ (𝑊 ∈ Word (Vtx‘𝐺) → 𝑊 ∈ Word 𝑉)
6	5	3ad2ant2 1131	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) → 𝑊 ∈ Word 𝑉)
7	6	ad2antlr 725	. . . . . . . 8 ⊢ (((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) → 𝑊 ∈ Word 𝑉)
8		s1cl 14584	. . . . . . . . 9 ⊢ (𝑍 ∈ 𝑉 → ⟨“𝑍”⟩ ∈ Word 𝑉)
9	8	adantl 480	. . . . . . . 8 ⊢ (((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) → ⟨“𝑍”⟩ ∈ Word 𝑉)
10		ccatcl 14556	. . . . . . . 8 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ⟨“𝑍”⟩ ∈ Word 𝑉) → (𝑊 ++ ⟨“𝑍”⟩) ∈ Word 𝑉)
11	7, 9, 10	syl2anc 582	. . . . . . 7 ⊢ (((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) → (𝑊 ++ ⟨“𝑍”⟩) ∈ Word 𝑉)
12	11	adantr 479	. . . . . 6 ⊢ ((((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) ∧ ({(lastS‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸)) → (𝑊 ++ ⟨“𝑍”⟩) ∈ Word 𝑉)
13		clwwlkext2edg.e	. . . . . . . . . 10 ⊢ 𝐸 = (Edg‘𝐺)
14	2, 13	wwlknp 29710	. . . . . . . . 9 ⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸))
15		simplll 773	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑊 ∈ Word 𝑉)
16	8	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀) → ⟨“𝑍”⟩ ∈ Word 𝑉)
17	16	ad2antlr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ 𝑖 ∈ (0..^𝑁)) → ⟨“𝑍”⟩ ∈ Word 𝑉)
18		elfzo0 13705	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑖 ∈ (0..^𝑁) ↔ (𝑖 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝑖 < 𝑁))
19		simp1 1133	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑖 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝑖 < 𝑁) → 𝑖 ∈ ℕ₀)
20		peano2nn 12254	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℕ)
21	20	3ad2ant2 1131	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑖 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝑖 < 𝑁) → (𝑁 + 1) ∈ ℕ)
22		nn0re 12511	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑖 ∈ ℕ₀ → 𝑖 ∈ ℝ)
23	22	3ad2ant1 1130	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑖 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝑖 < 𝑁) → 𝑖 ∈ ℝ)
24		nnre 12249	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
25	24	3ad2ant2 1131	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑖 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝑖 < 𝑁) → 𝑁 ∈ ℝ)
26		peano2re 11417	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑁 ∈ ℝ → (𝑁 + 1) ∈ ℝ)
27	24, 26	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℝ)
28	27	3ad2ant2 1131	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑖 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝑖 < 𝑁) → (𝑁 + 1) ∈ ℝ)
29		simp3 1135	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑖 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝑖 < 𝑁) → 𝑖 < 𝑁)
30	24	ltp1d 12174	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑁 ∈ ℕ → 𝑁 < (𝑁 + 1))
31	30	3ad2ant2 1131	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑖 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝑖 < 𝑁) → 𝑁 < (𝑁 + 1))
32	23, 25, 28, 29, 31	lttrd 11405	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑖 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝑖 < 𝑁) → 𝑖 < (𝑁 + 1))
33		elfzo0 13705	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑖 ∈ (0..^(𝑁 + 1)) ↔ (𝑖 ∈ ℕ₀ ∧ (𝑁 + 1) ∈ ℕ ∧ 𝑖 < (𝑁 + 1)))
34	19, 21, 32, 33	syl3anbrc 1340	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑖 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ ∧ 𝑖 < 𝑁) → 𝑖 ∈ (0..^(𝑁 + 1)))
35	18, 34	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑖 ∈ (0..^𝑁) → 𝑖 ∈ (0..^(𝑁 + 1)))
36	35	adantl 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑖 ∈ (0..^(𝑁 + 1)))
37		oveq2 7425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((♯‘𝑊) = (𝑁 + 1) → (0..^(♯‘𝑊)) = (0..^(𝑁 + 1)))
38	37	adantl 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) → (0..^(♯‘𝑊)) = (0..^(𝑁 + 1)))
39	38	eleq2d 2811	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) → (𝑖 ∈ (0..^(♯‘𝑊)) ↔ 𝑖 ∈ (0..^(𝑁 + 1))))
40	39	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑖 ∈ (0..^(♯‘𝑊)) ↔ 𝑖 ∈ (0..^(𝑁 + 1))))
41	36, 40	mpbird 256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑖 ∈ (0..^(♯‘𝑊)))
42		ccatval1 14559	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ⟨“𝑍”⟩ ∈ Word 𝑉 ∧ 𝑖 ∈ (0..^(♯‘𝑊))) → ((𝑊 ++ ⟨“𝑍”⟩)‘𝑖) = (𝑊‘𝑖))
43	15, 17, 41, 42	syl3anc 1368	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑊 ++ ⟨“𝑍”⟩)‘𝑖) = (𝑊‘𝑖))
44		fzonn0p1p1 13743	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑖 ∈ (0..^𝑁) → (𝑖 + 1) ∈ (0..^(𝑁 + 1)))
45	44	adantl 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑖 + 1) ∈ (0..^(𝑁 + 1)))
46	37	eleq2d 2811	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((♯‘𝑊) = (𝑁 + 1) → ((𝑖 + 1) ∈ (0..^(♯‘𝑊)) ↔ (𝑖 + 1) ∈ (0..^(𝑁 + 1))))
47	46	ad3antlr 729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑖 + 1) ∈ (0..^(♯‘𝑊)) ↔ (𝑖 + 1) ∈ (0..^(𝑁 + 1))))
48	45, 47	mpbird 256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑖 + 1) ∈ (0..^(♯‘𝑊)))
49		ccatval1 14559	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ⟨“𝑍”⟩ ∈ Word 𝑉 ∧ (𝑖 + 1) ∈ (0..^(♯‘𝑊))) → ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1)) = (𝑊‘(𝑖 + 1)))
50	15, 17, 48, 49	syl3anc 1368	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1)) = (𝑊‘(𝑖 + 1)))
51	43, 50	preq12d 4746	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) ∧ 𝑖 ∈ (0..^𝑁)) → {((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} = {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))})
52	51	ex 411	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → (𝑖 ∈ (0..^𝑁) → {((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} = {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))}))
53	52	expcom 412	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀) → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) → (𝑖 ∈ (0..^𝑁) → {((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} = {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))})))
54	53	expcom 412	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑁 ∈ ℕ₀ → (𝑍 ∈ 𝑉 → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) → (𝑖 ∈ (0..^𝑁) → {((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} = {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))}))))
55	54	3ad2ant1 1130	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) → (𝑍 ∈ 𝑉 → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) → (𝑖 ∈ (0..^𝑁) → {((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} = {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))}))))
56	55	imp 405	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉) → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) → (𝑖 ∈ (0..^𝑁) → {((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} = {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))})))
57	56	expdcom 413	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑊 ∈ Word 𝑉 → ((♯‘𝑊) = (𝑁 + 1) → (((𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉) → (𝑖 ∈ (0..^𝑁) → {((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} = {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))}))))
58	57	3imp1 1344	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ((𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ 𝑖 ∈ (0..^𝑁)) → {((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} = {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))})
59	58	eleq1d 2810	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ((𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ 𝑖 ∈ (0..^𝑁)) → ({((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ {(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸))
60	59	ralbidva 3166	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ((𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) → (∀𝑖 ∈ (0..^𝑁){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸))
61	60	biimprd 247	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ((𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) → (∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 → ∀𝑖 ∈ (0..^𝑁){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸))
62	61	3exp 1116	. . . . . . . . . . . . . . . 16 ⊢ (𝑊 ∈ Word 𝑉 → ((♯‘𝑊) = (𝑁 + 1) → (((𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉) → (∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 → ∀𝑖 ∈ (0..^𝑁){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸))))
63	62	com34 91	. . . . . . . . . . . . . . 15 ⊢ (𝑊 ∈ Word 𝑉 → ((♯‘𝑊) = (𝑁 + 1) → (∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 → (((𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉) → ∀𝑖 ∈ (0..^𝑁){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸))))
64	63	3imp1 1344	. . . . . . . . . . . . . 14 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) → ∀𝑖 ∈ (0..^𝑁){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸)
65	64	adantr 479	. . . . . . . . . . . . 13 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → ∀𝑖 ∈ (0..^𝑁){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸)
66		simpll 765	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → 𝑊 ∈ Word 𝑉)
67	8	ad2antrl 726	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → ⟨“𝑍”⟩ ∈ Word 𝑉)
68		nn0p1gt0 12531	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑁 ∈ ℕ₀ → 0 < (𝑁 + 1))
69	68	ad2antll 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → 0 < (𝑁 + 1))
70		breq2 5152	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((♯‘𝑊) = (𝑁 + 1) → (0 < (♯‘𝑊) ↔ 0 < (𝑁 + 1)))
71	70	ad2antlr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → (0 < (♯‘𝑊) ↔ 0 < (𝑁 + 1)))
72	69, 71	mpbird 256	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → 0 < (♯‘𝑊))
73		hashneq0 14355	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑊 ∈ Word 𝑉 → (0 < (♯‘𝑊) ↔ 𝑊 ≠ ∅))
74	73	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → (0 < (♯‘𝑊) ↔ 𝑊 ≠ ∅))
75	72, 74	mpbid 231	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → 𝑊 ≠ ∅)
76		ccatval1lsw 14566	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ⟨“𝑍”⟩ ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → ((𝑊 ++ ⟨“𝑍”⟩)‘((♯‘𝑊) − 1)) = (lastS‘𝑊))
77	66, 67, 75, 76	syl3anc 1368	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → ((𝑊 ++ ⟨“𝑍”⟩)‘((♯‘𝑊) − 1)) = (lastS‘𝑊))
78		oveq1 7424	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((♯‘𝑊) = (𝑁 + 1) → ((♯‘𝑊) − 1) = ((𝑁 + 1) − 1))
79	78	ad2antlr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → ((♯‘𝑊) − 1) = ((𝑁 + 1) − 1))
80		nn0cn 12512	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ ℂ)
81	80	ad2antll 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → 𝑁 ∈ ℂ)
82		pncan1 11668	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑁 ∈ ℂ → ((𝑁 + 1) − 1) = 𝑁)
83	81, 82	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → ((𝑁 + 1) − 1) = 𝑁)
84	79, 83	eqtrd 2765	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → ((♯‘𝑊) − 1) = 𝑁)
85	84	fveq2d 6898	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → ((𝑊 ++ ⟨“𝑍”⟩)‘((♯‘𝑊) − 1)) = ((𝑊 ++ ⟨“𝑍”⟩)‘𝑁))
86	77, 85	eqtr3d 2767	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → (lastS‘𝑊) = ((𝑊 ++ ⟨“𝑍”⟩)‘𝑁))
87		ccatws1ls 14615	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉) → ((𝑊 ++ ⟨“𝑍”⟩)‘(♯‘𝑊)) = 𝑍)
88	87	ad2ant2r 745	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → ((𝑊 ++ ⟨“𝑍”⟩)‘(♯‘𝑊)) = 𝑍)
89		fveq2 6894	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((♯‘𝑊) = (𝑁 + 1) → ((𝑊 ++ ⟨“𝑍”⟩)‘(♯‘𝑊)) = ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1)))
90	89	ad2antlr 725	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → ((𝑊 ++ ⟨“𝑍”⟩)‘(♯‘𝑊)) = ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1)))
91	88, 90	eqtr3d 2767	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → 𝑍 = ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1)))
92	86, 91	preq12d 4746	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ (𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀)) → {(lastS‘𝑊), 𝑍} = {((𝑊 ++ ⟨“𝑍”⟩)‘𝑁), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1))})
93	92	expcom 412	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ₀) → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) → {(lastS‘𝑊), 𝑍} = {((𝑊 ++ ⟨“𝑍”⟩)‘𝑁), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1))}))
94	93	expcom 412	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ ℕ₀ → (𝑍 ∈ 𝑉 → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) → {(lastS‘𝑊), 𝑍} = {((𝑊 ++ ⟨“𝑍”⟩)‘𝑁), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1))})))
95	94	3ad2ant1 1130	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) → (𝑍 ∈ 𝑉 → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) → {(lastS‘𝑊), 𝑍} = {((𝑊 ++ ⟨“𝑍”⟩)‘𝑁), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1))})))
96	95	imp 405	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉) → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) → {(lastS‘𝑊), 𝑍} = {((𝑊 ++ ⟨“𝑍”⟩)‘𝑁), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1))}))
97	96	com12 32	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1)) → (((𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉) → {(lastS‘𝑊), 𝑍} = {((𝑊 ++ ⟨“𝑍”⟩)‘𝑁), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1))}))
98	97	3adant3 1129	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) → (((𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉) → {(lastS‘𝑊), 𝑍} = {((𝑊 ++ ⟨“𝑍”⟩)‘𝑁), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1))}))
99	98	imp 405	. . . . . . . . . . . . . . . 16 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) → {(lastS‘𝑊), 𝑍} = {((𝑊 ++ ⟨“𝑍”⟩)‘𝑁), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1))})
100	99	eleq1d 2810	. . . . . . . . . . . . . . 15 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) → ({(lastS‘𝑊), 𝑍} ∈ 𝐸 ↔ {((𝑊 ++ ⟨“𝑍”⟩)‘𝑁), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1))} ∈ 𝐸))
101	100	biimpa 475	. . . . . . . . . . . . . 14 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → {((𝑊 ++ ⟨“𝑍”⟩)‘𝑁), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1))} ∈ 𝐸)
102		simprl1 1215	. . . . . . . . . . . . . . . 16 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) → 𝑁 ∈ ℕ₀)
103	102	adantr 479	. . . . . . . . . . . . . . 15 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → 𝑁 ∈ ℕ₀)
104		fveq2 6894	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑁 → ((𝑊 ++ ⟨“𝑍”⟩)‘𝑖) = ((𝑊 ++ ⟨“𝑍”⟩)‘𝑁))
105		fvoveq1 7440	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑁 → ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1)) = ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1)))
106	104, 105	preq12d 4746	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝑁 → {((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} = {((𝑊 ++ ⟨“𝑍”⟩)‘𝑁), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1))})
107	106	eleq1d 2810	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑁 → ({((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ {((𝑊 ++ ⟨“𝑍”⟩)‘𝑁), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1))} ∈ 𝐸))
108	107	ralsng 4678	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ ℕ₀ → (∀𝑖 ∈ {𝑁} {((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ {((𝑊 ++ ⟨“𝑍”⟩)‘𝑁), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1))} ∈ 𝐸))
109	103, 108	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → (∀𝑖 ∈ {𝑁} {((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ {((𝑊 ++ ⟨“𝑍”⟩)‘𝑁), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑁 + 1))} ∈ 𝐸))
110	101, 109	mpbird 256	. . . . . . . . . . . . 13 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → ∀𝑖 ∈ {𝑁} {((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸)
111		ralunb 4190	. . . . . . . . . . . . 13 ⊢ (∀𝑖 ∈ ((0..^𝑁) ∪ {𝑁}){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ (∀𝑖 ∈ (0..^𝑁){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸 ∧ ∀𝑖 ∈ {𝑁} {((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸))
112	65, 110, 111	sylanbrc 581	. . . . . . . . . . . 12 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → ∀𝑖 ∈ ((0..^𝑁) ∪ {𝑁}){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸)
113		elnn0uz 12897	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ₀ ↔ 𝑁 ∈ (ℤ_≥‘0))
114	102, 113	sylib 217	. . . . . . . . . . . . . . 15 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) → 𝑁 ∈ (ℤ_≥‘0))
115	114	adantr 479	. . . . . . . . . . . . . 14 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → 𝑁 ∈ (ℤ_≥‘0))
116		fzosplitsn 13772	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ (ℤ_≥‘0) → (0..^(𝑁 + 1)) = ((0..^𝑁) ∪ {𝑁}))
117	115, 116	syl 17	. . . . . . . . . . . . 13 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → (0..^(𝑁 + 1)) = ((0..^𝑁) ∪ {𝑁}))
118	117	raleqdv 3315	. . . . . . . . . . . 12 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → (∀𝑖 ∈ (0..^(𝑁 + 1)){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ ∀𝑖 ∈ ((0..^𝑁) ∪ {𝑁}){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸))
119	112, 118	mpbird 256	. . . . . . . . . . 11 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → ∀𝑖 ∈ (0..^(𝑁 + 1)){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸)
120		ccatws1len 14602	. . . . . . . . . . . . . . . . 17 ⊢ (𝑊 ∈ Word 𝑉 → (♯‘(𝑊 ++ ⟨“𝑍”⟩)) = ((♯‘𝑊) + 1))
121	120	3ad2ant1 1130	. . . . . . . . . . . . . . . 16 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) → (♯‘(𝑊 ++ ⟨“𝑍”⟩)) = ((♯‘𝑊) + 1))
122	121	ad2antrr 724	. . . . . . . . . . . . . . 15 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → (♯‘(𝑊 ++ ⟨“𝑍”⟩)) = ((♯‘𝑊) + 1))
123	122	oveq1d 7432	. . . . . . . . . . . . . 14 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → ((♯‘(𝑊 ++ ⟨“𝑍”⟩)) − 1) = (((♯‘𝑊) + 1) − 1))
124		oveq1 7424	. . . . . . . . . . . . . . . . . 18 ⊢ ((♯‘𝑊) = (𝑁 + 1) → ((♯‘𝑊) + 1) = ((𝑁 + 1) + 1))
125	124	oveq1d 7432	. . . . . . . . . . . . . . . . 17 ⊢ ((♯‘𝑊) = (𝑁 + 1) → (((♯‘𝑊) + 1) − 1) = (((𝑁 + 1) + 1) − 1))
126		1cnd 11239	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ ℕ₀ → 1 ∈ ℂ)
127	80, 126	addcld 11263	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ∈ ℕ₀ → (𝑁 + 1) ∈ ℂ)
128	127, 126	pncand 11602	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ ℕ₀ → (((𝑁 + 1) + 1) − 1) = (𝑁 + 1))
129	128	3ad2ant1 1130	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) → (((𝑁 + 1) + 1) − 1) = (𝑁 + 1))
130	129	adantr 479	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉) → (((𝑁 + 1) + 1) − 1) = (𝑁 + 1))
131	125, 130	sylan9eq 2785	. . . . . . . . . . . . . . . 16 ⊢ (((♯‘𝑊) = (𝑁 + 1) ∧ ((𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) → (((♯‘𝑊) + 1) − 1) = (𝑁 + 1))
132	131	3ad2antl2 1183	. . . . . . . . . . . . . . 15 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) → (((♯‘𝑊) + 1) − 1) = (𝑁 + 1))
133	132	adantr 479	. . . . . . . . . . . . . 14 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → (((♯‘𝑊) + 1) − 1) = (𝑁 + 1))
134	123, 133	eqtrd 2765	. . . . . . . . . . . . 13 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → ((♯‘(𝑊 ++ ⟨“𝑍”⟩)) − 1) = (𝑁 + 1))
135	134	oveq2d 7433	. . . . . . . . . . . 12 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → (0..^((♯‘(𝑊 ++ ⟨“𝑍”⟩)) − 1)) = (0..^(𝑁 + 1)))
136	135	raleqdv 3315	. . . . . . . . . . 11 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → (∀𝑖 ∈ (0..^((♯‘(𝑊 ++ ⟨“𝑍”⟩)) − 1)){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ ∀𝑖 ∈ (0..^(𝑁 + 1)){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸))
137	119, 136	mpbird 256	. . . . . . . . . 10 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) ∧ ((𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) ∧ 𝑍 ∈ 𝑉)) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → ∀𝑖 ∈ (0..^((♯‘(𝑊 ++ ⟨“𝑍”⟩)) − 1)){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸)
138	137	exp42 434	. . . . . . . . 9 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸) → ((𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) → (𝑍 ∈ 𝑉 → ({(lastS‘𝑊), 𝑍} ∈ 𝐸 → ∀𝑖 ∈ (0..^((♯‘(𝑊 ++ ⟨“𝑍”⟩)) − 1)){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸))))
139	14, 138	syl 17	. . . . . . . 8 ⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → ((𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) → (𝑍 ∈ 𝑉 → ({(lastS‘𝑊), 𝑍} ∈ 𝐸 → ∀𝑖 ∈ (0..^((♯‘(𝑊 ++ ⟨“𝑍”⟩)) − 1)){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸))))
140	139	imp41 424	. . . . . . 7 ⊢ ((((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) ∧ {(lastS‘𝑊), 𝑍} ∈ 𝐸) → ∀𝑖 ∈ (0..^((♯‘(𝑊 ++ ⟨“𝑍”⟩)) − 1)){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸)
141	140	adantrr 715	. . . . . 6 ⊢ ((((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) ∧ ({(lastS‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸)) → ∀𝑖 ∈ (0..^((♯‘(𝑊 ++ ⟨“𝑍”⟩)) − 1)){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸)
142		lswccats1 14616	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉) → (lastS‘(𝑊 ++ ⟨“𝑍”⟩)) = 𝑍)
143	7, 142	sylancom 586	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) → (lastS‘(𝑊 ++ ⟨“𝑍”⟩)) = 𝑍)
144	68	3ad2ant1 1130	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) → 0 < (𝑁 + 1))
145	70	3ad2ant3 1132	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) → (0 < (♯‘𝑊) ↔ 0 < (𝑁 + 1)))
146	144, 145	mpbird 256	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) → 0 < (♯‘𝑊))
147	146	ad2antlr 725	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) → 0 < (♯‘𝑊))
148		ccatfv0 14565	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ Word 𝑉 ∧ ⟨“𝑍”⟩ ∈ Word 𝑉 ∧ 0 < (♯‘𝑊)) → ((𝑊 ++ ⟨“𝑍”⟩)‘0) = (𝑊‘0))
149	7, 9, 147, 148	syl3anc 1368	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) → ((𝑊 ++ ⟨“𝑍”⟩)‘0) = (𝑊‘0))
150	143, 149	preq12d 4746	. . . . . . . . . 10 ⊢ (((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) → {(lastS‘(𝑊 ++ ⟨“𝑍”⟩)), ((𝑊 ++ ⟨“𝑍”⟩)‘0)} = {𝑍, (𝑊‘0)})
151	150	eleq1d 2810	. . . . . . . . 9 ⊢ (((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) → ({(lastS‘(𝑊 ++ ⟨“𝑍”⟩)), ((𝑊 ++ ⟨“𝑍”⟩)‘0)} ∈ 𝐸 ↔ {𝑍, (𝑊‘0)} ∈ 𝐸))
152	151	biimprcd 249	. . . . . . . 8 ⊢ ({𝑍, (𝑊‘0)} ∈ 𝐸 → (((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) → {(lastS‘(𝑊 ++ ⟨“𝑍”⟩)), ((𝑊 ++ ⟨“𝑍”⟩)‘0)} ∈ 𝐸))
153	152	adantl 480	. . . . . . 7 ⊢ (({(lastS‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸) → (((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) → {(lastS‘(𝑊 ++ ⟨“𝑍”⟩)), ((𝑊 ++ ⟨“𝑍”⟩)‘0)} ∈ 𝐸))
154	153	impcom 406	. . . . . 6 ⊢ ((((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) ∧ ({(lastS‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸)) → {(lastS‘(𝑊 ++ ⟨“𝑍”⟩)), ((𝑊 ++ ⟨“𝑍”⟩)‘0)} ∈ 𝐸)
155	12, 141, 154	3jca 1125	. . . . 5 ⊢ ((((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) ∧ ({(lastS‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸)) → ((𝑊 ++ ⟨“𝑍”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑊 ++ ⟨“𝑍”⟩)) − 1)){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘(𝑊 ++ ⟨“𝑍”⟩)), ((𝑊 ++ ⟨“𝑍”⟩)‘0)} ∈ 𝐸))
156		ccatws1len 14602	. . . . . . . 8 ⊢ (𝑊 ∈ Word (Vtx‘𝐺) → (♯‘(𝑊 ++ ⟨“𝑍”⟩)) = ((♯‘𝑊) + 1))
157	156	3ad2ant2 1131	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) → (♯‘(𝑊 ++ ⟨“𝑍”⟩)) = ((♯‘𝑊) + 1))
158	124	3ad2ant3 1132	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) → ((♯‘𝑊) + 1) = ((𝑁 + 1) + 1))
159	80, 126, 126	addassd 11266	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ₀ → ((𝑁 + 1) + 1) = (𝑁 + (1 + 1)))
160		1p1e2 12367	. . . . . . . . . 10 ⊢ (1 + 1) = 2
161	160	oveq2i 7428	. . . . . . . . 9 ⊢ (𝑁 + (1 + 1)) = (𝑁 + 2)
162	159, 161	eqtrdi 2781	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ₀ → ((𝑁 + 1) + 1) = (𝑁 + 2))
163	162	3ad2ant1 1130	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) → ((𝑁 + 1) + 1) = (𝑁 + 2))
164	157, 158, 163	3eqtrd 2769	. . . . . 6 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) → (♯‘(𝑊 ++ ⟨“𝑍”⟩)) = (𝑁 + 2))
165	164	ad3antlr 729	. . . . 5 ⊢ ((((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) ∧ ({(lastS‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸)) → (♯‘(𝑊 ++ ⟨“𝑍”⟩)) = (𝑁 + 2))
166		2nn 12315	. . . . . . . . 9 ⊢ 2 ∈ ℕ
167		nn0nnaddcl 12533	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ₀ ∧ 2 ∈ ℕ) → (𝑁 + 2) ∈ ℕ)
168	166, 167	mpan2 689	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ₀ → (𝑁 + 2) ∈ ℕ)
169	168	3ad2ant1 1130	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) → (𝑁 + 2) ∈ ℕ)
170	2, 13	isclwwlknx 29902	. . . . . . 7 ⊢ ((𝑁 + 2) ∈ ℕ → ((𝑊 ++ ⟨“𝑍”⟩) ∈ ((𝑁 + 2) ClWWalksN 𝐺) ↔ (((𝑊 ++ ⟨“𝑍”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑊 ++ ⟨“𝑍”⟩)) − 1)){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘(𝑊 ++ ⟨“𝑍”⟩)), ((𝑊 ++ ⟨“𝑍”⟩)‘0)} ∈ 𝐸) ∧ (♯‘(𝑊 ++ ⟨“𝑍”⟩)) = (𝑁 + 2))))
171	169, 170	syl 17	. . . . . 6 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1)) → ((𝑊 ++ ⟨“𝑍”⟩) ∈ ((𝑁 + 2) ClWWalksN 𝐺) ↔ (((𝑊 ++ ⟨“𝑍”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑊 ++ ⟨“𝑍”⟩)) − 1)){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘(𝑊 ++ ⟨“𝑍”⟩)), ((𝑊 ++ ⟨“𝑍”⟩)‘0)} ∈ 𝐸) ∧ (♯‘(𝑊 ++ ⟨“𝑍”⟩)) = (𝑁 + 2))))
172	171	ad3antlr 729	. . . . 5 ⊢ ((((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) ∧ ({(lastS‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸)) → ((𝑊 ++ ⟨“𝑍”⟩) ∈ ((𝑁 + 2) ClWWalksN 𝐺) ↔ (((𝑊 ++ ⟨“𝑍”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑊 ++ ⟨“𝑍”⟩)) − 1)){((𝑊 ++ ⟨“𝑍”⟩)‘𝑖), ((𝑊 ++ ⟨“𝑍”⟩)‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘(𝑊 ++ ⟨“𝑍”⟩)), ((𝑊 ++ ⟨“𝑍”⟩)‘0)} ∈ 𝐸) ∧ (♯‘(𝑊 ++ ⟨“𝑍”⟩)) = (𝑁 + 2))))
173	155, 165, 172	mpbir2and 711	. . . 4 ⊢ ((((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) ∧ 𝑍 ∈ 𝑉) ∧ ({(lastS‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸)) → (𝑊 ++ ⟨“𝑍”⟩) ∈ ((𝑁 + 2) ClWWalksN 𝐺))
174	173	exp31 418	. . 3 ⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑁 ∈ ℕ₀ ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = (𝑁 + 1))) → (𝑍 ∈ 𝑉 → (({(lastS‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸) → (𝑊 ++ ⟨“𝑍”⟩) ∈ ((𝑁 + 2) ClWWalksN 𝐺))))
175	1, 174	mpdan 685	. 2 ⊢ (𝑊 ∈ (𝑁 WWalksN 𝐺) → (𝑍 ∈ 𝑉 → (({(lastS‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸) → (𝑊 ++ ⟨“𝑍”⟩) ∈ ((𝑁 + 2) ClWWalksN 𝐺))))
176	175	imp 405	1 ⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ 𝑍 ∈ 𝑉) → (({(lastS‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸) → (𝑊 ++ ⟨“𝑍”⟩) ∈ ((𝑁 + 2) ClWWalksN 𝐺)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 ∧ w3a 1084 = wceq 1533 ∈ wcel 2098 ≠ wne 2930 ∀wral 3051 ∪ cun 3943 ∅c0 4323 {csn 4629 {cpr 4631 class class class wbr 5148 ‘cfv 6547 (class class class)co 7417 ℂcc 11136 ℝcr 11137 0cc0 11138 1c1 11139 + caddc 11141 < clt 11278 − cmin 11474 ℕcn 12242 2c2 12297 ℕ₀cn0 12502 ℤ_≥cuz 12852 ..^cfzo 13659 ♯chash 14321 Word cword 14496 lastSclsw 14544 ++ cconcat 14552 ⟨“cs1 14577 Vtxcvtx 28865 Edgcedg 28916 WWalksN cwwlksn 29693 ClWWalksN cclwwlkn 29890

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2696 ax-rep 5285 ax-sep 5299 ax-nul 5306 ax-pow 5364 ax-pr 5428 ax-un 7739 ax-cnex 11194 ax-resscn 11195 ax-1cn 11196 ax-icn 11197 ax-addcl 11198 ax-addrcl 11199 ax-mulcl 11200 ax-mulrcl 11201 ax-mulcom 11202 ax-addass 11203 ax-mulass 11204 ax-distr 11205 ax-i2m1 11206 ax-1ne0 11207 ax-1rid 11208 ax-rnegex 11209 ax-rrecex 11210 ax-cnre 11211 ax-pre-lttri 11212 ax-pre-lttrn 11213 ax-pre-ltadd 11214 ax-pre-mulgt0 11215

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2703 df-cleq 2717 df-clel 2802 df-nfc 2877 df-ne 2931 df-nel 3037 df-ral 3052 df-rex 3061 df-reu 3365 df-rab 3420 df-v 3465 df-sbc 3775 df-csb 3891 df-dif 3948 df-un 3950 df-in 3952 df-ss 3962 df-pss 3965 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4909 df-int 4950 df-iun 4998 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5575 df-eprel 5581 df-po 5589 df-so 5590 df-fr 5632 df-we 5634 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-pred 6305 df-ord 6372 df-on 6373 df-lim 6374 df-suc 6375 df-iota 6499 df-fun 6549 df-fn 6550 df-f 6551 df-f1 6552 df-fo 6553 df-f1o 6554 df-fv 6555 df-riota 7373 df-ov 7420 df-oprab 7421 df-mpo 7422 df-om 7870 df-1st 7992 df-2nd 7993 df-frecs 8285 df-wrecs 8316 df-recs 8390 df-rdg 8429 df-1o 8485 df-er 8723 df-map 8845 df-en 8963 df-dom 8964 df-sdom 8965 df-fin 8966 df-card 9962 df-pnf 11280 df-mnf 11281 df-xr 11282 df-ltxr 11283 df-le 11284 df-sub 11476 df-neg 11477 df-nn 12243 df-2 12305 df-n0 12503 df-xnn0 12575 df-z 12589 df-uz 12853 df-rp 13007 df-fz 13517 df-fzo 13660 df-hash 14322 df-word 14497 df-lsw 14545 df-concat 14553 df-s1 14578 df-wwlks 29697 df-wwlksn 29698 df-clwwlk 29848 df-clwwlkn 29891

This theorem is referenced by: numclwwlk2lem1 30242

W3C validator