Theorem wwlksnext 30494

Description: Extension of a walk (as word) by adding an edge/vertex. (Contributed by Alexander van der Vekens, 4-Aug-2018.) (Revised by AV, 16-Apr-2021.)

Hypotheses

Ref	Expression
wwlksnext.v	⊢ 𝑉 = (Vtx‘𝐺)
wwlksnext.e	⊢ 𝐸 = (Edg‘𝐺)

Assertion

Ref	Expression
wwlksnext	⊢ ((𝑇 ∈ (𝑁 WWalksN 𝐺) ∧ 𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸) → (𝑇 ++ ⟨“𝑆”⟩) ∈ ((𝑁 + 1) WWalksN 𝐺))

Proof of Theorem wwlksnext

Dummy variable 𝑖 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		wwlksnext.v	. . . 4 ⊢ 𝑉 = (Vtx‘𝐺)
2	1	wwlknbp 30443	. . 3 ⊢ (𝑇 ∈ (𝑁 WWalksN 𝐺) → (𝐺 ∈ V ∧ 𝑁 ∈ ℕ0 ∧ 𝑇 ∈ Word 𝑉))
3		wwlksnext.e	. . . . . . . . . . 11 ⊢ 𝐸 = (Edg‘𝐺)
4	1, 3	wwlknp 30444	. . . . . . . . . 10 ⊢ (𝑇 ∈ (𝑁 WWalksN 𝐺) → (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸))
5		simp1 1154	. . . . . . . . . . . . . . 15 ⊢ ((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) → 𝑇 ∈ Word 𝑉)
6		simprl 783	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸)) → 𝑆 ∈ 𝑉)
7		cats1un 14881	. . . . . . . . . . . . . . 15 ⊢ ((𝑇 ∈ Word 𝑉 ∧ 𝑆 ∈ 𝑉) → (𝑇 ++ ⟨“𝑆”⟩) = (𝑇 ∪ {⟨(♯‘𝑇), 𝑆⟩}))
8	5, 6, 7	syl2an 608	. . . . . . . . . . . . . 14 ⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → (𝑇 ++ ⟨“𝑆”⟩) = (𝑇 ∪ {⟨(♯‘𝑇), 𝑆⟩}))
9		opex 5435	. . . . . . . . . . . . . . . . . . 19 ⊢ ⟨(♯‘𝑇), 𝑆⟩ ∈ V
10	9	snnz 4736	. . . . . . . . . . . . . . . . . 18 ⊢ {⟨(♯‘𝑇), 𝑆⟩} ≠ ∅
11	10	neii 2960	. . . . . . . . . . . . . . . . 17 ⊢ ¬ {⟨(♯‘𝑇), 𝑆⟩} = ∅
12	11	intnan 492	. . . . . . . . . . . . . . . 16 ⊢ ¬ (𝑇 = ∅ ∧ {⟨(♯‘𝑇), 𝑆⟩} = ∅)
13		df-ne 2959	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑇 ∪ {⟨(♯‘𝑇), 𝑆⟩}) ≠ ∅ ↔ ¬ (𝑇 ∪ {⟨(♯‘𝑇), 𝑆⟩}) = ∅)
14		un00 4359	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑇 = ∅ ∧ {⟨(♯‘𝑇), 𝑆⟩} = ∅) ↔ (𝑇 ∪ {⟨(♯‘𝑇), 𝑆⟩}) = ∅)
15	13, 14	xchbinxr 338	. . . . . . . . . . . . . . . 16 ⊢ ((𝑇 ∪ {⟨(♯‘𝑇), 𝑆⟩}) ≠ ∅ ↔ ¬ (𝑇 = ∅ ∧ {⟨(♯‘𝑇), 𝑆⟩} = ∅))
16	12, 15	mpbir 234	. . . . . . . . . . . . . . 15 ⊢ (𝑇 ∪ {⟨(♯‘𝑇), 𝑆⟩}) ≠ ∅
17	16	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → (𝑇 ∪ {⟨(♯‘𝑇), 𝑆⟩}) ≠ ∅)
18	8, 17	eqnetrd 3025	. . . . . . . . . . . . 13 ⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → (𝑇 ++ ⟨“𝑆”⟩) ≠ ∅)
19		s1cl 14759	. . . . . . . . . . . . . . 15 ⊢ (𝑆 ∈ 𝑉 → ⟨“𝑆”⟩ ∈ Word 𝑉)
20	19	ad2antrl 741	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸)) → ⟨“𝑆”⟩ ∈ Word 𝑉)
21		ccatcl 14729	. . . . . . . . . . . . . 14 ⊢ ((𝑇 ∈ Word 𝑉 ∧ ⟨“𝑆”⟩ ∈ Word 𝑉) → (𝑇 ++ ⟨“𝑆”⟩) ∈ Word 𝑉)
22	5, 20, 21	syl2an 608	. . . . . . . . . . . . 13 ⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → (𝑇 ++ ⟨“𝑆”⟩) ∈ Word 𝑉)
23		simplrl 789	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑇 ∈ Word 𝑉)
24		fzossfzop1 13888	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑁 ∈ ℕ0 → (0..^𝑁) ⊆ (0..^(𝑁 + 1)))
25	24	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) → (0..^𝑁) ⊆ (0..^(𝑁 + 1)))
26	25	sselda 3912	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑖 ∈ (0..^(𝑁 + 1)))
27		oveq2 7435	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((♯‘𝑇) = (𝑁 + 1) → (0..^(♯‘𝑇)) = (0..^(𝑁 + 1)))
28	27	eleq2d 2849	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((♯‘𝑇) = (𝑁 + 1) → (𝑖 ∈ (0..^(♯‘𝑇)) ↔ 𝑖 ∈ (0..^(𝑁 + 1))))
29	28	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1)) → (𝑖 ∈ (0..^(♯‘𝑇)) ↔ 𝑖 ∈ (0..^(𝑁 + 1))))
30	29	ad2antlr 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑖 ∈ (0..^(♯‘𝑇)) ↔ 𝑖 ∈ (0..^(𝑁 + 1))))
31	26, 30	mpbird 260	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑖 ∈ (0..^(♯‘𝑇)))
32		ccats1val1 14785	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑇 ∈ Word 𝑉 ∧ 𝑖 ∈ (0..^(♯‘𝑇))) → ((𝑇 ++ ⟨“𝑆”⟩)‘𝑖) = (𝑇‘𝑖))
33	23, 31, 32	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑇 ++ ⟨“𝑆”⟩)‘𝑖) = (𝑇‘𝑖))
34		fzonn0p1p1 13889	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑖 ∈ (0..^𝑁) → (𝑖 + 1) ∈ (0..^(𝑁 + 1)))
35	34	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑖 + 1) ∈ (0..^(𝑁 + 1)))
36	27	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1)) → (0..^(♯‘𝑇)) = (0..^(𝑁 + 1)))
37	36	ad2antlr 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) ∧ 𝑖 ∈ (0..^𝑁)) → (0..^(♯‘𝑇)) = (0..^(𝑁 + 1)))
38	35, 37	eleqtrrd 2866	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑖 + 1) ∈ (0..^(♯‘𝑇)))
39		ccats1val1 14785	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑇 ∈ Word 𝑉 ∧ (𝑖 + 1) ∈ (0..^(♯‘𝑇))) → ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1)) = (𝑇‘(𝑖 + 1)))
40	23, 38, 39	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1)) = (𝑇‘(𝑖 + 1)))
41	33, 40	preq12d 4701	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) ∧ 𝑖 ∈ (0..^𝑁)) → {((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} = {(𝑇‘𝑖), (𝑇‘(𝑖 + 1))})
42	41	exp31 425	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉) → ((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1)) → (𝑖 ∈ (0..^𝑁) → {((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} = {(𝑇‘𝑖), (𝑇‘(𝑖 + 1))})))
43	42	adantrr 730	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸)) → ((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1)) → (𝑖 ∈ (0..^𝑁) → {((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} = {(𝑇‘𝑖), (𝑇‘(𝑖 + 1))})))
44	43	impcom 413	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1)) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → (𝑖 ∈ (0..^𝑁) → {((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} = {(𝑇‘𝑖), (𝑇‘(𝑖 + 1))}))
45	44	imp 412	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1)) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) ∧ 𝑖 ∈ (0..^𝑁)) → {((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} = {(𝑇‘𝑖), (𝑇‘(𝑖 + 1))})
46	45	eleq1d 2848	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1)) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) ∧ 𝑖 ∈ (0..^𝑁)) → ({((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ {(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸))
47	46	ralbidva 3186	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1)) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → (∀𝑖 ∈ (0..^𝑁){((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸))
48	47	exbiri 823	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1)) → ((𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸)) → (∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸 → ∀𝑖 ∈ (0..^𝑁){((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} ∈ 𝐸)))
49	48	com23 87	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1)) → (∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸 → ((𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸)) → ∀𝑖 ∈ (0..^𝑁){((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} ∈ 𝐸)))
50	49	3impia 1135	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) → ((𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸)) → ∀𝑖 ∈ (0..^𝑁){((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} ∈ 𝐸))
51	50	imp 412	. . . . . . . . . . . . . . . 16 ⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → ∀𝑖 ∈ (0..^𝑁){((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} ∈ 𝐸)
52		oveq1 7434	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((♯‘𝑇) = (𝑁 + 1) → ((♯‘𝑇) − 1) = ((𝑁 + 1) − 1))
53	52	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1)) → ((♯‘𝑇) − 1) = ((𝑁 + 1) − 1))
54		nn0cn 12626	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ)
55		1cnd 11312	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑁 ∈ ℕ0 → 1 ∈ ℂ)
56	54, 55	pncand 11680	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑁 ∈ ℕ0 → ((𝑁 + 1) − 1) = 𝑁)
57	56	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → ((𝑁 + 1) − 1) = 𝑁)
58	53, 57	sylan9eqr 2820	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) → ((♯‘𝑇) − 1) = 𝑁)
59	58	fveq2d 6897	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) → (𝑇‘((♯‘𝑇) − 1)) = (𝑇‘𝑁))
60		lsw 14719	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑇 ∈ Word 𝑉 → (lastS‘𝑇) = (𝑇‘((♯‘𝑇) − 1)))
61	60	ad2antrl 741	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) → (lastS‘𝑇) = (𝑇‘((♯‘𝑇) − 1)))
62		simprl 783	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) → 𝑇 ∈ Word 𝑉)
63		fzonn0p1 13887	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ (0..^(𝑁 + 1)))
64	63	ad2antlr 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) → 𝑁 ∈ (0..^(𝑁 + 1)))
65	27	eleq2d 2849	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((♯‘𝑇) = (𝑁 + 1) → (𝑁 ∈ (0..^(♯‘𝑇)) ↔ 𝑁 ∈ (0..^(𝑁 + 1))))
66	65	ad2antll 742	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) → (𝑁 ∈ (0..^(♯‘𝑇)) ↔ 𝑁 ∈ (0..^(𝑁 + 1))))
67	64, 66	mpbird 260	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) → 𝑁 ∈ (0..^(♯‘𝑇)))
68		ccats1val1 14785	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑇 ∈ Word 𝑉 ∧ 𝑁 ∈ (0..^(♯‘𝑇))) → ((𝑇 ++ ⟨“𝑆”⟩)‘𝑁) = (𝑇‘𝑁))
69	62, 67, 68	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) → ((𝑇 ++ ⟨“𝑆”⟩)‘𝑁) = (𝑇‘𝑁))
70	59, 61, 69	3eqtr4d 2808	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) → (lastS‘𝑇) = ((𝑇 ++ ⟨“𝑆”⟩)‘𝑁))
71		simpll 779	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) → 𝑆 ∈ 𝑉)
72		simprr 785	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) → (♯‘𝑇) = (𝑁 + 1))
73	72	eqcomd 2769	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) → (𝑁 + 1) = (♯‘𝑇))
74		ccats1val2 14786	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑇 ∈ Word 𝑉 ∧ 𝑆 ∈ 𝑉 ∧ (𝑁 + 1) = (♯‘𝑇)) → ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑁 + 1)) = 𝑆)
75	74	eqcomd 2769	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑇 ∈ Word 𝑉 ∧ 𝑆 ∈ 𝑉 ∧ (𝑁 + 1) = (♯‘𝑇)) → 𝑆 = ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑁 + 1)))
76	62, 71, 73, 75	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) → 𝑆 = ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑁 + 1)))
77	70, 76	preq12d 4701	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) → {(lastS‘𝑇), 𝑆} = {((𝑇 ++ ⟨“𝑆”⟩)‘𝑁), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑁 + 1))})
78	77	eleq1d 2848	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) → ({(lastS‘𝑇), 𝑆} ∈ 𝐸 ↔ {((𝑇 ++ ⟨“𝑆”⟩)‘𝑁), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑁 + 1))} ∈ 𝐸))
79	78	biimpcd 252	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ({(lastS‘𝑇), 𝑆} ∈ 𝐸 → (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) → {((𝑇 ++ ⟨“𝑆”⟩)‘𝑁), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑁 + 1))} ∈ 𝐸))
80	79	exp4c 438	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({(lastS‘𝑇), 𝑆} ∈ 𝐸 → (𝑆 ∈ 𝑉 → (𝑁 ∈ ℕ0 → ((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1)) → {((𝑇 ++ ⟨“𝑆”⟩)‘𝑁), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑁 + 1))} ∈ 𝐸))))
81	80	impcom 413	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸) → (𝑁 ∈ ℕ0 → ((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1)) → {((𝑇 ++ ⟨“𝑆”⟩)‘𝑁), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑁 + 1))} ∈ 𝐸)))
82	81	impcom 413	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸)) → ((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1)) → {((𝑇 ++ ⟨“𝑆”⟩)‘𝑁), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑁 + 1))} ∈ 𝐸))
83	82	impcom 413	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1)) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → {((𝑇 ++ ⟨“𝑆”⟩)‘𝑁), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑁 + 1))} ∈ 𝐸)
84	83	3adantl3 1187	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → {((𝑇 ++ ⟨“𝑆”⟩)‘𝑁), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑁 + 1))} ∈ 𝐸)
85		fveq2 6893	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 𝑁 → ((𝑇 ++ ⟨“𝑆”⟩)‘𝑖) = ((𝑇 ++ ⟨“𝑆”⟩)‘𝑁))
86		fvoveq1 7450	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 𝑁 → ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1)) = ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑁 + 1)))
87	85, 86	preq12d 4701	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 𝑁 → {((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} = {((𝑇 ++ ⟨“𝑆”⟩)‘𝑁), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑁 + 1))})
88	87	eleq1d 2848	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = 𝑁 → ({((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ {((𝑇 ++ ⟨“𝑆”⟩)‘𝑁), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑁 + 1))} ∈ 𝐸))
89	88	ralsng 4635	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ ℕ0 → (∀𝑖 ∈ {𝑁} {((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ {((𝑇 ++ ⟨“𝑆”⟩)‘𝑁), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑁 + 1))} ∈ 𝐸))
90	89	ad2antrl 741	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → (∀𝑖 ∈ {𝑁} {((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ {((𝑇 ++ ⟨“𝑆”⟩)‘𝑁), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑁 + 1))} ∈ 𝐸))
91	84, 90	mpbird 260	. . . . . . . . . . . . . . . 16 ⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → ∀𝑖 ∈ {𝑁} {((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} ∈ 𝐸)
92		ralunb 4197	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑖 ∈ ((0..^𝑁) ∪ {𝑁}){((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ (∀𝑖 ∈ (0..^𝑁){((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} ∈ 𝐸 ∧ ∀𝑖 ∈ {𝑁} {((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} ∈ 𝐸))
93	51, 91, 92	sylanbrc 595	. . . . . . . . . . . . . . 15 ⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → ∀𝑖 ∈ ((0..^𝑁) ∪ {𝑁}){((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} ∈ 𝐸)
94		elnn0uz 13016	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ ℕ0 ↔ 𝑁 ∈ (ℤ≥‘0))
95		eluzfz2 13675	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ (ℤ≥‘0) → 𝑁 ∈ (0...𝑁))
96	94, 95	sylbi 220	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ (0...𝑁))
97		fzelp1 13720	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ (0...𝑁) → 𝑁 ∈ (0...(𝑁 + 1)))
98		fzosplit 13837	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ (0...(𝑁 + 1)) → (0..^(𝑁 + 1)) = ((0..^𝑁) ∪ (𝑁..^(𝑁 + 1))))
99	96, 97, 98	3syl 19	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℕ0 → (0..^(𝑁 + 1)) = ((0..^𝑁) ∪ (𝑁..^(𝑁 + 1))))
100		nn0z 12727	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ)
101		fzosn 13881	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ ℤ → (𝑁..^(𝑁 + 1)) = {𝑁})
102	100, 101	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ ℕ0 → (𝑁..^(𝑁 + 1)) = {𝑁})
103	102	uneq2d 4169	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℕ0 → ((0..^𝑁) ∪ (𝑁..^(𝑁 + 1))) = ((0..^𝑁) ∪ {𝑁}))
104	99, 103	eqtrd 2798	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ0 → (0..^(𝑁 + 1)) = ((0..^𝑁) ∪ {𝑁}))
105	104	ad2antrl 741	. . . . . . . . . . . . . . 15 ⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → (0..^(𝑁 + 1)) = ((0..^𝑁) ∪ {𝑁}))
106	93, 105	raleqtrrdv 3326	. . . . . . . . . . . . . 14 ⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → ∀𝑖 ∈ (0..^(𝑁 + 1)){((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} ∈ 𝐸)
107		ccatlen 14730	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑇 ∈ Word 𝑉 ∧ ⟨“𝑆”⟩ ∈ Word 𝑉) → (♯‘(𝑇 ++ ⟨“𝑆”⟩)) = ((♯‘𝑇) + (♯‘⟨“𝑆”⟩)))
108	5, 20, 107	syl2an 608	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → (♯‘(𝑇 ++ ⟨“𝑆”⟩)) = ((♯‘𝑇) + (♯‘⟨“𝑆”⟩)))
109	108	oveq1d 7442	. . . . . . . . . . . . . . . 16 ⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → ((♯‘(𝑇 ++ ⟨“𝑆”⟩)) − 1) = (((♯‘𝑇) + (♯‘⟨“𝑆”⟩)) − 1))
110		simpl2 1211	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → (♯‘𝑇) = (𝑁 + 1))
111		s1len 14763	. . . . . . . . . . . . . . . . . . 19 ⊢ (♯‘⟨“𝑆”⟩) = 1
112	111	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → (♯‘⟨“𝑆”⟩) = 1)
113	110, 112	oveq12d 7445	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → ((♯‘𝑇) + (♯‘⟨“𝑆”⟩)) = ((𝑁 + 1) + 1))
114	113	oveq1d 7442	. . . . . . . . . . . . . . . 16 ⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → (((♯‘𝑇) + (♯‘⟨“𝑆”⟩)) − 1) = (((𝑁 + 1) + 1) − 1))
115		peano2nn0 12656	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℕ0)
116	115	nn0cnd 12679	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℂ)
117	116, 55	pncand 11680	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℕ0 → (((𝑁 + 1) + 1) − 1) = (𝑁 + 1))
118	117	ad2antrl 741	. . . . . . . . . . . . . . . 16 ⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → (((𝑁 + 1) + 1) − 1) = (𝑁 + 1))
119	109, 114, 118	3eqtrd 2802	. . . . . . . . . . . . . . 15 ⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → ((♯‘(𝑇 ++ ⟨“𝑆”⟩)) − 1) = (𝑁 + 1))
120	119	oveq2d 7443	. . . . . . . . . . . . . 14 ⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → (0..^((♯‘(𝑇 ++ ⟨“𝑆”⟩)) − 1)) = (0..^(𝑁 + 1)))
121	106, 120	raleqtrrdv 3326	. . . . . . . . . . . . 13 ⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → ∀𝑖 ∈ (0..^((♯‘(𝑇 ++ ⟨“𝑆”⟩)) − 1)){((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} ∈ 𝐸)
122	18, 22, 121	3jca 1146	. . . . . . . . . . . 12 ⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → ((𝑇 ++ ⟨“𝑆”⟩) ≠ ∅ ∧ (𝑇 ++ ⟨“𝑆”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑇 ++ ⟨“𝑆”⟩)) − 1)){((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} ∈ 𝐸))
123	108, 113	eqtrd 2798	. . . . . . . . . . . 12 ⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → (♯‘(𝑇 ++ ⟨“𝑆”⟩)) = ((𝑁 + 1) + 1))
124	122, 123	jca 521	. . . . . . . . . . 11 ⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → (((𝑇 ++ ⟨“𝑆”⟩) ≠ ∅ ∧ (𝑇 ++ ⟨“𝑆”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑇 ++ ⟨“𝑆”⟩)) − 1)){((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} ∈ 𝐸) ∧ (♯‘(𝑇 ++ ⟨“𝑆”⟩)) = ((𝑁 + 1) + 1)))
125	124	ex 418	. . . . . . . . . 10 ⊢ ((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) → ((𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸)) → (((𝑇 ++ ⟨“𝑆”⟩) ≠ ∅ ∧ (𝑇 ++ ⟨“𝑆”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑇 ++ ⟨“𝑆”⟩)) − 1)){((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} ∈ 𝐸) ∧ (♯‘(𝑇 ++ ⟨“𝑆”⟩)) = ((𝑁 + 1) + 1))))
126	4, 125	syl 18	. . . . . . . . 9 ⊢ (𝑇 ∈ (𝑁 WWalksN 𝐺) → ((𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸)) → (((𝑇 ++ ⟨“𝑆”⟩) ≠ ∅ ∧ (𝑇 ++ ⟨“𝑆”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑇 ++ ⟨“𝑆”⟩)) − 1)){((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} ∈ 𝐸) ∧ (♯‘(𝑇 ++ ⟨“𝑆”⟩)) = ((𝑁 + 1) + 1))))
127	126	expd 421	. . . . . . . 8 ⊢ (𝑇 ∈ (𝑁 WWalksN 𝐺) → (𝑁 ∈ ℕ0 → ((𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸) → (((𝑇 ++ ⟨“𝑆”⟩) ≠ ∅ ∧ (𝑇 ++ ⟨“𝑆”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑇 ++ ⟨“𝑆”⟩)) − 1)){((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} ∈ 𝐸) ∧ (♯‘(𝑇 ++ ⟨“𝑆”⟩)) = ((𝑁 + 1) + 1)))))
128	127	impcom 413	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑇 ∈ (𝑁 WWalksN 𝐺)) → ((𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸) → (((𝑇 ++ ⟨“𝑆”⟩) ≠ ∅ ∧ (𝑇 ++ ⟨“𝑆”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑇 ++ ⟨“𝑆”⟩)) − 1)){((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} ∈ 𝐸) ∧ (♯‘(𝑇 ++ ⟨“𝑆”⟩)) = ((𝑁 + 1) + 1))))
129	128	adantll 727	. . . . . 6 ⊢ (((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0) ∧ 𝑇 ∈ (𝑁 WWalksN 𝐺)) → ((𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸) → (((𝑇 ++ ⟨“𝑆”⟩) ≠ ∅ ∧ (𝑇 ++ ⟨“𝑆”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑇 ++ ⟨“𝑆”⟩)) − 1)){((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} ∈ 𝐸) ∧ (♯‘(𝑇 ++ ⟨“𝑆”⟩)) = ((𝑁 + 1) + 1))))
130		iswwlksn 30439	. . . . . . . . . 10 ⊢ ((𝑁 + 1) ∈ ℕ0 → ((𝑇 ++ ⟨“𝑆”⟩) ∈ ((𝑁 + 1) WWalksN 𝐺) ↔ ((𝑇 ++ ⟨“𝑆”⟩) ∈ (WWalks‘𝐺) ∧ (♯‘(𝑇 ++ ⟨“𝑆”⟩)) = ((𝑁 + 1) + 1))))
131	115, 130	syl 18	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → ((𝑇 ++ ⟨“𝑆”⟩) ∈ ((𝑁 + 1) WWalksN 𝐺) ↔ ((𝑇 ++ ⟨“𝑆”⟩) ∈ (WWalks‘𝐺) ∧ (♯‘(𝑇 ++ ⟨“𝑆”⟩)) = ((𝑁 + 1) + 1))))
132	131	adantl 487	. . . . . . . 8 ⊢ ((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0) → ((𝑇 ++ ⟨“𝑆”⟩) ∈ ((𝑁 + 1) WWalksN 𝐺) ↔ ((𝑇 ++ ⟨“𝑆”⟩) ∈ (WWalks‘𝐺) ∧ (♯‘(𝑇 ++ ⟨“𝑆”⟩)) = ((𝑁 + 1) + 1))))
133	1, 3	iswwlks 30437	. . . . . . . . 9 ⊢ ((𝑇 ++ ⟨“𝑆”⟩) ∈ (WWalks‘𝐺) ↔ ((𝑇 ++ ⟨“𝑆”⟩) ≠ ∅ ∧ (𝑇 ++ ⟨“𝑆”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑇 ++ ⟨“𝑆”⟩)) − 1)){((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} ∈ 𝐸))
134	133	anbi1i 636	. . . . . . . 8 ⊢ (((𝑇 ++ ⟨“𝑆”⟩) ∈ (WWalks‘𝐺) ∧ (♯‘(𝑇 ++ ⟨“𝑆”⟩)) = ((𝑁 + 1) + 1)) ↔ (((𝑇 ++ ⟨“𝑆”⟩) ≠ ∅ ∧ (𝑇 ++ ⟨“𝑆”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑇 ++ ⟨“𝑆”⟩)) − 1)){((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} ∈ 𝐸) ∧ (♯‘(𝑇 ++ ⟨“𝑆”⟩)) = ((𝑁 + 1) + 1)))
135	132, 134	bitrdi 290	. . . . . . 7 ⊢ ((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0) → ((𝑇 ++ ⟨“𝑆”⟩) ∈ ((𝑁 + 1) WWalksN 𝐺) ↔ (((𝑇 ++ ⟨“𝑆”⟩) ≠ ∅ ∧ (𝑇 ++ ⟨“𝑆”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑇 ++ ⟨“𝑆”⟩)) − 1)){((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} ∈ 𝐸) ∧ (♯‘(𝑇 ++ ⟨“𝑆”⟩)) = ((𝑁 + 1) + 1))))
136	135	adantr 486	. . . . . 6 ⊢ (((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0) ∧ 𝑇 ∈ (𝑁 WWalksN 𝐺)) → ((𝑇 ++ ⟨“𝑆”⟩) ∈ ((𝑁 + 1) WWalksN 𝐺) ↔ (((𝑇 ++ ⟨“𝑆”⟩) ≠ ∅ ∧ (𝑇 ++ ⟨“𝑆”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑇 ++ ⟨“𝑆”⟩)) − 1)){((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} ∈ 𝐸) ∧ (♯‘(𝑇 ++ ⟨“𝑆”⟩)) = ((𝑁 + 1) + 1))))
137	129, 136	sylibrd 262	. . . . 5 ⊢ (((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0) ∧ 𝑇 ∈ (𝑁 WWalksN 𝐺)) → ((𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸) → (𝑇 ++ ⟨“𝑆”⟩) ∈ ((𝑁 + 1) WWalksN 𝐺)))
138	137	ex 418	. . . 4 ⊢ ((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0) → (𝑇 ∈ (𝑁 WWalksN 𝐺) → ((𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸) → (𝑇 ++ ⟨“𝑆”⟩) ∈ ((𝑁 + 1) WWalksN 𝐺))))
139	138	3adant3 1150	. . 3 ⊢ ((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0 ∧ 𝑇 ∈ Word 𝑉) → (𝑇 ∈ (𝑁 WWalksN 𝐺) → ((𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸) → (𝑇 ++ ⟨“𝑆”⟩) ∈ ((𝑁 + 1) WWalksN 𝐺))))
140	2, 139	mpcom 39	. 2 ⊢ (𝑇 ∈ (𝑁 WWalksN 𝐺) → ((𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸) → (𝑇 ++ ⟨“𝑆”⟩) ∈ ((𝑁 + 1) WWalksN 𝐺)))
141	140	3impib 1134	1 ⊢ ((𝑇 ∈ (𝑁 WWalksN 𝐺) ∧ 𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸) → (𝑇 ++ ⟨“𝑆”⟩) ∈ ((𝑁 + 1) WWalksN 𝐺))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1569   ∈ wcel 2146   ≠ wne 2958  ∀wral 3079  Vcvv 3453   ⊆ wss 3899   ∪ cun 4151  ∅c0 4280  {csn 4587  {cpr 4589  ⟨cop 4837  ‘cfv 6546  (class class class)co 7427  0cc0 11210  1c1 11211   + caddc 11213   − cmin 11551  ℕ₀cn0 12616  ℤcz 12703  ℤ_≥cuz 12975  ...cfz 13649  ..^cfzo 13798  ♯chash 14484  Word cword 14668  lastSclsw 14717   ++ cconcat 14725  ⟨“cs1 14752  Vtxcvtx 29586  Edgcedg 29637  WWalkscwwlks 30426   WWalksN cwwlksn 30427

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735  ax-rep 5234  ax-sep 5251  ax-nul 5262  ax-pow 5330  ax-pr 5394  ax-un 7758  ax-cnex 11266  ax-resscn 11267  ax-1cn 11268  ax-icn 11269  ax-addcl 11270  ax-addrcl 11271  ax-mulcl 11272  ax-mulrcl 11273  ax-mulcom 11274  ax-addass 11275  ax-mulass 11276  ax-distr 11277  ax-i2m1 11278  ax-1ne0 11279  ax-1rid 11280  ax-rnegex 11281  ax-rrecex 11282  ax-cnre 11283  ax-pre-lttri 11284  ax-pre-lttrn 11285  ax-pre-ltadd 11286  ax-pre-mulgt0 11287

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-reu 3369  df-rab 3416  df-v 3455  df-sbc 3742  df-csb 3851  df-ss 3900  df-pss 4016  df-dif 4049  df-in 4093  df-un 4153  df-nul 4281  df-if 4485  df-pw 4561  df-sn 4588  df-pr 4590  df-op 4838  df-uni 4870  df-int 4910  df-iun 4955  df-br 5106  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5549  df-eprel 5554  df-po 5562  df-so 5563  df-fr 5607  df-we 5609  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6310  df-ord 6371  df-on 6372  df-lim 6373  df-suc 6374  df-iota 6500  df-fun 6548  df-fn 6549  df-f 6550  df-f1 6551  df-fo 6552  df-f1o 6553  df-fv 6554  df-riota 7384  df-ov 7430  df-oprab 7431  df-mpo 7432  df-om 7885  df-1st 8008  df-2nd 8009  df-frecs 8310  df-wrecs 8341  df-recs 8390  df-rdg 8429  df-1o 8487  df-er 8728  df-map 8860  df-en 8985  df-dom 8986  df-sdom 8987  df-fin 8988  df-card 10030  df-pnf 11355  df-mnf 11356  df-xr 11357  df-ltxr 11358  df-le 11359  df-sub 11553  df-neg 11554  df-nn 12346  df-n0 12617  df-z 12704  df-uz 12976  df-fz 13650  df-fzo 13799  df-hash 14485  df-word 14669  df-lsw 14718  df-concat 14726  df-s1 14753  df-wwlks 30431  df-wwlksn 30432

This theorem is used by:  wwlksnextbi  30495  wwlksnextsurj  30501