Definition df-clwwlk 16187

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 16186	. 2 class ClWWalks
2		vg	. . 3 setvar g
3		cvv 2800	. . 3 class _V
4		vw	. . . . . . 7 setvar w
5	4	cv 1394	. . . . . 6 class w
6		c0 3492	. . . . . 6 class (/)
7	5, 6	wne 2400	. . . . 5 wff w =/= (/)
8		vi	. . . . . . . . . 10 setvar i
9	8	cv 1394	. . . . . . . . 9 class i
10	9, 5	cfv 5324	. . . . . . . 8 class ( w ` i )
11		c1 8023	. . . . . . . . . 10 class 1
12		caddc 8025	. . . . . . . . . 10 class +
13	9, 11, 12	co 6013	. . . . . . . . 9 class ( i + 1 )
14	13, 5	cfv 5324	. . . . . . . 8 class ( w ` ( i + 1 ) )
15	10, 14	cpr 3668	. . . . . . 7 class { ( w ` i ) , ( w ` ( i + 1 ) ) }
16	2	cv 1394	. . . . . . . 8 class g
17		cedg 15898	. . . . . . . 8 class Edg
18	16, 17	cfv 5324	. . . . . . 7 class (Edg ` g )
19	15, 18	wcel 2200	. . . . . 6 wff { ( w ` i ) , ( w ` ( i + 1 ) ) } e. (Edg ` g )
20		cc0 8022	. . . . . . 7 class 0
21		chash 11027	. . . . . . . . 9 class ♯
22	5, 21	cfv 5324	. . . . . . . 8 class (♯ ` w )
23		cmin 8340	. . . . . . . 8 class -
24	22, 11, 23	co 6013	. . . . . . 7 class ( (♯ ` w ) - 1 )
25		cfzo 10367	. . . . . . 7 class ..^
26	20, 24, 25	co 6013	. . . . . 6 class ( 0..^ ( (♯ ` w ) - 1 ) )
27	19, 8, 26	wral 2508	. . . . 5 wff A. i e. ( 0..^ ( (♯ ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. (Edg ` g )
28		clsw 11148	. . . . . . . 8 class lastS
29	5, 28	cfv 5324	. . . . . . 7 class (lastS ` w )
30	20, 5	cfv 5324	. . . . . . 7 class ( w ` 0 )
31	29, 30	cpr 3668	. . . . . 6 class { (lastS ` w ) , ( w ` 0 ) }
32	31, 18	wcel 2200	. . . . 5 wff { (lastS ` w ) , ( w ` 0 ) } e. (Edg ` g )
33	7, 27, 32	w3a 1002	. . . 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 15853	. . . . . 6 class Vtx
35	16, 34	cfv 5324	. . . . 5 class (Vtx ` g )
36	35	cword 11103	. . . 4 class Word (Vtx ` g )
37	33, 4, 36	crab 2512	. . 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 4148	. 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 1395	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  16188  isclwwlk  16189  clwwlkbp  16190