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

Metamath Proof Explorer

Definition df-clwwlkn

Description: Define the set of all closed walks of a fixed length n as words over the set of vertices in a graph g . If 0 < n , 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 . For n = 0 , the set is empty, see clwwlkn0 . (Contributed by Alexander van der Vekens, 20-Mar-2018) (Revised by AV, 24-Apr-2021) (Revised by AV, 22-Mar-2022)

Ref Expression
Assertion df-clwwlkn ClWWalksN = ( 𝑛 ∈ ℕ0 , 𝑔 ∈ V ↦ { 𝑤 ∈ ( ClWWalks ‘ 𝑔 ) ∣ ( ♯ ‘ 𝑤 ) = 𝑛 } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cclwwlkn ⊢ ClWWalksN
1 vn ⊢ 𝑛
2 cn0 ⊢ ℕ0
3 vg ⊢ 𝑔
4 cvv ⊢ V
5 vw ⊢ 𝑤
6 cclwwlk ⊢ ClWWalks
7 3 cv ⊢ 𝑔
8 7 6 cfv ⊢ ( ClWWalks ‘ 𝑔 )
9 chash ⊢ ♯
10 5 cv ⊢ 𝑤
11 10 9 cfv ⊢ ( ♯ ‘ 𝑤 )
12 1 cv ⊢ 𝑛
13 11 12 wceq ⊢ ( ♯ ‘ 𝑤 ) = 𝑛
14 13 5 8 crab ⊢ { 𝑤 ∈ ( ClWWalks ‘ 𝑔 ) ∣ ( ♯ ‘ 𝑤 ) = 𝑛 }
15 1 3 2 4 14 cmpo ⊢ ( 𝑛 ∈ ℕ0 , 𝑔 ∈ V ↦ { 𝑤 ∈ ( ClWWalks ‘ 𝑔 ) ∣ ( ♯ ‘ 𝑤 ) = 𝑛 } )
16 0 15 wceq ⊢ ClWWalksN = ( 𝑛 ∈ ℕ0 , 𝑔 ∈ V ↦ { 𝑤 ∈ ( ClWWalks ‘ 𝑔 ) ∣ ( ♯ ‘ 𝑤 ) = 𝑛 } )