This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∈ V , s ∈ ℕ 0 * ⟼ f | [˙ iEdg ⁡ g / i]˙ f ∈ Word dom ⁡ i ∧ ∀ k ∈ 1 ..^ f s ≤ i ⁡ f ⁡ k − 1 ∩ 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 ∈ 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 ≤
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 ∩ i ⁡ f ⁡ k
31 30 18 cfv class i ⁡ f ⁡ k − 1 ∩ i ⁡ f ⁡ k
32 21 31 22 wbr wff s ≤ i ⁡ f ⁡ k − 1 ∩ i ⁡ f ⁡ k
33 32 15 20 wral wff ∀ k ∈ 1 ..^ f s ≤ i ⁡ f ⁡ k − 1 ∩ i ⁡ f ⁡ k
34 14 33 wa wff f ∈ Word dom ⁡ i ∧ ∀ k ∈ 1 ..^ f s ≤ i ⁡ f ⁡ k − 1 ∩ i ⁡ f ⁡ k
35 34 9 8 wsbc wff [˙ iEdg ⁡ g / i]˙ f ∈ Word dom ⁡ i ∧ ∀ k ∈ 1 ..^ f s ≤ i ⁡ f ⁡ k − 1 ∩ i ⁡ f ⁡ k
36 35 5 cab class f | [˙ iEdg ⁡ g / i]˙ f ∈ Word dom ⁡ i ∧ ∀ k ∈ 1 ..^ f s ≤ i ⁡ f ⁡ k − 1 ∩ i ⁡ f ⁡ k
37 1 3 2 4 36 cmpo class g ∈ V , s ∈ ℕ 0 * ⟼ f | [˙ iEdg ⁡ g / i]˙ f ∈ Word dom ⁡ i ∧ ∀ k ∈ 1 ..^ f s ≤ i ⁡ f ⁡ k − 1 ∩ i ⁡ f ⁡ k
38 0 37 wceq wff EdgWalks = g ∈ V , s ∈ ℕ 0 * ⟼ f | [˙ iEdg ⁡ g / i]˙ f ∈ Word dom ⁡ i ∧ ∀ k ∈ 1 ..^ f s ≤ i ⁡ f ⁡ k − 1 ∩ i ⁡ f ⁡ k