This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-wwlksn

Description: Define the set of all walks (in an undirected graph) of a fixed length n as words over the set of vertices. Such a word corresponds to the sequence p(0) p(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 . (Contributed by Alexander van der Vekens, 15-Jul-2018) (Revised by AV, 8-Apr-2021)

Ref Expression
Assertion df-wwlksn ⊢ WWalksN = n ∈ ℕ 0 , g ∈ V ⟼ w ∈ WWalks ⁡ g | w = n + 1

Detailed syntax breakdown

Step Hyp Ref Expression
0 cwwlksn class WWalksN
1 vn setvar n
2 cn0 class ℕ 0
3 vg setvar g
4 cvv class V
5 vw setvar w
6 cwwlks class WWalks
7 3 cv setvar g
8 7 6 cfv class WWalks ⁡ g
9 chash class .
10 5 cv setvar w
11 10 9 cfv class w
12 1 cv setvar n
13 caddc class +
14 c1 class 1
15 12 14 13 co class n + 1
16 11 15 wceq wff w = n + 1
17 16 5 8 crab class w ∈ WWalks ⁡ g | w = n + 1
18 1 3 2 4 17 cmpo class n ∈ ℕ 0 , g ∈ V ⟼ w ∈ WWalks ⁡ g | w = n + 1
19 0 18 wceq wff WWalksN = n ∈ ℕ 0 , g ∈ V ⟼ w ∈ WWalks ⁡ g | w = n + 1