Definition df-wwlk 26207

Description: Define the set of all Walks (in an undirected graph) as words over the set of vertices. Such a word corresponds to the sequence p(0) p(1) ... p(n-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-wlk 26036. 𝑤 = ∅ has to be excluded because a walk always consists of at least one vertex, see wlkn0 26055. (Contributed by Alexander van der Vekens, 15-Jul-2018.)

Assertion

Ref	Expression
df-wwlk	⊢ WWalks = (𝑣 ∈ V, 𝑒 ∈ V ↦ {𝑤 ∈ Word 𝑣 ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝑒)})

Distinct variable group:   𝑒,𝑖,𝑣,𝑤

Detailed syntax breakdown of Definition df-wwlk

Step	Hyp	Ref	Expression
1		cwwlk 26205	. 2 class WWalks
2		vv	. . 3 setvar 𝑣
3		ve	. . 3 setvar 𝑒
4		cvv 3173	. . 3 class V
5		vw	. . . . . . 7 setvar 𝑤
6	5	cv 1474	. . . . . 6 class 𝑤
7		c0 3874	. . . . . 6 class ∅
8	6, 7	wne 2780	. . . . 5 wff 𝑤 ≠ ∅
9		vi	. . . . . . . . . 10 setvar 𝑖
10	9	cv 1474	. . . . . . . . 9 class 𝑖
11	10, 6	cfv 5804	. . . . . . . 8 class (𝑤‘𝑖)
12		c1 9816	. . . . . . . . . 10 class 1
13		caddc 9818	. . . . . . . . . 10 class +
14	10, 12, 13	co 6549	. . . . . . . . 9 class (𝑖 + 1)
15	14, 6	cfv 5804	. . . . . . . 8 class (𝑤‘(𝑖 + 1))
16	11, 15	cpr 4127	. . . . . . 7 class {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))}
17	3	cv 1474	. . . . . . . 8 class 𝑒
18	17	crn 5039	. . . . . . 7 class ran 𝑒
19	16, 18	wcel 1977	. . . . . 6 wff {(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝑒
20		cc0 9815	. . . . . . 7 class 0
21		chash 12979	. . . . . . . . 9 class #
22	6, 21	cfv 5804	. . . . . . . 8 class (#‘𝑤)
23		cmin 10145	. . . . . . . 8 class −
24	22, 12, 23	co 6549	. . . . . . 7 class ((#‘𝑤) − 1)
25		cfzo 12334	. . . . . . 7 class ..^
26	20, 24, 25	co 6549	. . . . . 6 class (0..^((#‘𝑤) − 1))
27	19, 9, 26	wral 2896	. . . . 5 wff ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝑒
28	8, 27	wa 383	. . . 4 wff (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝑒)
29	2	cv 1474	. . . . 5 class 𝑣
30	29	cword 13146	. . . 4 class Word 𝑣
31	28, 5, 30	crab 2900	. . 3 class {𝑤 ∈ Word 𝑣 ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝑒)}
32	2, 3, 4, 4, 31	cmpt2 6551	. 2 class (𝑣 ∈ V, 𝑒 ∈ V ↦ {𝑤 ∈ Word 𝑣 ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝑒)})
33	1, 32	wceq 1475	1 wff WWalks = (𝑣 ∈ V, 𝑒 ∈ V ↦ {𝑤 ∈ Word 𝑣 ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ ran 𝑒)})

This definition is referenced by:  wwlk  26209  wwlkprop  26213