Definition df-clwwlk 16838

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 16837	. 2 class ClWWalks
2		vg	. . 3 setvar g
3		cvv 2821	. . 3 class _V
4		vw	. . . . . . 7 setvar w
5	4	cv 1401	. . . . . 6 class w
6		c0 3520	. . . . . 6 class (/)
7	5, 6	wne 2420	. . . . 5 wff w =/= (/)
8		vi	. . . . . . . . . 10 setvar i
9	8	cv 1401	. . . . . . . . 9 class i
10	9, 5	cfv 5380	. . . . . . . 8 class ( w ` i )
11		c1 8186	. . . . . . . . . 10 class 1
12		caddc 8188	. . . . . . . . . 10 class +
13	9, 11, 12	co 6088	. . . . . . . . 9 class ( i + 1 )
14	13, 5	cfv 5380	. . . . . . . 8 class ( w ` ( i + 1 ) )
15	10, 14	cpr 3710	. . . . . . 7 class { ( w ` i ) , ( w ` ( i + 1 ) ) }
16	2	cv 1401	. . . . . . . 8 class g
17		cedg 16503	. . . . . . . 8 class Edg
18	16, 17	cfv 5380	. . . . . . 7 class (Edg ` g )
19	15, 18	wcel 2209	. . . . . 6 wff { ( w ` i ) , ( w ` ( i + 1 ) ) } e. (Edg ` g )
20		cc0 8185	. . . . . . 7 class 0
21		chash 11236	. . . . . . . . 9 class ♯
22	5, 21	cfv 5380	. . . . . . . 8 class (♯ ` w )
23		cmin 8504	. . . . . . . 8 class -
24	22, 11, 23	co 6088	. . . . . . 7 class ( (♯ ` w ) - 1 )
25		cfzo 10566	. . . . . . 7 class ..^
26	20, 24, 25	co 6088	. . . . . 6 class ( 0..^ ( (♯ ` w ) - 1 ) )
27	19, 8, 26	wral 2528	. . . . 5 wff A. i e. ( 0..^ ( (♯ ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. (Edg ` g )
28		clsw 11371	. . . . . . . 8 class lastS
29	5, 28	cfv 5380	. . . . . . 7 class (lastS ` w )
30	20, 5	cfv 5380	. . . . . . 7 class ( w ` 0 )
31	29, 30	cpr 3710	. . . . . 6 class { (lastS ` w ) , ( w ` 0 ) }
32	31, 18	wcel 2209	. . . . 5 wff { (lastS ` w ) , ( w ` 0 ) } e. (Edg ` g )
33	7, 27, 32	w3a 1009	. . . 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 16458	. . . . . 6 class Vtx
35	16, 34	cfv 5380	. . . . 5 class (Vtx ` g )
36	35	cword 11326	. . . 4 class Word (Vtx ` g )
37	33, 4, 36	crab 2532	. . 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 4193	. 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 1402	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 used by:  clwwlkg  16839  isclwwlk  16840  clwwlkbp  16841