Definition df-wwlksn 29082

Description: Define the set of all walks (in an undirected graph) of a fixed length n as words over the set of vertices. Such a word corresponds to the sequence p(0) p(1) ... p(n) of the vertices in a walk p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n) as defined in df-wlks 28853. (Contributed by Alexander van der Vekens, 15-Jul-2018.) (Revised by AV, 8-Apr-2021.)

Assertion

Ref	Expression
df-wwlksn	⊢ WWalksN = (𝑛 ∈ ℕ0, 𝑔 ∈ V ↦ {𝑤 ∈ (WWalks‘𝑔) ∣ (♯‘𝑤) = (𝑛 + 1)})

Distinct variable group:   𝑔,𝑛,𝑤

Detailed syntax breakdown of Definition df-wwlksn

Step	Hyp	Ref	Expression
1		cwwlksn 29077	. 2 class WWalksN
2		vn	. . 3 setvar 𝑛
3		vg	. . 3 setvar 𝑔
4		cn0 12471	. . 3 class ℕ0
5		cvv 3474	. . 3 class V
6		vw	. . . . . . 7 setvar 𝑤
7	6	cv 1540	. . . . . 6 class 𝑤
8		chash 14289	. . . . . 6 class ♯
9	7, 8	cfv 6543	. . . . 5 class (♯‘𝑤)
10	2	cv 1540	. . . . . 6 class 𝑛
11		c1 11110	. . . . . 6 class 1
12		caddc 11112	. . . . . 6 class +
13	10, 11, 12	co 7408	. . . . 5 class (𝑛 + 1)
14	9, 13	wceq 1541	. . . 4 wff (♯‘𝑤) = (𝑛 + 1)
15	3	cv 1540	. . . . 5 class 𝑔
16		cwwlks 29076	. . . . 5 class WWalks
17	15, 16	cfv 6543	. . . 4 class (WWalks‘𝑔)
18	14, 6, 17	crab 3432	. . 3 class {𝑤 ∈ (WWalks‘𝑔) ∣ (♯‘𝑤) = (𝑛 + 1)}
19	2, 3, 4, 5, 18	cmpo 7410	. 2 class (𝑛 ∈ ℕ0, 𝑔 ∈ V ↦ {𝑤 ∈ (WWalks‘𝑔) ∣ (♯‘𝑤) = (𝑛 + 1)})
20	1, 19	wceq 1541	1 wff WWalksN = (𝑛 ∈ ℕ0, 𝑔 ∈ V ↦ {𝑤 ∈ (WWalks‘𝑔) ∣ (♯‘𝑤) = (𝑛 + 1)})

This definition is referenced by:  wwlksn  29088  wwlknbp  29093  wspthsn  29099  iswwlksnon  29104