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 ) } )