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

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 = ( 𝑔 ∈ V ↦ { 𝑤 ∈ Word ( Vtx ‘ 𝑔 ) ∣ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝑔 ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cwwlks ⊢ WWalks
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 10 29 wa ⊢ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝑔 ) )
31 30 3 7 crab ⊢ { 𝑤 ∈ Word ( Vtx ‘ 𝑔 ) ∣ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝑔 ) ) }
32 1 2 31 cmpt ⊢ ( 𝑔 ∈ V ↦ { 𝑤 ∈ Word ( Vtx ‘ 𝑔 ) ∣ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝑔 ) ) } )
33 0 32 wceq ⊢ WWalks = ( 𝑔 ∈ V ↦ { 𝑤 ∈ Word ( Vtx ‘ 𝑔 ) ∣ ( 𝑤 ≠ ∅ ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑤 ) − 1 ) ) { ( 𝑤 ‘ 𝑖 ) , ( 𝑤 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝑔 ) ) } )