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 = ( 𝑛 ∈ ℕ0 , 𝑔 ∈ V ↦ { 𝑤 ∈ ( WWalks ‘ 𝑔 ) ∣ ( ♯ ‘ 𝑤 ) = ( 𝑛 + 1 ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cwwlksn ⊢ WWalksN
1 vn ⊢ 𝑛
2 cn0 ⊢ ℕ0
3 vg ⊢ 𝑔
4 cvv ⊢ V
5 vw ⊢ 𝑤
6 cwwlks ⊢ WWalks
7 3 cv ⊢ 𝑔
8 7 6 cfv ⊢ ( WWalks ‘ 𝑔 )
9 chash ⊢ ♯
10 5 cv ⊢ 𝑤
11 10 9 cfv ⊢ ( ♯ ‘ 𝑤 )
12 1 cv ⊢ 𝑛
13 caddc ⊢ +
14 c1 ⊢ 1
15 12 14 13 co ⊢ ( 𝑛 + 1 )
16 11 15 wceq ⊢ ( ♯ ‘ 𝑤 ) = ( 𝑛 + 1 )
17 16 5 8 crab ⊢ { 𝑤 ∈ ( WWalks ‘ 𝑔 ) ∣ ( ♯ ‘ 𝑤 ) = ( 𝑛 + 1 ) }
18 1 3 2 4 17 cmpo ⊢ ( 𝑛 ∈ ℕ0 , 𝑔 ∈ V ↦ { 𝑤 ∈ ( WWalks ‘ 𝑔 ) ∣ ( ♯ ‘ 𝑤 ) = ( 𝑛 + 1 ) } )
19 0 18 wceq ⊢ WWalksN = ( 𝑛 ∈ ℕ0 , 𝑔 ∈ V ↦ { 𝑤 ∈ ( WWalks ‘ 𝑔 ) ∣ ( ♯ ‘ 𝑤 ) = ( 𝑛 + 1 ) } )