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 \in V, s \in ℕ_{0}^{*} ⟼ \{f \| \underset{˙}{[} iEdg (g) / i \underset{˙}{]} (f \in Word dom i \land \forall k \in (1 ..^\|f\|) s \leq \|i (f (k - 1)) \cap i (f (k))\|)\})$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cewlks	$class EdgWalks$
1		vg	$setvar g$
2		cvv	$class V$
3		vs	$setvar s$
4		cxnn0	$class ℕ_{0}^{*}$
5		vf	$setvar f$
6		ciedg	$class iEdg$
7	1	cv	$setvar g$
8	7 6	cfv	$class iEdg (g)$
9		vi	$setvar i$
10	5	cv	$setvar f$
11	9	cv	$setvar i$
12	11	cdm	$class dom i$
13	12	cword	$class Word dom i$
14	10 13	wcel	$wff f \in Word dom i$
15		vk	$setvar k$
16		c1	$class 1$
17		cfzo	$class ..^$
18		chash	$class \|.\|$
19	10 18	cfv	$class \|f\|$
20	16 19 17	co	$class (1 ..^\|f\|)$
21	3	cv	$setvar s$
22		cle	$class \leq$
23	15	cv	$setvar k$
24		cmin	$class -$
25	23 16 24	co	$class (k - 1)$
26	25 10	cfv	$class f (k - 1)$
27	26 11	cfv	$class i (f (k - 1))$
28	23 10	cfv	$class f (k)$
29	28 11	cfv	$class i (f (k))$
30	27 29	cin	$class (i (f (k - 1)) \cap i (f (k)))$
31	30 18	cfv	$class \|i (f (k - 1)) \cap i (f (k))\|$
32	21 31 22	wbr	$wff s \leq \|i (f (k - 1)) \cap i (f (k))\|$
33	32 15 20	wral	$wff \forall k \in (1 ..^\|f\|) s \leq \|i (f (k - 1)) \cap i (f (k))\|$
34	14 33	wa	$wff (f \in Word dom i \land \forall k \in (1 ..^\|f\|) s \leq \|i (f (k - 1)) \cap i (f (k))\|)$
35	34 9 8	wsbc	$wff \underset{˙}{[} iEdg (g) / i \underset{˙}{]} (f \in Word dom i \land \forall k \in (1 ..^\|f\|) s \leq \|i (f (k - 1)) \cap i (f (k))\|)$
36	35 5	cab	$class \{f \| \underset{˙}{[} iEdg (g) / i \underset{˙}{]} (f \in Word dom i \land \forall k \in (1 ..^\|f\|) s \leq \|i (f (k - 1)) \cap i (f (k))\|)\}$
37	1 3 2 4 36	cmpo	$class (g \in V, s \in ℕ_{0}^{*} ⟼ \{f \| \underset{˙}{[} iEdg (g) / i \underset{˙}{]} (f \in Word dom i \land \forall k \in (1 ..^\|f\|) s \leq \|i (f (k - 1)) \cap i (f (k))\|)\})$
38	0 37	wceq	$wff EdgWalks = (g \in V, s \in ℕ_{0}^{*} ⟼ \{f \| \underset{˙}{[} iEdg (g) / i \underset{˙}{]} (f \in Word dom i \land \forall k \in (1 ..^\|f\|) s \leq \|i (f (k - 1)) \cap i (f (k))\|)\})$

Metamath Proof Explorer

Definition df-ewlks

Detailed syntax breakdown