Definition df-clwwlk 16316

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 16315	. 2 class ClWWalks
2		vg	. . 3 setvar g
3		cvv 2803	. . 3 class _V
4		vw	. . . . . . 7 setvar w
5	4	cv 1397	. . . . . 6 class w
6		c0 3496	. . . . . 6 class (/)
7	5, 6	wne 2403	. . . . 5 wff w =/= (/)
8		vi	. . . . . . . . . 10 setvar i
9	8	cv 1397	. . . . . . . . 9 class i
10	9, 5	cfv 5333	. . . . . . . 8 class ( w ` i )
11		c1 8076	. . . . . . . . . 10 class 1
12		caddc 8078	. . . . . . . . . 10 class +
13	9, 11, 12	co 6028	. . . . . . . . 9 class ( i + 1 )
14	13, 5	cfv 5333	. . . . . . . 8 class ( w ` ( i + 1 ) )
15	10, 14	cpr 3674	. . . . . . 7 class { ( w ` i ) , ( w ` ( i + 1 ) ) }
16	2	cv 1397	. . . . . . . 8 class g
17		cedg 15981	. . . . . . . 8 class Edg
18	16, 17	cfv 5333	. . . . . . 7 class (Edg ` g )
19	15, 18	wcel 2202	. . . . . 6 wff { ( w ` i ) , ( w ` ( i + 1 ) ) } e. (Edg ` g )
20		cc0 8075	. . . . . . 7 class 0
21		chash 11083	. . . . . . . . 9 class ♯
22	5, 21	cfv 5333	. . . . . . . 8 class (♯ ` w )
23		cmin 8392	. . . . . . . 8 class -
24	22, 11, 23	co 6028	. . . . . . 7 class ( (♯ ` w ) - 1 )
25		cfzo 10422	. . . . . . 7 class ..^
26	20, 24, 25	co 6028	. . . . . 6 class ( 0..^ ( (♯ ` w ) - 1 ) )
27	19, 8, 26	wral 2511	. . . . 5 wff A. i e. ( 0..^ ( (♯ ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. (Edg ` g )
28		clsw 11207	. . . . . . . 8 class lastS
29	5, 28	cfv 5333	. . . . . . 7 class (lastS ` w )
30	20, 5	cfv 5333	. . . . . . 7 class ( w ` 0 )
31	29, 30	cpr 3674	. . . . . 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 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 15936	. . . . . 6 class Vtx
35	16, 34	cfv 5333	. . . . 5 class (Vtx ` g )
36	35	cword 11162	. . . 4 class Word (Vtx ` g )
37	33, 4, 36	crab 2515	. . 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 4155	. 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  16317  isclwwlk  16318  clwwlkbp  16319