# Metamath Proof Explorer

## Definition df-wwlksn

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 . (Contributed by Alexander van der Vekens, 15-Jul-2018) (Revised by AV, 8-Apr-2021)

Ref Expression
Assertion df-wwlksn ${⊢}\mathrm{WWalksN}=\left({n}\in {ℕ}_{0},{g}\in \mathrm{V}⟼\left\{{w}\in \mathrm{WWalks}\left({g}\right)|\left|{w}\right|={n}+1\right\}\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cwwlksn ${class}\mathrm{WWalksN}$
1 vn ${setvar}{n}$
2 cn0 ${class}{ℕ}_{0}$
3 vg ${setvar}{g}$
4 cvv ${class}\mathrm{V}$
5 vw ${setvar}{w}$
6 cwwlks ${class}\mathrm{WWalks}$
7 3 cv ${setvar}{g}$
8 7 6 cfv ${class}\mathrm{WWalks}\left({g}\right)$
9 chash ${class}\left|.\right|$
10 5 cv ${setvar}{w}$
11 10 9 cfv ${class}\left|{w}\right|$
12 1 cv ${setvar}{n}$
13 caddc ${class}+$
14 c1 ${class}1$
15 12 14 13 co ${class}\left({n}+1\right)$
16 11 15 wceq ${wff}\left|{w}\right|={n}+1$
17 16 5 8 crab ${class}\left\{{w}\in \mathrm{WWalks}\left({g}\right)|\left|{w}\right|={n}+1\right\}$
18 1 3 2 4 17 cmpo ${class}\left({n}\in {ℕ}_{0},{g}\in \mathrm{V}⟼\left\{{w}\in \mathrm{WWalks}\left({g}\right)|\left|{w}\right|={n}+1\right\}\right)$
19 0 18 wceq ${wff}\mathrm{WWalksN}=\left({n}\in {ℕ}_{0},{g}\in \mathrm{V}⟼\left\{{w}\in \mathrm{WWalks}\left({g}\right)|\left|{w}\right|={n}+1\right\}\right)$