Definition df-clwwlks 26877

Description: Define the set of all closed 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) of the vertices in a closed walk p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n)=p(0) as defined in df-clwlks 26667. Notice that the word does not contain the terminating vertex p(n) of the walk, because it is always equal to the first vertex of the closed walk. (Contributed by Alexander van der Vekens, 20-Mar-2018.) (Revised by AV, 24-Apr-2021.)

Assertion

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

Distinct variable group:   g, i, w

Detailed syntax breakdown of Definition df-clwwlks

Step	Hyp	Ref	Expression
1		cclwwlks 26875	. 2 class ClWWalks
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		clsw 13292	. . . . . . . 8 class lastS
29	5, 28	cfv 5888	. . . . . . 7 class ( lastS ` w )
30	20, 5	cfv 5888	. . . . . . 7 class ( w ` 0 )
31	29, 30	cpr 4179	. . . . . 6 class { ( lastS ` w ) , ( w ` 0 ) }
32	31, 18	wcel 1990	. . . . 5 wff { ( lastS ` w ) , ( w ` 0 ) } e. (Edg ` g )
33	7, 27, 32	w3a 1037	. . . 4 wff ( w =/= (/) /\ A. i e. ( 0..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. (Edg ` g ) /\ { ( lastS ` w ) , ( w ` 0 ) } e. (Edg ` g ) )
34		cvtx 25874	. . . . . 6 class Vtx
35	16, 34	cfv 5888	. . . . 5 class (Vtx ` g )
36	35	cword 13291	. . . 4 class Word (Vtx ` g )
37	33, 4, 36	crab 2916	. . 3 class { w e. Word (Vtx ` g ) | ( w =/= (/) /\ A. i e. ( 0..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. (Edg ` g ) /\ { ( lastS ` w ) , ( w ` 0 ) } e. (Edg ` g ) ) }
38	2, 3, 37	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 ) /\ { ( lastS ` w ) , ( w ` 0 ) } e. (Edg ` g ) ) } )
39	1, 38	wceq 1483	1 wff ClWWalks = ( g e. _V |-> { w e. Word (Vtx ` g ) | ( w =/= (/) /\ A. i e. ( 0..^ ( ( # ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. (Edg ` g ) /\ { ( lastS ` w ) , ( w ` 0 ) } e. (Edg ` g ) ) } )

This definition is referenced by:  clwwlks  26879