Definition df-ewlks 27993

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 27990	. 2 class EdgWalks
2		vg	. . 3 setvar 𝑔
3		vs	. . 3 setvar 𝑠
4		cvv 3434	. . 3 class V
5		cxnn0 12333	. . 3 class ℕ0*
6		vf	. . . . . . . 8 setvar 𝑓
7	6	cv 1536	. . . . . . 7 class 𝑓
8		vi	. . . . . . . . . 10 setvar 𝑖
9	8	cv 1536	. . . . . . . . 9 class 𝑖
10	9	cdm 5591	. . . . . . . 8 class dom 𝑖
11	10	cword 14245	. . . . . . 7 class Word dom 𝑖
12	7, 11	wcel 2101	. . . . . 6 wff 𝑓 ∈ Word dom 𝑖
13	3	cv 1536	. . . . . . . 8 class 𝑠
14		vk	. . . . . . . . . . . . . 14 setvar 𝑘
15	14	cv 1536	. . . . . . . . . . . . 13 class 𝑘
16		c1 10900	. . . . . . . . . . . . 13 class 1
17		cmin 11233	. . . . . . . . . . . . 13 class −
18	15, 16, 17	co 7295	. . . . . . . . . . . 12 class (𝑘 − 1)
19	18, 7	cfv 6447	. . . . . . . . . . 11 class (𝑓‘(𝑘 − 1))
20	19, 9	cfv 6447	. . . . . . . . . 10 class (𝑖‘(𝑓‘(𝑘 − 1)))
21	15, 7	cfv 6447	. . . . . . . . . . 11 class (𝑓‘𝑘)
22	21, 9	cfv 6447	. . . . . . . . . 10 class (𝑖‘(𝑓‘𝑘))
23	20, 22	cin 3888	. . . . . . . . 9 class ((𝑖‘(𝑓‘(𝑘 − 1))) ∩ (𝑖‘(𝑓‘𝑘)))
24		chash 14072	. . . . . . . . 9 class ♯
25	23, 24	cfv 6447	. . . . . . . 8 class (♯‘((𝑖‘(𝑓‘(𝑘 − 1))) ∩ (𝑖‘(𝑓‘𝑘))))
26		cle 11038	. . . . . . . 8 class ≤
27	13, 25, 26	wbr 5077	. . . . . . 7 wff 𝑠 ≤ (♯‘((𝑖‘(𝑓‘(𝑘 − 1))) ∩ (𝑖‘(𝑓‘𝑘))))
28	7, 24	cfv 6447	. . . . . . . 8 class (♯‘𝑓)
29		cfzo 13410	. . . . . . . 8 class ..^
30	16, 28, 29	co 7295	. . . . . . 7 class (1..^(♯‘𝑓))
31	27, 14, 30	wral 3059	. . . . . 6 wff ∀𝑘 ∈ (1..^(♯‘𝑓))𝑠 ≤ (♯‘((𝑖‘(𝑓‘(𝑘 − 1))) ∩ (𝑖‘(𝑓‘𝑘))))
32	12, 31	wa 395	. . . . 5 wff (𝑓 ∈ Word dom 𝑖 ∧ ∀𝑘 ∈ (1..^(♯‘𝑓))𝑠 ≤ (♯‘((𝑖‘(𝑓‘(𝑘 − 1))) ∩ (𝑖‘(𝑓‘𝑘)))))
33	2	cv 1536	. . . . . 6 class 𝑔
34		ciedg 27395	. . . . . 6 class iEdg
35	33, 34	cfv 6447	. . . . 5 class (iEdg‘𝑔)
36	32, 8, 35	wsbc 3718	. . . 4 wff [(iEdg‘𝑔) / 𝑖](𝑓 ∈ Word dom 𝑖 ∧ ∀𝑘 ∈ (1..^(♯‘𝑓))𝑠 ≤ (♯‘((𝑖‘(𝑓‘(𝑘 − 1))) ∩ (𝑖‘(𝑓‘𝑘)))))
37	36, 6	cab 2710	. . 3 class {𝑓 ∣ [(iEdg‘𝑔) / 𝑖](𝑓 ∈ Word dom 𝑖 ∧ ∀𝑘 ∈ (1..^(♯‘𝑓))𝑠 ≤ (♯‘((𝑖‘(𝑓‘(𝑘 − 1))) ∩ (𝑖‘(𝑓‘𝑘)))))}
38	2, 3, 4, 5, 37	cmpo 7297	. 2 class (𝑔 ∈ V, 𝑠 ∈ ℕ0* ↦ {𝑓 ∣ [(iEdg‘𝑔) / 𝑖](𝑓 ∈ Word dom 𝑖 ∧ ∀𝑘 ∈ (1..^(♯‘𝑓))𝑠 ≤ (♯‘((𝑖‘(𝑓‘(𝑘 − 1))) ∩ (𝑖‘(𝑓‘𝑘)))))})
39	1, 38	wceq 1537	1 wff EdgWalks = (𝑔 ∈ V, 𝑠 ∈ ℕ0* ↦ {𝑓 ∣ [(iEdg‘𝑔) / 𝑖](𝑓 ∈ Word dom 𝑖 ∧ ∀𝑘 ∈ (1..^(♯‘𝑓))𝑠 ≤ (♯‘((𝑖‘(𝑓‘(𝑘 − 1))) ∩ (𝑖‘(𝑓‘𝑘)))))})

This definition is referenced by:  ewlksfval  27996  ewlkprop  27998