Metamath Proof Explorer

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=g∈V⟼w∈WordVtx⁡g|w≠∅∧∀i∈0..^w−1w⁡iw⁡i+1∈Edg⁡g∧lastS⁡ww⁡0∈Edg⁡g

Detailed syntax breakdown

Step Hyp Ref Expression
0 cclwwlk classClWWalks
1 vg setvarg
2 cvv classV
3 vw setvarw
4 cvtx classVtx
5 1 cv setvarg
6 5 4 cfv classVtx⁡g
7 6 cword classWordVtx⁡g
8 3 cv setvarw
9 c0 class∅
10 8 9 wne wffw≠∅
11 vi setvari
12 cc0 class0
13 cfzo class..^
14 chash class.
15 8 14 cfv classw
16 cmin class−
17 c1 class1
18 15 17 16 co classw−1
19 12 18 13 co class0..^w−1
20 11 cv setvari
21 20 8 cfv classw⁡i
22 caddc class+
23 20 17 22 co classi+1
24 23 8 cfv classw⁡i+1
25 21 24 cpr classw⁡iw⁡i+1
26 cedg classEdg
27 5 26 cfv classEdg⁡g
28 25 27 wcel wffw⁡iw⁡i+1∈Edg⁡g
29 28 11 19 wral wff∀i∈0..^w−1w⁡iw⁡i+1∈Edg⁡g
30 clsw classlastS
31 8 30 cfv classlastS⁡w
32 12 8 cfv classw⁡0
33 31 32 cpr classlastS⁡ww⁡0
34 33 27 wcel wfflastS⁡ww⁡0∈Edg⁡g
35 10 29 34 w3a wffw≠∅∧∀i∈0..^w−1w⁡iw⁡i+1∈Edg⁡g∧lastS⁡ww⁡0∈Edg⁡g
36 35 3 7 crab classw∈WordVtx⁡g|w≠∅∧∀i∈0..^w−1w⁡iw⁡i+1∈Edg⁡g∧lastS⁡ww⁡0∈Edg⁡g
37 1 2 36 cmpt classg∈V⟼w∈WordVtx⁡g|w≠∅∧∀i∈0..^w−1w⁡iw⁡i+1∈Edg⁡g∧lastS⁡ww⁡0∈Edg⁡g
38 0 37 wceq wffClWWalks=g∈V⟼w∈WordVtx⁡g|w≠∅∧∀i∈0..^w−1w⁡iw⁡i+1∈Edg⁡g∧lastS⁡ww⁡0∈Edg⁡g