Definition df-ewlks

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)

	Ref	Expression
Assertion	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 ) ) ) ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cewlks	|- EdgWalks
1		vg	|- g
2		cvv	|- _V
3		vs	|- s
4		cxnn0	|- NN0*
5		vf	|- f
6		ciedg	|- iEdg
7	1	cv	|- g
8	7 6	cfv	|- ( iEdg ` g )
9		vi	|- i
10	5	cv	|- f
11	9	cv	|- i
12	11	cdm	|- dom i
13	12	cword	|- Word dom i
14	10 13	wcel	|- f e. Word dom i
15		vk	|- k
16		c1	|- 1
17		cfzo	|- ..^
18		chash	|- #
19	10 18	cfv	|- ( # ` f )
20	16 19 17	co	|- ( 1 ..^ ( # ` f ) )
21	3	cv	|- s
22		cle	|- <_
23	15	cv	|- k
24		cmin	|- -
25	23 16 24	co	|- ( k - 1 )
26	25 10	cfv	|- ( f ` ( k - 1 ) )
27	26 11	cfv	|- ( i ` ( f ` ( k - 1 ) ) )
28	23 10	cfv	|- ( f ` k )
29	28 11	cfv	|- ( i ` ( f ` k ) )
30	27 29	cin	|- ( ( i ` ( f ` ( k - 1 ) ) ) i^i ( i ` ( f ` k ) ) )
31	30 18	cfv	|- ( # ` ( ( i ` ( f ` ( k - 1 ) ) ) i^i ( i ` ( f ` k ) ) ) )
32	21 31 22	wbr	|- s <_ ( # ` ( ( i ` ( f ` ( k - 1 ) ) ) i^i ( i ` ( f ` k ) ) ) )
33	32 15 20	wral	|- A. k e. ( 1 ..^ ( # ` f ) ) s <_ ( # ` ( ( i ` ( f ` ( k - 1 ) ) ) i^i ( i ` ( f ` k ) ) ) )
34	14 33	wa	|- ( f e. Word dom i /\ A. k e. ( 1 ..^ ( # ` f ) ) s <_ ( # ` ( ( i ` ( f ` ( k - 1 ) ) ) i^i ( i ` ( f ` k ) ) ) ) )
35	34 9 8	wsbc	|- [. ( iEdg ` g ) / i ]. ( f e. Word dom i /\ A. k e. ( 1 ..^ ( # ` f ) ) s <_ ( # ` ( ( i ` ( f ` ( k - 1 ) ) ) i^i ( i ` ( f ` k ) ) ) ) )
36	35 5	cab	|- { f | [. ( iEdg ` g ) / i ]. ( f e. Word dom i /\ A. k e. ( 1 ..^ ( # ` f ) ) s <_ ( # ` ( ( i ` ( f ` ( k - 1 ) ) ) i^i ( i ` ( f ` k ) ) ) ) ) }
37	1 3 2 4 36	cmpo	|- ( 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 ) ) ) ) ) } )
38	0 37	wceq	|- 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 ) ) ) ) ) } )