Definition df-wlks 16025

Description: Define the set of all walks (in a hypergraph). Such walks correspond to the s-walks "on the vertex level" (with s = 1), and also to 1-walks "on the edge level" discussed in Aksoy et al. The predicate F (Walks ` G ) P can be read as "The pair <. F , P >. represents a walk in a graph G", see also iswlk 16029.

The condition { ( p ` k ) , ( p ` ( k + 1 ) ) } C_ ( (iEdg ` g ) ` ( f ` k ) ) (hereinafter referred to as C) would not be sufficient, because the repetition of a vertex in a walk (i.e. ( p ` k ) = ( p ` ( k + 1 ) ) should be allowed only if there is a loop at ( p ` k ). Otherwise, C would be fulfilled by each edge containing ( p ` k ).

According to the definition of [Bollobas] p. 4.: "A walk W in a graph is an alternating sequence of vertices and edges x0 , e1 , x1 , e2 , ... , e(l) , x(l) ...", a walk can be represented by two mappings f from { 1 , ... , n } and p from { 0 , ... , n }, where f enumerates the (indices of the) edges, and p enumerates the vertices. So the walk is represented by the following sequence: p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n). (Contributed by AV, 30-Dec-2020.)

Assertion

Ref	Expression
df-wlks	|- Walks = ( g e. _V |-> { <. f , p >. | ( f e. Word dom (iEdg ` g ) /\ p : ( 0 ... (♯ ` f ) ) --> (Vtx ` g ) /\ A. k e. ( 0..^ (♯ ` f ) )if- ( ( p ` k ) = ( p ` ( k + 1 ) ) , ( (iEdg ` g ) ` ( f ` k ) ) = { ( p ` k ) } , { ( p ` k ) , ( p ` ( k + 1 ) ) } C_ ( (iEdg ` g ) ` ( f ` k ) ) ) ) } )

Distinct variable group:   f, g, k, p

Detailed syntax breakdown of Definition df-wlks

Step	Hyp	Ref	Expression
1		cwlks 16024	. 2 class Walks
2		vg	. . 3 setvar g
3		cvv 2799	. . 3 class _V
4		vf	. . . . . . 7 setvar f
5	4	cv 1394	. . . . . 6 class f
6	2	cv 1394	. . . . . . . . 9 class g
7		ciedg 15808	. . . . . . . . 9 class iEdg
8	6, 7	cfv 5317	. . . . . . . 8 class (iEdg ` g )
9	8	cdm 4718	. . . . . . 7 class dom (iEdg ` g )
10	9	cword 11066	. . . . . 6 class Word dom (iEdg ` g )
11	5, 10	wcel 2200	. . . . 5 wff f e. Word dom (iEdg ` g )
12		cc0 7995	. . . . . . 7 class 0
13		chash 10992	. . . . . . . 8 class ♯
14	5, 13	cfv 5317	. . . . . . 7 class (♯ ` f )
15		cfz 10200	. . . . . . 7 class ...
16	12, 14, 15	co 6000	. . . . . 6 class ( 0 ... (♯ ` f ) )
17		cvtx 15807	. . . . . . 7 class Vtx
18	6, 17	cfv 5317	. . . . . 6 class (Vtx ` g )
19		vp	. . . . . . 7 setvar p
20	19	cv 1394	. . . . . 6 class p
21	16, 18, 20	wf 5313	. . . . 5 wff p : ( 0 ... (♯ ` f ) ) --> (Vtx ` g )
22		vk	. . . . . . . . . 10 setvar k
23	22	cv 1394	. . . . . . . . 9 class k
24	23, 20	cfv 5317	. . . . . . . 8 class ( p ` k )
25		c1 7996	. . . . . . . . . 10 class 1
26		caddc 7998	. . . . . . . . . 10 class +
27	23, 25, 26	co 6000	. . . . . . . . 9 class ( k + 1 )
28	27, 20	cfv 5317	. . . . . . . 8 class ( p ` ( k + 1 ) )
29	24, 28	wceq 1395	. . . . . . 7 wff ( p ` k ) = ( p ` ( k + 1 ) )
30	23, 5	cfv 5317	. . . . . . . . 9 class ( f ` k )
31	30, 8	cfv 5317	. . . . . . . 8 class ( (iEdg ` g ) ` ( f ` k ) )
32	24	csn 3666	. . . . . . . 8 class { ( p ` k ) }
33	31, 32	wceq 1395	. . . . . . 7 wff ( (iEdg ` g ) ` ( f ` k ) ) = { ( p ` k ) }
34	24, 28	cpr 3667	. . . . . . . 8 class { ( p ` k ) , ( p ` ( k + 1 ) ) }
35	34, 31	wss 3197	. . . . . . 7 wff { ( p ` k ) , ( p ` ( k + 1 ) ) } C_ ( (iEdg ` g ) ` ( f ` k ) )
36	29, 33, 35	wif 983	. . . . . 6 wff if- ( ( p ` k ) = ( p ` ( k + 1 ) ) , ( (iEdg ` g ) ` ( f ` k ) ) = { ( p ` k ) } , { ( p ` k ) , ( p ` ( k + 1 ) ) } C_ ( (iEdg ` g ) ` ( f ` k ) ) )
37		cfzo 10334	. . . . . . 7 class ..^
38	12, 14, 37	co 6000	. . . . . 6 class ( 0..^ (♯ ` f ) )
39	36, 22, 38	wral 2508	. . . . 5 wff A. k e. ( 0..^ (♯ ` f ) )if- ( ( p ` k ) = ( p ` ( k + 1 ) ) , ( (iEdg ` g ) ` ( f ` k ) ) = { ( p ` k ) } , { ( p ` k ) , ( p ` ( k + 1 ) ) } C_ ( (iEdg ` g ) ` ( f ` k ) ) )
40	11, 21, 39	w3a 1002	. . . 4 wff ( f e. Word dom (iEdg ` g ) /\ p : ( 0 ... (♯ ` f ) ) --> (Vtx ` g ) /\ A. k e. ( 0..^ (♯ ` f ) )if- ( ( p ` k ) = ( p ` ( k + 1 ) ) , ( (iEdg ` g ) ` ( f ` k ) ) = { ( p ` k ) } , { ( p ` k ) , ( p ` ( k + 1 ) ) } C_ ( (iEdg ` g ) ` ( f ` k ) ) ) )
41	40, 4, 19	copab 4143	. . 3 class { <. f , p >. | ( f e. Word dom (iEdg ` g ) /\ p : ( 0 ... (♯ ` f ) ) --> (Vtx ` g ) /\ A. k e. ( 0..^ (♯ ` f ) )if- ( ( p ` k ) = ( p ` ( k + 1 ) ) , ( (iEdg ` g ) ` ( f ` k ) ) = { ( p ` k ) } , { ( p ` k ) , ( p ` ( k + 1 ) ) } C_ ( (iEdg ` g ) ` ( f ` k ) ) ) ) }
42	2, 3, 41	cmpt 4144	. 2 class ( g e. _V |-> { <. f , p >. | ( f e. Word dom (iEdg ` g ) /\ p : ( 0 ... (♯ ` f ) ) --> (Vtx ` g ) /\ A. k e. ( 0..^ (♯ ` f ) )if- ( ( p ` k ) = ( p ` ( k + 1 ) ) , ( (iEdg ` g ) ` ( f ` k ) ) = { ( p ` k ) } , { ( p ` k ) , ( p ` ( k + 1 ) ) } C_ ( (iEdg ` g ) ` ( f ` k ) ) ) ) } )
43	1, 42	wceq 1395	1 wff Walks = ( g e. _V |-> { <. f , p >. | ( f e. Word dom (iEdg ` g ) /\ p : ( 0 ... (♯ ` f ) ) --> (Vtx ` g ) /\ A. k e. ( 0..^ (♯ ` f ) )if- ( ( p ` k ) = ( p ` ( k + 1 ) ) , ( (iEdg ` g ) ` ( f ` k ) ) = { ( p ` k ) } , { ( p ` k ) , ( p ` ( k + 1 ) ) } C_ ( (iEdg ` g ) ` ( f ` k ) ) ) ) } )

This definition is referenced by:  wksfval  16028