Definition df-wwlks 26722

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-wlks 26495. w = (/) has to be excluded because a walk always consists of at least one vertex, see wlkn0 26516. (Contributed by Alexander van der Vekens, 15-Jul-2018.) (Revised by AV, 8-Apr-2021.)

Assertion

Ref	Expression
df-wwlks	|- WWalks = ( g e. _V |-> { w e. Word (Vtx ` g ) | ( w =/= (/) /\ A. i e. ( 0..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. (Edg ` g ) ) } )

Distinct variable group:   g, i, w

Detailed syntax breakdown of Definition df-wwlks

Step	Hyp	Ref	Expression
1		cwwlks 26717	. 2 class WWalks
2		vg	. . 3 setvar g
3		cvv 3200	. . 3 class _V
4		vw	. . . . . . 7 setvar w
5	4	cv 1482	. . . . . 6 class w
6		c0 3915	. . . . . 6 class (/)
7	5, 6	wne 2794	. . . . 5 wff w =/= (/)
8		vi	. . . . . . . . . 10 setvar i
9	8	cv 1482	. . . . . . . . 9 class i
10	9, 5	cfv 5888	. . . . . . . 8 class ( w ` i )
11		c1 9937	. . . . . . . . . 10 class 1
12		caddc 9939	. . . . . . . . . 10 class +
13	9, 11, 12	co 6650	. . . . . . . . 9 class ( i + 1 )
14	13, 5	cfv 5888	. . . . . . . 8 class ( w ` ( i + 1 ) )
15	10, 14	cpr 4179	. . . . . . 7 class { ( w ` i ) , ( w ` ( i + 1 ) ) }
16	2	cv 1482	. . . . . . . 8 class g
17		cedg 25939	. . . . . . . 8 class Edg
18	16, 17	cfv 5888	. . . . . . 7 class (Edg ` g )
19	15, 18	wcel 1990	. . . . . 6 wff { ( w ` i ) , ( w ` ( i + 1 ) ) } e. (Edg ` g )
20		cc0 9936	. . . . . . 7 class 0
21		chash 13117	. . . . . . . . 9 class #
22	5, 21	cfv 5888	. . . . . . . 8 class ( # ` w )
23		cmin 10266	. . . . . . . 8 class -
24	22, 11, 23	co 6650	. . . . . . 7 class ( ( # ` w ) - 1 )
25		cfzo 12465	. . . . . . 7 class ..^
26	20, 24, 25	co 6650	. . . . . 6 class ( 0..^ ( ( # ` w ) - 1 ) )
27	19, 8, 26	wral 2912	. . . . 5 wff A. i e. ( 0..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. (Edg ` g )
28	7, 27	wa 384	. . . 4 wff ( w =/= (/) /\ A. i e. ( 0..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. (Edg ` g ) )
29		cvtx 25874	. . . . . 6 class Vtx
30	16, 29	cfv 5888	. . . . 5 class (Vtx ` g )
31	30	cword 13291	. . . 4 class Word (Vtx ` g )
32	28, 4, 31	crab 2916	. . 3 class { w e. Word (Vtx ` g ) | ( w =/= (/) /\ A. i e. ( 0..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. (Edg ` g ) ) }
33	2, 3, 32	cmpt 4729	. 2 class ( g e. _V |-> { w e. Word (Vtx ` g ) | ( w =/= (/) /\ A. i e. ( 0..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. (Edg ` g ) ) } )
34	1, 33	wceq 1483	1 wff WWalks = ( g e. _V |-> { w e. Word (Vtx ` g ) | ( w =/= (/) /\ A. i e. ( 0..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. (Edg ` g ) ) } )

This definition is referenced by:  wwlks  26727