Definition df-clwwlk 16262

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 16261	. 2 class ClWWalks
2		vg	. . 3 setvar g
3		cvv 2802	. . 3 class _V
4		vw	. . . . . . 7 setvar w
5	4	cv 1396	. . . . . 6 class w
6		c0 3494	. . . . . 6 class (/)
7	5, 6	wne 2402	. . . . 5 wff w =/= (/)
8		vi	. . . . . . . . . 10 setvar i
9	8	cv 1396	. . . . . . . . 9 class i
10	9, 5	cfv 5326	. . . . . . . 8 class ( w ` i )
11		c1 8033	. . . . . . . . . 10 class 1
12		caddc 8035	. . . . . . . . . 10 class +
13	9, 11, 12	co 6018	. . . . . . . . 9 class ( i + 1 )
14	13, 5	cfv 5326	. . . . . . . 8 class ( w ` ( i + 1 ) )
15	10, 14	cpr 3670	. . . . . . 7 class { ( w ` i ) , ( w ` ( i + 1 ) ) }
16	2	cv 1396	. . . . . . . 8 class g
17		cedg 15927	. . . . . . . 8 class Edg
18	16, 17	cfv 5326	. . . . . . 7 class (Edg ` g )
19	15, 18	wcel 2202	. . . . . 6 wff { ( w ` i ) , ( w ` ( i + 1 ) ) } e. (Edg ` g )
20		cc0 8032	. . . . . . 7 class 0
21		chash 11038	. . . . . . . . 9 class ♯
22	5, 21	cfv 5326	. . . . . . . 8 class (♯ ` w )
23		cmin 8350	. . . . . . . 8 class -
24	22, 11, 23	co 6018	. . . . . . 7 class ( (♯ ` w ) - 1 )
25		cfzo 10377	. . . . . . 7 class ..^
26	20, 24, 25	co 6018	. . . . . 6 class ( 0..^ ( (♯ ` w ) - 1 ) )
27	19, 8, 26	wral 2510	. . . . 5 wff A. i e. ( 0..^ ( (♯ ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. (Edg ` g )
28		clsw 11162	. . . . . . . 8 class lastS
29	5, 28	cfv 5326	. . . . . . 7 class (lastS ` w )
30	20, 5	cfv 5326	. . . . . . 7 class ( w ` 0 )
31	29, 30	cpr 3670	. . . . . 6 class { (lastS ` w ) , ( w ` 0 ) }
32	31, 18	wcel 2202	. . . . 5 wff { (lastS ` w ) , ( w ` 0 ) } e. (Edg ` g )
33	7, 27, 32	w3a 1004	. . . 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 15882	. . . . . 6 class Vtx
35	16, 34	cfv 5326	. . . . 5 class (Vtx ` g )
36	35	cword 11117	. . . 4 class Word (Vtx ` g )
37	33, 4, 36	crab 2514	. . 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 4150	. 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 1397	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  16263  isclwwlk  16264  clwwlkbp  16265