MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ewlks Structured version   Visualization version   GIF version

Definition df-ewlks 27307
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
StepHypRef Expression
1 cewlks 27304 . 2 class EdgWalks
2 vg . . 3 setvar 𝑔
3 vs . . 3 setvar 𝑠
4 cvv 3492 . . 3 class V
5 cxnn0 11955 . . 3 class 0*
6 vf . . . . . . . 8 setvar 𝑓
76cv 1527 . . . . . . 7 class 𝑓
8 vi . . . . . . . . . 10 setvar 𝑖
98cv 1527 . . . . . . . . 9 class 𝑖
109cdm 5548 . . . . . . . 8 class dom 𝑖
1110cword 13849 . . . . . . 7 class Word dom 𝑖
127, 11wcel 2105 . . . . . 6 wff 𝑓 ∈ Word dom 𝑖
133cv 1527 . . . . . . . 8 class 𝑠
14 vk . . . . . . . . . . . . . 14 setvar 𝑘
1514cv 1527 . . . . . . . . . . . . 13 class 𝑘
16 c1 10526 . . . . . . . . . . . . 13 class 1
17 cmin 10858 . . . . . . . . . . . . 13 class
1815, 16, 17co 7145 . . . . . . . . . . . 12 class (𝑘 − 1)
1918, 7cfv 6348 . . . . . . . . . . 11 class (𝑓‘(𝑘 − 1))
2019, 9cfv 6348 . . . . . . . . . 10 class (𝑖‘(𝑓‘(𝑘 − 1)))
2115, 7cfv 6348 . . . . . . . . . . 11 class (𝑓𝑘)
2221, 9cfv 6348 . . . . . . . . . 10 class (𝑖‘(𝑓𝑘))
2320, 22cin 3932 . . . . . . . . 9 class ((𝑖‘(𝑓‘(𝑘 − 1))) ∩ (𝑖‘(𝑓𝑘)))
24 chash 13678 . . . . . . . . 9 class
2523, 24cfv 6348 . . . . . . . 8 class (♯‘((𝑖‘(𝑓‘(𝑘 − 1))) ∩ (𝑖‘(𝑓𝑘))))
26 cle 10664 . . . . . . . 8 class
2713, 25, 26wbr 5057 . . . . . . 7 wff 𝑠 ≤ (♯‘((𝑖‘(𝑓‘(𝑘 − 1))) ∩ (𝑖‘(𝑓𝑘))))
287, 24cfv 6348 . . . . . . . 8 class (♯‘𝑓)
29 cfzo 13021 . . . . . . . 8 class ..^
3016, 28, 29co 7145 . . . . . . 7 class (1..^(♯‘𝑓))
3127, 14, 30wral 3135 . . . . . 6 wff 𝑘 ∈ (1..^(♯‘𝑓))𝑠 ≤ (♯‘((𝑖‘(𝑓‘(𝑘 − 1))) ∩ (𝑖‘(𝑓𝑘))))
3212, 31wa 396 . . . . 5 wff (𝑓 ∈ Word dom 𝑖 ∧ ∀𝑘 ∈ (1..^(♯‘𝑓))𝑠 ≤ (♯‘((𝑖‘(𝑓‘(𝑘 − 1))) ∩ (𝑖‘(𝑓𝑘)))))
332cv 1527 . . . . . 6 class 𝑔
34 ciedg 26709 . . . . . 6 class iEdg
3533, 34cfv 6348 . . . . 5 class (iEdg‘𝑔)
3632, 8, 35wsbc 3769 . . . 4 wff [(iEdg‘𝑔) / 𝑖](𝑓 ∈ Word dom 𝑖 ∧ ∀𝑘 ∈ (1..^(♯‘𝑓))𝑠 ≤ (♯‘((𝑖‘(𝑓‘(𝑘 − 1))) ∩ (𝑖‘(𝑓𝑘)))))
3736, 6cab 2796 . . 3 class {𝑓[(iEdg‘𝑔) / 𝑖](𝑓 ∈ Word dom 𝑖 ∧ ∀𝑘 ∈ (1..^(♯‘𝑓))𝑠 ≤ (♯‘((𝑖‘(𝑓‘(𝑘 − 1))) ∩ (𝑖‘(𝑓𝑘)))))}
382, 3, 4, 5, 37cmpo 7147 . 2 class (𝑔 ∈ V, 𝑠 ∈ ℕ0* ↦ {𝑓[(iEdg‘𝑔) / 𝑖](𝑓 ∈ Word dom 𝑖 ∧ ∀𝑘 ∈ (1..^(♯‘𝑓))𝑠 ≤ (♯‘((𝑖‘(𝑓‘(𝑘 − 1))) ∩ (𝑖‘(𝑓𝑘)))))})
391, 38wceq 1528 1 wff EdgWalks = (𝑔 ∈ V, 𝑠 ∈ ℕ0* ↦ {𝑓[(iEdg‘𝑔) / 𝑖](𝑓 ∈ Word dom 𝑖 ∧ ∀𝑘 ∈ (1..^(♯‘𝑓))𝑠 ≤ (♯‘((𝑖‘(𝑓‘(𝑘 − 1))) ∩ (𝑖‘(𝑓𝑘)))))})
Colors of variables: wff setvar class
This definition is referenced by:  ewlksfval  27310  ewlkprop  27312
  Copyright terms: Public domain W3C validator