Theorem wwlksnext 29978

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 29927	. . 3 ⊢ (𝑇 ∈ (𝑁 WWalksN 𝐺) → (𝐺 ∈ V ∧ 𝑁 ∈ ℕ0 ∧ 𝑇 ∈ Word 𝑉))
3		wwlksnext.e	. . . . . . . . . . 11 ⊢ 𝐸 = (Edg‘𝐺)
4	1, 3	wwlknp 29928	. . . . . . . . . 10 ⊢ (𝑇 ∈ (𝑁 WWalksN 𝐺) → (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸))
5		simp1 1137	. . . . . . . . . . . . . . 15 ⊢ ((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) → 𝑇 ∈ Word 𝑉)
6		simprl 771	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸)) → 𝑆 ∈ 𝑉)
7		cats1un 14656	. . . . . . . . . . . . . . 15 ⊢ ((𝑇 ∈ Word 𝑉 ∧ 𝑆 ∈ 𝑉) → (𝑇 ++ ⟨“𝑆”⟩) = (𝑇 ∪ {⟨(♯‘𝑇), 𝑆⟩}))
8	5, 6, 7	syl2an 597	. . . . . . . . . . . . . 14 ⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → (𝑇 ++ ⟨“𝑆”⟩) = (𝑇 ∪ {⟨(♯‘𝑇), 𝑆⟩}))
9		opex 5419	. . . . . . . . . . . . . . . . . . 19 ⊢ ⟨(♯‘𝑇), 𝑆⟩ ∈ V
10	9	snnz 4735	. . . . . . . . . . . . . . . . . 18 ⊢ {⟨(♯‘𝑇), 𝑆⟩} ≠ ∅
11	10	neii 2935	. . . . . . . . . . . . . . . . 17 ⊢ ¬ {⟨(♯‘𝑇), 𝑆⟩} = ∅
12	11	intnan 486	. . . . . . . . . . . . . . . 16 ⊢ ¬ (𝑇 = ∅ ∧ {⟨(♯‘𝑇), 𝑆⟩} = ∅)
13		df-ne 2934	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑇 ∪ {⟨(♯‘𝑇), 𝑆⟩}) ≠ ∅ ↔ ¬ (𝑇 ∪ {⟨(♯‘𝑇), 𝑆⟩}) = ∅)
14		un00 4399	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑇 = ∅ ∧ {⟨(♯‘𝑇), 𝑆⟩} = ∅) ↔ (𝑇 ∪ {⟨(♯‘𝑇), 𝑆⟩}) = ∅)
15	13, 14	xchbinxr 335	. . . . . . . . . . . . . . . 16 ⊢ ((𝑇 ∪ {⟨(♯‘𝑇), 𝑆⟩}) ≠ ∅ ↔ ¬ (𝑇 = ∅ ∧ {⟨(♯‘𝑇), 𝑆⟩} = ∅))
16	12, 15	mpbir 231	. . . . . . . . . . . . . . 15 ⊢ (𝑇 ∪ {⟨(♯‘𝑇), 𝑆⟩}) ≠ ∅
17	16	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → (𝑇 ∪ {⟨(♯‘𝑇), 𝑆⟩}) ≠ ∅)
18	8, 17	eqnetrd 3000	. . . . . . . . . . . . 13 ⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → (𝑇 ++ ⟨“𝑆”⟩) ≠ ∅)
19		s1cl 14538	. . . . . . . . . . . . . . 15 ⊢ (𝑆 ∈ 𝑉 → ⟨“𝑆”⟩ ∈ Word 𝑉)
20	19	ad2antrl 729	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸)) → ⟨“𝑆”⟩ ∈ Word 𝑉)
21		ccatcl 14509	. . . . . . . . . . . . . 14 ⊢ ((𝑇 ∈ Word 𝑉 ∧ ⟨“𝑆”⟩ ∈ Word 𝑉) → (𝑇 ++ ⟨“𝑆”⟩) ∈ Word 𝑉)
22	5, 20, 21	syl2an 597	. . . . . . . . . . . . 13 ⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → (𝑇 ++ ⟨“𝑆”⟩) ∈ Word 𝑉)
23		simplrl 777	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑇 ∈ Word 𝑉)
24		fzossfzop1 13671	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑁 ∈ ℕ0 → (0..^𝑁) ⊆ (0..^(𝑁 + 1)))
25	24	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) → (0..^𝑁) ⊆ (0..^(𝑁 + 1)))
26	25	sselda 3935	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑖 ∈ (0..^(𝑁 + 1)))
27		oveq2 7376	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((♯‘𝑇) = (𝑁 + 1) → (0..^(♯‘𝑇)) = (0..^(𝑁 + 1)))
28	27	eleq2d 2823	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((♯‘𝑇) = (𝑁 + 1) → (𝑖 ∈ (0..^(♯‘𝑇)) ↔ 𝑖 ∈ (0..^(𝑁 + 1))))
29	28	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1)) → (𝑖 ∈ (0..^(♯‘𝑇)) ↔ 𝑖 ∈ (0..^(𝑁 + 1))))
30	29	ad2antlr 728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑖 ∈ (0..^(♯‘𝑇)) ↔ 𝑖 ∈ (0..^(𝑁 + 1))))
31	26, 30	mpbird 257	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) ∧ 𝑖 ∈ (0..^𝑁)) → 𝑖 ∈ (0..^(♯‘𝑇)))
32		ccats1val1 14562	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑇 ∈ Word 𝑉 ∧ 𝑖 ∈ (0..^(♯‘𝑇))) → ((𝑇 ++ ⟨“𝑆”⟩)‘𝑖) = (𝑇‘𝑖))
33	23, 31, 32	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑇 ++ ⟨“𝑆”⟩)‘𝑖) = (𝑇‘𝑖))
34		fzonn0p1p1 13672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑖 ∈ (0..^𝑁) → (𝑖 + 1) ∈ (0..^(𝑁 + 1)))
35	34	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑖 + 1) ∈ (0..^(𝑁 + 1)))
36	27	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1)) → (0..^(♯‘𝑇)) = (0..^(𝑁 + 1)))
37	36	ad2antlr 728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) ∧ 𝑖 ∈ (0..^𝑁)) → (0..^(♯‘𝑇)) = (0..^(𝑁 + 1)))
38	35, 37	eleqtrrd 2840	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) ∧ 𝑖 ∈ (0..^𝑁)) → (𝑖 + 1) ∈ (0..^(♯‘𝑇)))
39		ccats1val1 14562	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑇 ∈ Word 𝑉 ∧ (𝑖 + 1) ∈ (0..^(♯‘𝑇))) → ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1)) = (𝑇‘(𝑖 + 1)))
40	23, 38, 39	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) ∧ 𝑖 ∈ (0..^𝑁)) → ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1)) = (𝑇‘(𝑖 + 1)))
41	33, 40	preq12d 4700	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) ∧ 𝑖 ∈ (0..^𝑁)) → {((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} = {(𝑇‘𝑖), (𝑇‘(𝑖 + 1))})
42	41	exp31 419	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉) → ((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1)) → (𝑖 ∈ (0..^𝑁) → {((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} = {(𝑇‘𝑖), (𝑇‘(𝑖 + 1))})))
43	42	adantrr 718	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸)) → ((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1)) → (𝑖 ∈ (0..^𝑁) → {((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} = {(𝑇‘𝑖), (𝑇‘(𝑖 + 1))})))
44	43	impcom 407	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1)) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → (𝑖 ∈ (0..^𝑁) → {((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} = {(𝑇‘𝑖), (𝑇‘(𝑖 + 1))}))
45	44	imp 406	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1)) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) ∧ 𝑖 ∈ (0..^𝑁)) → {((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} = {(𝑇‘𝑖), (𝑇‘(𝑖 + 1))})
46	45	eleq1d 2822	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1)) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) ∧ 𝑖 ∈ (0..^𝑁)) → ({((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ {(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸))
47	46	ralbidva 3159	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1)) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → (∀𝑖 ∈ (0..^𝑁){((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸))
48	47	exbiri 811	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1)) → ((𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸)) → (∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸 → ∀𝑖 ∈ (0..^𝑁){((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} ∈ 𝐸)))
49	48	com23 86	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1)) → (∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸 → ((𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸)) → ∀𝑖 ∈ (0..^𝑁){((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} ∈ 𝐸)))
50	49	3impia 1118	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) → ((𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸)) → ∀𝑖 ∈ (0..^𝑁){((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} ∈ 𝐸))
51	50	imp 406	. . . . . . . . . . . . . . . 16 ⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → ∀𝑖 ∈ (0..^𝑁){((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} ∈ 𝐸)
52		oveq1 7375	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((♯‘𝑇) = (𝑁 + 1) → ((♯‘𝑇) − 1) = ((𝑁 + 1) − 1))
53	52	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1)) → ((♯‘𝑇) − 1) = ((𝑁 + 1) − 1))
54		nn0cn 12423	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ)
55		1cnd 11139	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑁 ∈ ℕ0 → 1 ∈ ℂ)
56	54, 55	pncand 11505	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑁 ∈ ℕ0 → ((𝑁 + 1) − 1) = 𝑁)
57	56	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → ((𝑁 + 1) − 1) = 𝑁)
58	53, 57	sylan9eqr 2794	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) → ((♯‘𝑇) − 1) = 𝑁)
59	58	fveq2d 6846	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) → (𝑇‘((♯‘𝑇) − 1)) = (𝑇‘𝑁))
60		lsw 14499	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑇 ∈ Word 𝑉 → (lastS‘𝑇) = (𝑇‘((♯‘𝑇) − 1)))
61	60	ad2antrl 729	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) → (lastS‘𝑇) = (𝑇‘((♯‘𝑇) − 1)))
62		simprl 771	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) → 𝑇 ∈ Word 𝑉)
63		fzonn0p1 13670	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ (0..^(𝑁 + 1)))
64	63	ad2antlr 728	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) → 𝑁 ∈ (0..^(𝑁 + 1)))
65	27	eleq2d 2823	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((♯‘𝑇) = (𝑁 + 1) → (𝑁 ∈ (0..^(♯‘𝑇)) ↔ 𝑁 ∈ (0..^(𝑁 + 1))))
66	65	ad2antll 730	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) → (𝑁 ∈ (0..^(♯‘𝑇)) ↔ 𝑁 ∈ (0..^(𝑁 + 1))))
67	64, 66	mpbird 257	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) → 𝑁 ∈ (0..^(♯‘𝑇)))
68		ccats1val1 14562	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑇 ∈ Word 𝑉 ∧ 𝑁 ∈ (0..^(♯‘𝑇))) → ((𝑇 ++ ⟨“𝑆”⟩)‘𝑁) = (𝑇‘𝑁))
69	62, 67, 68	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) → ((𝑇 ++ ⟨“𝑆”⟩)‘𝑁) = (𝑇‘𝑁))
70	59, 61, 69	3eqtr4d 2782	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) → (lastS‘𝑇) = ((𝑇 ++ ⟨“𝑆”⟩)‘𝑁))
71		simpll 767	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) → 𝑆 ∈ 𝑉)
72		simprr 773	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) → (♯‘𝑇) = (𝑁 + 1))
73	72	eqcomd 2743	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) → (𝑁 + 1) = (♯‘𝑇))
74		ccats1val2 14563	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑇 ∈ Word 𝑉 ∧ 𝑆 ∈ 𝑉 ∧ (𝑁 + 1) = (♯‘𝑇)) → ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑁 + 1)) = 𝑆)
75	74	eqcomd 2743	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑇 ∈ Word 𝑉 ∧ 𝑆 ∈ 𝑉 ∧ (𝑁 + 1) = (♯‘𝑇)) → 𝑆 = ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑁 + 1)))
76	62, 71, 73, 75	syl3anc 1374	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) → 𝑆 = ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑁 + 1)))
77	70, 76	preq12d 4700	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) → {(lastS‘𝑇), 𝑆} = {((𝑇 ++ ⟨“𝑆”⟩)‘𝑁), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑁 + 1))})
78	77	eleq1d 2822	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) → ({(lastS‘𝑇), 𝑆} ∈ 𝐸 ↔ {((𝑇 ++ ⟨“𝑆”⟩)‘𝑁), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑁 + 1))} ∈ 𝐸))
79	78	biimpcd 249	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ({(lastS‘𝑇), 𝑆} ∈ 𝐸 → (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ (𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1))) → {((𝑇 ++ ⟨“𝑆”⟩)‘𝑁), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑁 + 1))} ∈ 𝐸))
80	79	exp4c 432	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({(lastS‘𝑇), 𝑆} ∈ 𝐸 → (𝑆 ∈ 𝑉 → (𝑁 ∈ ℕ0 → ((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1)) → {((𝑇 ++ ⟨“𝑆”⟩)‘𝑁), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑁 + 1))} ∈ 𝐸))))
81	80	impcom 407	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸) → (𝑁 ∈ ℕ0 → ((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1)) → {((𝑇 ++ ⟨“𝑆”⟩)‘𝑁), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑁 + 1))} ∈ 𝐸)))
82	81	impcom 407	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸)) → ((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1)) → {((𝑇 ++ ⟨“𝑆”⟩)‘𝑁), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑁 + 1))} ∈ 𝐸))
83	82	impcom 407	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1)) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → {((𝑇 ++ ⟨“𝑆”⟩)‘𝑁), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑁 + 1))} ∈ 𝐸)
84	83	3adantl3 1170	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → {((𝑇 ++ ⟨“𝑆”⟩)‘𝑁), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑁 + 1))} ∈ 𝐸)
85		fveq2 6842	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 𝑁 → ((𝑇 ++ ⟨“𝑆”⟩)‘𝑖) = ((𝑇 ++ ⟨“𝑆”⟩)‘𝑁))
86		fvoveq1 7391	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 𝑁 → ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1)) = ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑁 + 1)))
87	85, 86	preq12d 4700	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 𝑁 → {((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} = {((𝑇 ++ ⟨“𝑆”⟩)‘𝑁), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑁 + 1))})
88	87	eleq1d 2822	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = 𝑁 → ({((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ {((𝑇 ++ ⟨“𝑆”⟩)‘𝑁), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑁 + 1))} ∈ 𝐸))
89	88	ralsng 4634	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ ℕ0 → (∀𝑖 ∈ {𝑁} {((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ {((𝑇 ++ ⟨“𝑆”⟩)‘𝑁), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑁 + 1))} ∈ 𝐸))
90	89	ad2antrl 729	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → (∀𝑖 ∈ {𝑁} {((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ {((𝑇 ++ ⟨“𝑆”⟩)‘𝑁), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑁 + 1))} ∈ 𝐸))
91	84, 90	mpbird 257	. . . . . . . . . . . . . . . 16 ⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → ∀𝑖 ∈ {𝑁} {((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} ∈ 𝐸)
92		ralunb 4151	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑖 ∈ ((0..^𝑁) ∪ {𝑁}){((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} ∈ 𝐸 ↔ (∀𝑖 ∈ (0..^𝑁){((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} ∈ 𝐸 ∧ ∀𝑖 ∈ {𝑁} {((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} ∈ 𝐸))
93	51, 91, 92	sylanbrc 584	. . . . . . . . . . . . . . 15 ⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → ∀𝑖 ∈ ((0..^𝑁) ∪ {𝑁}){((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} ∈ 𝐸)
94		elnn0uz 12804	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ ℕ0 ↔ 𝑁 ∈ (ℤ≥‘0))
95		eluzfz2 13460	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ (ℤ≥‘0) → 𝑁 ∈ (0...𝑁))
96	94, 95	sylbi 217	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ (0...𝑁))
97		fzelp1 13504	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ (0...𝑁) → 𝑁 ∈ (0...(𝑁 + 1)))
98		fzosplit 13620	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ (0...(𝑁 + 1)) → (0..^(𝑁 + 1)) = ((0..^𝑁) ∪ (𝑁..^(𝑁 + 1))))
99	96, 97, 98	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℕ0 → (0..^(𝑁 + 1)) = ((0..^𝑁) ∪ (𝑁..^(𝑁 + 1))))
100		nn0z 12524	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ)
101		fzosn 13664	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ ℤ → (𝑁..^(𝑁 + 1)) = {𝑁})
102	100, 101	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ ℕ0 → (𝑁..^(𝑁 + 1)) = {𝑁})
103	102	uneq2d 4122	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℕ0 → ((0..^𝑁) ∪ (𝑁..^(𝑁 + 1))) = ((0..^𝑁) ∪ {𝑁}))
104	99, 103	eqtrd 2772	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ0 → (0..^(𝑁 + 1)) = ((0..^𝑁) ∪ {𝑁}))
105	104	ad2antrl 729	. . . . . . . . . . . . . . 15 ⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → (0..^(𝑁 + 1)) = ((0..^𝑁) ∪ {𝑁}))
106	93, 105	raleqtrrdv 3302	. . . . . . . . . . . . . 14 ⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → ∀𝑖 ∈ (0..^(𝑁 + 1)){((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} ∈ 𝐸)
107		ccatlen 14510	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑇 ∈ Word 𝑉 ∧ ⟨“𝑆”⟩ ∈ Word 𝑉) → (♯‘(𝑇 ++ ⟨“𝑆”⟩)) = ((♯‘𝑇) + (♯‘⟨“𝑆”⟩)))
108	5, 20, 107	syl2an 597	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → (♯‘(𝑇 ++ ⟨“𝑆”⟩)) = ((♯‘𝑇) + (♯‘⟨“𝑆”⟩)))
109	108	oveq1d 7383	. . . . . . . . . . . . . . . 16 ⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → ((♯‘(𝑇 ++ ⟨“𝑆”⟩)) − 1) = (((♯‘𝑇) + (♯‘⟨“𝑆”⟩)) − 1))
110		simpl2 1194	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → (♯‘𝑇) = (𝑁 + 1))
111		s1len 14542	. . . . . . . . . . . . . . . . . . 19 ⊢ (♯‘⟨“𝑆”⟩) = 1
112	111	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → (♯‘⟨“𝑆”⟩) = 1)
113	110, 112	oveq12d 7386	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → ((♯‘𝑇) + (♯‘⟨“𝑆”⟩)) = ((𝑁 + 1) + 1))
114	113	oveq1d 7383	. . . . . . . . . . . . . . . 16 ⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → (((♯‘𝑇) + (♯‘⟨“𝑆”⟩)) − 1) = (((𝑁 + 1) + 1) − 1))
115		peano2nn0 12453	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℕ0)
116	115	nn0cnd 12476	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℂ)
117	116, 55	pncand 11505	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℕ0 → (((𝑁 + 1) + 1) − 1) = (𝑁 + 1))
118	117	ad2antrl 729	. . . . . . . . . . . . . . . 16 ⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → (((𝑁 + 1) + 1) − 1) = (𝑁 + 1))
119	109, 114, 118	3eqtrd 2776	. . . . . . . . . . . . . . 15 ⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → ((♯‘(𝑇 ++ ⟨“𝑆”⟩)) − 1) = (𝑁 + 1))
120	119	oveq2d 7384	. . . . . . . . . . . . . 14 ⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → (0..^((♯‘(𝑇 ++ ⟨“𝑆”⟩)) − 1)) = (0..^(𝑁 + 1)))
121	106, 120	raleqtrrdv 3302	. . . . . . . . . . . . 13 ⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → ∀𝑖 ∈ (0..^((♯‘(𝑇 ++ ⟨“𝑆”⟩)) − 1)){((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} ∈ 𝐸)
122	18, 22, 121	3jca 1129	. . . . . . . . . . . 12 ⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → ((𝑇 ++ ⟨“𝑆”⟩) ≠ ∅ ∧ (𝑇 ++ ⟨“𝑆”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑇 ++ ⟨“𝑆”⟩)) − 1)){((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} ∈ 𝐸))
123	108, 113	eqtrd 2772	. . . . . . . . . . . 12 ⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → (♯‘(𝑇 ++ ⟨“𝑆”⟩)) = ((𝑁 + 1) + 1))
124	122, 123	jca 511	. . . . . . . . . . 11 ⊢ (((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) ∧ (𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸))) → (((𝑇 ++ ⟨“𝑆”⟩) ≠ ∅ ∧ (𝑇 ++ ⟨“𝑆”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑇 ++ ⟨“𝑆”⟩)) − 1)){((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} ∈ 𝐸) ∧ (♯‘(𝑇 ++ ⟨“𝑆”⟩)) = ((𝑁 + 1) + 1)))
125	124	ex 412	. . . . . . . . . 10 ⊢ ((𝑇 ∈ Word 𝑉 ∧ (♯‘𝑇) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑇‘𝑖), (𝑇‘(𝑖 + 1))} ∈ 𝐸) → ((𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸)) → (((𝑇 ++ ⟨“𝑆”⟩) ≠ ∅ ∧ (𝑇 ++ ⟨“𝑆”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑇 ++ ⟨“𝑆”⟩)) − 1)){((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} ∈ 𝐸) ∧ (♯‘(𝑇 ++ ⟨“𝑆”⟩)) = ((𝑁 + 1) + 1))))
126	4, 125	syl 17	. . . . . . . . 9 ⊢ (𝑇 ∈ (𝑁 WWalksN 𝐺) → ((𝑁 ∈ ℕ0 ∧ (𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸)) → (((𝑇 ++ ⟨“𝑆”⟩) ≠ ∅ ∧ (𝑇 ++ ⟨“𝑆”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑇 ++ ⟨“𝑆”⟩)) − 1)){((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} ∈ 𝐸) ∧ (♯‘(𝑇 ++ ⟨“𝑆”⟩)) = ((𝑁 + 1) + 1))))
127	126	expd 415	. . . . . . . 8 ⊢ (𝑇 ∈ (𝑁 WWalksN 𝐺) → (𝑁 ∈ ℕ0 → ((𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸) → (((𝑇 ++ ⟨“𝑆”⟩) ≠ ∅ ∧ (𝑇 ++ ⟨“𝑆”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑇 ++ ⟨“𝑆”⟩)) − 1)){((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} ∈ 𝐸) ∧ (♯‘(𝑇 ++ ⟨“𝑆”⟩)) = ((𝑁 + 1) + 1)))))
128	127	impcom 407	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑇 ∈ (𝑁 WWalksN 𝐺)) → ((𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸) → (((𝑇 ++ ⟨“𝑆”⟩) ≠ ∅ ∧ (𝑇 ++ ⟨“𝑆”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑇 ++ ⟨“𝑆”⟩)) − 1)){((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} ∈ 𝐸) ∧ (♯‘(𝑇 ++ ⟨“𝑆”⟩)) = ((𝑁 + 1) + 1))))
129	128	adantll 715	. . . . . 6 ⊢ (((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0) ∧ 𝑇 ∈ (𝑁 WWalksN 𝐺)) → ((𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸) → (((𝑇 ++ ⟨“𝑆”⟩) ≠ ∅ ∧ (𝑇 ++ ⟨“𝑆”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑇 ++ ⟨“𝑆”⟩)) − 1)){((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} ∈ 𝐸) ∧ (♯‘(𝑇 ++ ⟨“𝑆”⟩)) = ((𝑁 + 1) + 1))))
130		iswwlksn 29923	. . . . . . . . . 10 ⊢ ((𝑁 + 1) ∈ ℕ0 → ((𝑇 ++ ⟨“𝑆”⟩) ∈ ((𝑁 + 1) WWalksN 𝐺) ↔ ((𝑇 ++ ⟨“𝑆”⟩) ∈ (WWalks‘𝐺) ∧ (♯‘(𝑇 ++ ⟨“𝑆”⟩)) = ((𝑁 + 1) + 1))))
131	115, 130	syl 17	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → ((𝑇 ++ ⟨“𝑆”⟩) ∈ ((𝑁 + 1) WWalksN 𝐺) ↔ ((𝑇 ++ ⟨“𝑆”⟩) ∈ (WWalks‘𝐺) ∧ (♯‘(𝑇 ++ ⟨“𝑆”⟩)) = ((𝑁 + 1) + 1))))
132	131	adantl 481	. . . . . . . 8 ⊢ ((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0) → ((𝑇 ++ ⟨“𝑆”⟩) ∈ ((𝑁 + 1) WWalksN 𝐺) ↔ ((𝑇 ++ ⟨“𝑆”⟩) ∈ (WWalks‘𝐺) ∧ (♯‘(𝑇 ++ ⟨“𝑆”⟩)) = ((𝑁 + 1) + 1))))
133	1, 3	iswwlks 29921	. . . . . . . . 9 ⊢ ((𝑇 ++ ⟨“𝑆”⟩) ∈ (WWalks‘𝐺) ↔ ((𝑇 ++ ⟨“𝑆”⟩) ≠ ∅ ∧ (𝑇 ++ ⟨“𝑆”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑇 ++ ⟨“𝑆”⟩)) − 1)){((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} ∈ 𝐸))
134	133	anbi1i 625	. . . . . . . 8 ⊢ (((𝑇 ++ ⟨“𝑆”⟩) ∈ (WWalks‘𝐺) ∧ (♯‘(𝑇 ++ ⟨“𝑆”⟩)) = ((𝑁 + 1) + 1)) ↔ (((𝑇 ++ ⟨“𝑆”⟩) ≠ ∅ ∧ (𝑇 ++ ⟨“𝑆”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑇 ++ ⟨“𝑆”⟩)) − 1)){((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} ∈ 𝐸) ∧ (♯‘(𝑇 ++ ⟨“𝑆”⟩)) = ((𝑁 + 1) + 1)))
135	132, 134	bitrdi 287	. . . . . . 7 ⊢ ((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0) → ((𝑇 ++ ⟨“𝑆”⟩) ∈ ((𝑁 + 1) WWalksN 𝐺) ↔ (((𝑇 ++ ⟨“𝑆”⟩) ≠ ∅ ∧ (𝑇 ++ ⟨“𝑆”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑇 ++ ⟨“𝑆”⟩)) − 1)){((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} ∈ 𝐸) ∧ (♯‘(𝑇 ++ ⟨“𝑆”⟩)) = ((𝑁 + 1) + 1))))
136	135	adantr 480	. . . . . 6 ⊢ (((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0) ∧ 𝑇 ∈ (𝑁 WWalksN 𝐺)) → ((𝑇 ++ ⟨“𝑆”⟩) ∈ ((𝑁 + 1) WWalksN 𝐺) ↔ (((𝑇 ++ ⟨“𝑆”⟩) ≠ ∅ ∧ (𝑇 ++ ⟨“𝑆”⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑇 ++ ⟨“𝑆”⟩)) − 1)){((𝑇 ++ ⟨“𝑆”⟩)‘𝑖), ((𝑇 ++ ⟨“𝑆”⟩)‘(𝑖 + 1))} ∈ 𝐸) ∧ (♯‘(𝑇 ++ ⟨“𝑆”⟩)) = ((𝑁 + 1) + 1))))
137	129, 136	sylibrd 259	. . . . 5 ⊢ (((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0) ∧ 𝑇 ∈ (𝑁 WWalksN 𝐺)) → ((𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸) → (𝑇 ++ ⟨“𝑆”⟩) ∈ ((𝑁 + 1) WWalksN 𝐺)))
138	137	ex 412	. . . 4 ⊢ ((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0) → (𝑇 ∈ (𝑁 WWalksN 𝐺) → ((𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸) → (𝑇 ++ ⟨“𝑆”⟩) ∈ ((𝑁 + 1) WWalksN 𝐺))))
139	138	3adant3 1133	. . 3 ⊢ ((𝐺 ∈ V ∧ 𝑁 ∈ ℕ0 ∧ 𝑇 ∈ Word 𝑉) → (𝑇 ∈ (𝑁 WWalksN 𝐺) → ((𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸) → (𝑇 ++ ⟨“𝑆”⟩) ∈ ((𝑁 + 1) WWalksN 𝐺))))
140	2, 139	mpcom 38	. 2 ⊢ (𝑇 ∈ (𝑁 WWalksN 𝐺) → ((𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸) → (𝑇 ++ ⟨“𝑆”⟩) ∈ ((𝑁 + 1) WWalksN 𝐺)))
141	140	3impib 1117	1 ⊢ ((𝑇 ∈ (𝑁 WWalksN 𝐺) ∧ 𝑆 ∈ 𝑉 ∧ {(lastS‘𝑇), 𝑆} ∈ 𝐸) → (𝑇 ++ ⟨“𝑆”⟩) ∈ ((𝑁 + 1) WWalksN 𝐺))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114   ≠ wne 2933  ∀wral 3052  Vcvv 3442   ∪ cun 3901   ⊆ wss 3903  ∅c0 4287  {csn 4582  {cpr 4584  ⟨cop 4588  ‘cfv 6500  (class class class)co 7368  0cc0 11038  1c1 11039   + caddc 11041   − cmin 11376  ℕ₀cn0 12413  ℤcz 12500  ℤ_≥cuz 12763  ...cfz 13435  ..^cfzo 13582  ♯chash 14265  Word cword 14448  lastSclsw 14497   ++ cconcat 14505  ⟨“cs1 14531  Vtxcvtx 29081  Edgcedg 29132  WWalkscwwlks 29910   WWalksN cwwlksn 29911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5226  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-cnex 11094  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-int 4905  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-we 5587  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6267  df-ord 6328  df-on 6329  df-lim 6330  df-suc 6331  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-riota 7325  df-ov 7371  df-oprab 7372  df-mpo 7373  df-om 7819  df-1st 7943  df-2nd 7944  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351  df-1o 8407  df-er 8645  df-map 8777  df-en 8896  df-dom 8897  df-sdom 8898  df-fin 8899  df-card 9863  df-pnf 11180  df-mnf 11181  df-xr 11182  df-ltxr 11183  df-le 11184  df-sub 11378  df-neg 11379  df-nn 12158  df-n0 12414  df-z 12501  df-uz 12764  df-fz 13436  df-fzo 13583  df-hash 14266  df-word 14449  df-lsw 14498  df-concat 14506  df-s1 14532  df-wwlks 29915  df-wwlksn 29916

This theorem is referenced by:  wwlksnextbi  29979  wwlksnextsurj  29985