Definition df-ewlks 26494

Description: Define the set of all s-walks of edges (in a hypergraph) corresponding to s-walks "on the edge level" discussed in Aksoy et al. For an extended nonnegative integer s, an s-walk is a sequence of hyperedges, e(0), e(1), ... , e(k), where e(j-1) and e(j) have at least s vertices in common (for j=1, ... , k). In contrast to the definition in Aksoy et al., s = 0 (a 0-walk is an arbitrary sequence of hyperedges) and s = +oo (then the number of common vertices of two adjacent hyperedges must be infinite) are allowed. Furthermore, it is not forbidden that adjacent hyperedges are equal. (Contributed by AV, 4-Jan-2021.)

Assertion

Ref	Expression
df-ewlks	|- EdgWalks = ( g e. _V , s e. NN0* |-> { f | [. (iEdg ` g ) / i ]. ( f e. Word dom i /\ A. k e. ( 1..^ ( # ` f ) ) s <_ ( # ` ( ( i ` ( f ` ( k - 1 ) ) ) i^i ( i ` ( f ` k ) ) ) ) ) } )

Distinct variable group:   f, g, i, k, s

Detailed syntax breakdown of Definition df-ewlks

Step	Hyp	Ref	Expression
1		cewlks 26491	. 2 class EdgWalks
2		vg	. . 3 setvar g
3		vs	. . 3 setvar s
4		cvv 3200	. . 3 class _V
5		cxnn0 11363	. . 3 class NN0*
6		vf	. . . . . . . 8 setvar f
7	6	cv 1482	. . . . . . 7 class f
8		vi	. . . . . . . . . 10 setvar i
9	8	cv 1482	. . . . . . . . 9 class i
10	9	cdm 5114	. . . . . . . 8 class dom i
11	10	cword 13291	. . . . . . 7 class Word dom i
12	7, 11	wcel 1990	. . . . . 6 wff f e. Word dom i
13	3	cv 1482	. . . . . . . 8 class s
14		vk	. . . . . . . . . . . . . 14 setvar k
15	14	cv 1482	. . . . . . . . . . . . 13 class k
16		c1 9937	. . . . . . . . . . . . 13 class 1
17		cmin 10266	. . . . . . . . . . . . 13 class -
18	15, 16, 17	co 6650	. . . . . . . . . . . 12 class ( k - 1 )
19	18, 7	cfv 5888	. . . . . . . . . . 11 class ( f ` ( k - 1 ) )
20	19, 9	cfv 5888	. . . . . . . . . 10 class ( i ` ( f ` ( k - 1 ) ) )
21	15, 7	cfv 5888	. . . . . . . . . . 11 class ( f ` k )
22	21, 9	cfv 5888	. . . . . . . . . 10 class ( i ` ( f ` k ) )
23	20, 22	cin 3573	. . . . . . . . 9 class ( ( i ` ( f ` ( k - 1 ) ) ) i^i ( i ` ( f ` k ) ) )
24		chash 13117	. . . . . . . . 9 class #
25	23, 24	cfv 5888	. . . . . . . 8 class ( # ` ( ( i ` ( f ` ( k - 1 ) ) ) i^i ( i ` ( f ` k ) ) ) )
26		cle 10075	. . . . . . . 8 class <_
27	13, 25, 26	wbr 4653	. . . . . . 7 wff s <_ ( # ` ( ( i ` ( f ` ( k - 1 ) ) ) i^i ( i ` ( f ` k ) ) ) )
28	7, 24	cfv 5888	. . . . . . . 8 class ( # ` f )
29		cfzo 12465	. . . . . . . 8 class ..^
30	16, 28, 29	co 6650	. . . . . . 7 class ( 1..^ ( # ` f ) )
31	27, 14, 30	wral 2912	. . . . . 6 wff A. k e. ( 1..^ ( # ` f ) ) s <_ ( # ` ( ( i ` ( f ` ( k - 1 ) ) ) i^i ( i ` ( f ` k ) ) ) )
32	12, 31	wa 384	. . . . 5 wff ( f e. Word dom i /\ A. k e. ( 1..^ ( # ` f ) ) s <_ ( # ` ( ( i ` ( f ` ( k - 1 ) ) ) i^i ( i ` ( f ` k ) ) ) ) )
33	2	cv 1482	. . . . . 6 class g
34		ciedg 25875	. . . . . 6 class iEdg
35	33, 34	cfv 5888	. . . . 5 class (iEdg ` g )
36	32, 8, 35	wsbc 3435	. . . 4 wff [. (iEdg ` g ) / i ]. ( f e. Word dom i /\ A. k e. ( 1..^ ( # ` f ) ) s <_ ( # ` ( ( i ` ( f ` ( k - 1 ) ) ) i^i ( i ` ( f ` k ) ) ) ) )
37	36, 6	cab 2608	. . 3 class { f | [. (iEdg ` g ) / i ]. ( f e. Word dom i /\ A. k e. ( 1..^ ( # ` f ) ) s <_ ( # ` ( ( i ` ( f ` ( k - 1 ) ) ) i^i ( i ` ( f ` k ) ) ) ) ) }
38	2, 3, 4, 5, 37	cmpt2 6652	. 2 class ( g e. _V , s e. NN0* |-> { f | [. (iEdg ` g ) / i ]. ( f e. Word dom i /\ A. k e. ( 1..^ ( # ` f ) ) s <_ ( # ` ( ( i ` ( f ` ( k - 1 ) ) ) i^i ( i ` ( f ` k ) ) ) ) ) } )
39	1, 38	wceq 1483	1 wff EdgWalks = ( g e. _V , s e. NN0* |-> { f | [. (iEdg ` g ) / i ]. ( f e. Word dom i /\ A. k e. ( 1..^ ( # ` f ) ) s <_ ( # ` ( ( i ` ( f ` ( k - 1 ) ) ) i^i ( i ` ( f ` k ) ) ) ) ) } )

This definition is referenced by:  ewlksfval  26497  ewlkprop  26499