Definition df-ewlks 29524

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., 𝑠 = 0 (a 0-walk is an arbitrary sequence of hyperedges) and 𝑠 = +∞ (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 = (𝑔 ∈ V, 𝑠 ∈ ℕ0* ↦ {𝑓 ∣ [(iEdg‘𝑔) / 𝑖](𝑓 ∈ Word dom 𝑖 ∧ ∀𝑘 ∈ (1..^(♯‘𝑓))𝑠 ≤ (♯‘((𝑖‘(𝑓‘(𝑘 − 1))) ∩ (𝑖‘(𝑓‘𝑘)))))})

Distinct variable group:   𝑓,𝑔,𝑖,𝑘,𝑠

Detailed syntax breakdown of Definition df-ewlks

Step	Hyp	Ref	Expression
1		cewlks 29521	. 2 class EdgWalks
2		vg	. . 3 setvar 𝑔
3		vs	. . 3 setvar 𝑠
4		cvv 3459	. . 3 class V
5		cxnn0 12572	. . 3 class ℕ0*
6		vf	. . . . . . . 8 setvar 𝑓
7	6	cv 1539	. . . . . . 7 class 𝑓
8		vi	. . . . . . . . . 10 setvar 𝑖
9	8	cv 1539	. . . . . . . . 9 class 𝑖
10	9	cdm 5654	. . . . . . . 8 class dom 𝑖
11	10	cword 14529	. . . . . . 7 class Word dom 𝑖
12	7, 11	wcel 2108	. . . . . 6 wff 𝑓 ∈ Word dom 𝑖
13	3	cv 1539	. . . . . . . 8 class 𝑠
14		vk	. . . . . . . . . . . . . 14 setvar 𝑘
15	14	cv 1539	. . . . . . . . . . . . 13 class 𝑘
16		c1 11128	. . . . . . . . . . . . 13 class 1
17		cmin 11464	. . . . . . . . . . . . 13 class −
18	15, 16, 17	co 7403	. . . . . . . . . . . 12 class (𝑘 − 1)
19	18, 7	cfv 6530	. . . . . . . . . . 11 class (𝑓‘(𝑘 − 1))
20	19, 9	cfv 6530	. . . . . . . . . 10 class (𝑖‘(𝑓‘(𝑘 − 1)))
21	15, 7	cfv 6530	. . . . . . . . . . 11 class (𝑓‘𝑘)
22	21, 9	cfv 6530	. . . . . . . . . 10 class (𝑖‘(𝑓‘𝑘))
23	20, 22	cin 3925	. . . . . . . . 9 class ((𝑖‘(𝑓‘(𝑘 − 1))) ∩ (𝑖‘(𝑓‘𝑘)))
24		chash 14346	. . . . . . . . 9 class ♯
25	23, 24	cfv 6530	. . . . . . . 8 class (♯‘((𝑖‘(𝑓‘(𝑘 − 1))) ∩ (𝑖‘(𝑓‘𝑘))))
26		cle 11268	. . . . . . . 8 class ≤
27	13, 25, 26	wbr 5119	. . . . . . 7 wff 𝑠 ≤ (♯‘((𝑖‘(𝑓‘(𝑘 − 1))) ∩ (𝑖‘(𝑓‘𝑘))))
28	7, 24	cfv 6530	. . . . . . . 8 class (♯‘𝑓)
29		cfzo 13669	. . . . . . . 8 class ..^
30	16, 28, 29	co 7403	. . . . . . 7 class (1..^(♯‘𝑓))
31	27, 14, 30	wral 3051	. . . . . 6 wff ∀𝑘 ∈ (1..^(♯‘𝑓))𝑠 ≤ (♯‘((𝑖‘(𝑓‘(𝑘 − 1))) ∩ (𝑖‘(𝑓‘𝑘))))
32	12, 31	wa 395	. . . . 5 wff (𝑓 ∈ Word dom 𝑖 ∧ ∀𝑘 ∈ (1..^(♯‘𝑓))𝑠 ≤ (♯‘((𝑖‘(𝑓‘(𝑘 − 1))) ∩ (𝑖‘(𝑓‘𝑘)))))
33	2	cv 1539	. . . . . 6 class 𝑔
34		ciedg 28922	. . . . . 6 class iEdg
35	33, 34	cfv 6530	. . . . 5 class (iEdg‘𝑔)
36	32, 8, 35	wsbc 3765	. . . 4 wff [(iEdg‘𝑔) / 𝑖](𝑓 ∈ Word dom 𝑖 ∧ ∀𝑘 ∈ (1..^(♯‘𝑓))𝑠 ≤ (♯‘((𝑖‘(𝑓‘(𝑘 − 1))) ∩ (𝑖‘(𝑓‘𝑘)))))
37	36, 6	cab 2713	. . 3 class {𝑓 ∣ [(iEdg‘𝑔) / 𝑖](𝑓 ∈ Word dom 𝑖 ∧ ∀𝑘 ∈ (1..^(♯‘𝑓))𝑠 ≤ (♯‘((𝑖‘(𝑓‘(𝑘 − 1))) ∩ (𝑖‘(𝑓‘𝑘)))))}
38	2, 3, 4, 5, 37	cmpo 7405	. 2 class (𝑔 ∈ V, 𝑠 ∈ ℕ0* ↦ {𝑓 ∣ [(iEdg‘𝑔) / 𝑖](𝑓 ∈ Word dom 𝑖 ∧ ∀𝑘 ∈ (1..^(♯‘𝑓))𝑠 ≤ (♯‘((𝑖‘(𝑓‘(𝑘 − 1))) ∩ (𝑖‘(𝑓‘𝑘)))))})
39	1, 38	wceq 1540	1 wff EdgWalks = (𝑔 ∈ V, 𝑠 ∈ ℕ0* ↦ {𝑓 ∣ [(iEdg‘𝑔) / 𝑖](𝑓 ∈ Word dom 𝑖 ∧ ∀𝑘 ∈ (1..^(♯‘𝑓))𝑠 ≤ (♯‘((𝑖‘(𝑓‘(𝑘 − 1))) ∩ (𝑖‘(𝑓‘𝑘)))))})

This definition is referenced by:  ewlksfval  29527  ewlkprop  29529