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