Definition df-clwwlk

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 in df-clwlks . 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)

	Ref	Expression
Assertion	df-clwwlk	⊢ ClWWalks = ( 𝑔 ∈ V ↦ { 𝑤 ∈ Word ( Vtx ‘ 𝑔 ) ∣ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝑔 ) ∧ { ( lastS ‘ 𝑤 ) , ( 𝑤 ‘ 0 ) } ∈ ( Edg ‘ 𝑔 ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cclwwlk	⊢ ClWWalks
1		vg	⊢ 𝑔
2		cvv	⊢ V
3		vw	⊢ 𝑤
4		cvtx	⊢ Vtx
5	1	cv	⊢ 𝑔
6	5 4	cfv	⊢ ( Vtx ‘ 𝑔 )
7	6	cword	⊢ Word ( Vtx ‘ 𝑔 )
8	3	cv	⊢ 𝑤
9		c0	⊢ ∅
10	8 9	wne	⊢ 𝑤 ≠ ∅
11		vi	⊢ 𝑖
12		cc0	⊢ 0
13		cfzo	⊢ ..^
14		chash	⊢ ♯
15	8 14	cfv	⊢ ( ♯ ‘ 𝑤 )
16		cmin	⊢ −
17		c1	⊢ 1
18	15 17 16	co	⊢ ( ( ♯ ‘ 𝑤 ) − 1 )
19	12 18 13	co	⊢ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) )
20	11	cv	⊢ 𝑖
21	20 8	cfv	⊢ ( 𝑤 ‘ 𝑖 )
22		caddc	⊢ +
23	20 17 22	co	⊢ ( 𝑖 + 1 )
24	23 8	cfv	⊢ ( 𝑤 ‘ ( 𝑖 + 1 ) )
25	21 24	cpr	⊢ { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) }
26		cedg	⊢ Edg
27	5 26	cfv	⊢ ( Edg ‘ 𝑔 )
28	25 27	wcel	⊢ { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝑔 )
29	28 11 19	wral	⊢ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝑔 )
30		clsw	⊢ lastS
31	8 30	cfv	⊢ ( lastS ‘ 𝑤 )
32	12 8	cfv	⊢ ( 𝑤 ‘ 0 )
33	31 32	cpr	⊢ { ( lastS ‘ 𝑤 ) , ( 𝑤 ‘ 0 ) }
34	33 27	wcel	⊢ { ( lastS ‘ 𝑤 ) , ( 𝑤 ‘ 0 ) } ∈ ( Edg ‘ 𝑔 )
35	10 29 34	w3a	⊢ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝑔 ) ∧ { ( lastS ‘ 𝑤 ) , ( 𝑤 ‘ 0 ) } ∈ ( Edg ‘ 𝑔 ) )
36	35 3 7	crab	⊢ { 𝑤 ∈ Word ( Vtx ‘ 𝑔 ) ∣ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝑔 ) ∧ { ( lastS ‘ 𝑤 ) , ( 𝑤 ‘ 0 ) } ∈ ( Edg ‘ 𝑔 ) ) }
37	1 2 36	cmpt	⊢ ( 𝑔 ∈ V ↦ { 𝑤 ∈ Word ( Vtx ‘ 𝑔 ) ∣ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝑔 ) ∧ { ( lastS ‘ 𝑤 ) , ( 𝑤 ‘ 0 ) } ∈ ( Edg ‘ 𝑔 ) ) } )
38	0 37	wceq	⊢ ClWWalks = ( 𝑔 ∈ V ↦ { 𝑤 ∈ Word ( Vtx ‘ 𝑔 ) ∣ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝑔 ) ∧ { ( lastS ‘ 𝑤 ) , ( 𝑤 ‘ 0 ) } ∈ ( Edg ‘ 𝑔 ) ) } )