Definition df-clwwlk 16387

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 elsewhere. 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-clwwlk	|- 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-clwwlk

Step	Hyp	Ref	Expression
1		cclwwlk 16386	. 2 class ClWWalks
2		vg	. . 3 setvar g
3		cvv 2813	. . 3 class _V
4		vw	. . . . . . 7 setvar w
5	4	cv 1397	. . . . . 6 class w
6		c0 3508	. . . . . 6 class (/)
7	5, 6	wne 2412	. . . . 5 wff w =/= (/)
8		vi	. . . . . . . . . 10 setvar i
9	8	cv 1397	. . . . . . . . 9 class i
10	9, 5	cfv 5352	. . . . . . . 8 class ( w ` i )
11		c1 8128	. . . . . . . . . 10 class 1
12		caddc 8130	. . . . . . . . . 10 class +
13	9, 11, 12	co 6050	. . . . . . . . 9 class ( i + 1 )
14	13, 5	cfv 5352	. . . . . . . 8 class ( w ` ( i + 1 ) )
15	10, 14	cpr 3690	. . . . . . 7 class { ( w ` i ) , ( w ` ( i + 1 ) ) }
16	2	cv 1397	. . . . . . . 8 class g
17		cedg 16052	. . . . . . . 8 class Edg
18	16, 17	cfv 5352	. . . . . . 7 class (Edg ` g )
19	15, 18	wcel 2203	. . . . . 6 wff { ( w ` i ) , ( w ` ( i + 1 ) ) } e. (Edg ` g )
20		cc0 8127	. . . . . . 7 class 0
21		chash 11138	. . . . . . . . 9 class ♯
22	5, 21	cfv 5352	. . . . . . . 8 class (♯ ` w )
23		cmin 8444	. . . . . . . 8 class -
24	22, 11, 23	co 6050	. . . . . . 7 class ( (♯ ` w ) - 1 )
25		cfzo 10476	. . . . . . 7 class ..^
26	20, 24, 25	co 6050	. . . . . 6 class ( 0..^ ( (♯ ` w ) - 1 ) )
27	19, 8, 26	wral 2520	. . . . 5 wff A. i e. ( 0..^ ( (♯ ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. (Edg ` g )
28		clsw 11269	. . . . . . . 8 class lastS
29	5, 28	cfv 5352	. . . . . . 7 class (lastS ` w )
30	20, 5	cfv 5352	. . . . . . 7 class ( w ` 0 )
31	29, 30	cpr 3690	. . . . . 6 class { (lastS ` w ) , ( w ` 0 ) }
32	31, 18	wcel 2203	. . . . 5 wff { (lastS ` w ) , ( w ` 0 ) } e. (Edg ` g )
33	7, 27, 32	w3a 1005	. . . 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 16007	. . . . . 6 class Vtx
35	16, 34	cfv 5352	. . . . 5 class (Vtx ` g )
36	35	cword 11224	. . . 4 class Word (Vtx ` g )
37	33, 4, 36	crab 2524	. . 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 4171	. 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 1398	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:  clwwlkg  16388  isclwwlk  16389  clwwlkbp  16390