Metamath Proof Explorer

Definition df-wwlks

Description: Define the set of all 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) p(n) of the vertices in a walk p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n) as defined in df-wlks . w = (/) has to be excluded because a walk always consists of at least one vertex, see wlkn0 . (Contributed by Alexander van der Vekens, 15-Jul-2018) (Revised by AV, 8-Apr-2021)

Ref Expression
Assertion df-wwlks ⊢WWalks=g∈V⟼w∈WordVtx⁡g|w≠∅∧∀i∈0..^w−1w⁡iw⁡i+1∈Edg⁡g

Detailed syntax breakdown

Step Hyp Ref Expression
0 cwwlks classWWalks
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 10 29 wa wffw≠∅∧∀i∈0..^w−1w⁡iw⁡i+1∈Edg⁡g
31 30 3 7 crab classw∈WordVtx⁡g|w≠∅∧∀i∈0..^w−1w⁡iw⁡i+1∈Edg⁡g
32 1 2 31 cmpt classg∈V⟼w∈WordVtx⁡g|w≠∅∧∀i∈0..^w−1w⁡iw⁡i+1∈Edg⁡g
33 0 32 wceq wffWWalks=g∈V⟼w∈WordVtx⁡g|w≠∅∧∀i∈0..^w−1w⁡iw⁡i+1∈Edg⁡g