Definition df-clwwlk 16513

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 16512	. 2 class ClWWalks
2		vg	. . 3 setvar g
3		cvv 2815	. . 3 class _V
4		vw	. . . . . . 7 setvar w
5	4	cv 1397	. . . . . 6 class w
6		c0 3512	. . . . . 6 class (/)
7	5, 6	wne 2414	. . . . 5 wff w =/= (/)
8		vi	. . . . . . . . . 10 setvar i
9	8	cv 1397	. . . . . . . . 9 class i
10	9, 5	cfv 5357	. . . . . . . 8 class ( w ` i )
11		c1 8144	. . . . . . . . . 10 class 1
12		caddc 8146	. . . . . . . . . 10 class +
13	9, 11, 12	co 6058	. . . . . . . . 9 class ( i + 1 )
14	13, 5	cfv 5357	. . . . . . . 8 class ( w ` ( i + 1 ) )
15	10, 14	cpr 3695	. . . . . . 7 class { ( w ` i ) , ( w ` ( i + 1 ) ) }
16	2	cv 1397	. . . . . . . 8 class g
17		cedg 16178	. . . . . . . 8 class Edg
18	16, 17	cfv 5357	. . . . . . 7 class (Edg ` g )
19	15, 18	wcel 2205	. . . . . 6 wff { ( w ` i ) , ( w ` ( i + 1 ) ) } e. (Edg ` g )
20		cc0 8143	. . . . . . 7 class 0
21		chash 11163	. . . . . . . . 9 class ♯
22	5, 21	cfv 5357	. . . . . . . 8 class (♯ ` w )
23		cmin 8460	. . . . . . . 8 class -
24	22, 11, 23	co 6058	. . . . . . 7 class ( (♯ ` w ) - 1 )
25		cfzo 10498	. . . . . . 7 class ..^
26	20, 24, 25	co 6058	. . . . . 6 class ( 0..^ ( (♯ ` w ) - 1 ) )
27	19, 8, 26	wral 2522	. . . . 5 wff A. i e. ( 0..^ ( (♯ ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. (Edg ` g )
28		clsw 11294	. . . . . . . 8 class lastS
29	5, 28	cfv 5357	. . . . . . 7 class (lastS ` w )
30	20, 5	cfv 5357	. . . . . . 7 class ( w ` 0 )
31	29, 30	cpr 3695	. . . . . 6 class { (lastS ` w ) , ( w ` 0 ) }
32	31, 18	wcel 2205	. . . . 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 16133	. . . . . 6 class Vtx
35	16, 34	cfv 5357	. . . . 5 class (Vtx ` g )
36	35	cword 11249	. . . 4 class Word (Vtx ` g )
37	33, 4, 36	crab 2526	. . 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 4176	. 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  16514  isclwwlk  16515  clwwlkbp  16516