Definition df-upwlks 42243

Description: Define the set of all walks (in a pseudograph), called "simple walks" in the following.

According to Wikipedia ("Path (graph theory)", https://en.wikipedia.org/wiki/Path_(graph_theory), 3-Oct-2017): "A walk of length k in a graph is an alternating sequence of vertices and edges, v0 , e0 , v1 , e1 , v2 , ... , v(k-1) , e(k-1) , v(k) which begins and ends with vertices. If the graph is undirected, then the endpoints of e(i) are v(i) and v(i+1)."

According to Bollobas: " A walk W in a graph is an alternating sequence of vertices and edges x0 , e1 , x1 , e2 , ... , e(l) , x(l) where e(i) = x(i-1)x(i), 0<i<=l.", see Definition of [Bollobas] p. 4.

Therefore, a walk can be represented by two mappings f from { 1 , ... , n } and p from { 0 , ... , n }, where f enumerates the (indices of the) edges, and p enumerates the vertices. So the walk is represented by the following sequence: p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n).

Although this definition is also applicable for arbitrary hypergraphs, it allows only walks consisting of not proper hyperedges (i.e. edges connecting at most two vertices). Therefore, it should be used for pseudograhs only. (Contributed by Alexander van der Vekens and Mario Carneiro, 4-Oct-2017.) (Revised by AV, 28-Dec-2020.)

Assertion

Ref	Expression
df-upwlks	⊢ UPWalks = (𝑔 ∈ V ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓 ∈ Word dom (iEdg‘𝑔) ∧ 𝑝:(0...(♯‘𝑓))⟶(Vtx‘𝑔) ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})})

Distinct variable group:   𝑓,𝑔,𝑘,𝑝

Detailed syntax breakdown of Definition df-upwlks

Step	Hyp	Ref	Expression
1		cupwlks 42242	. 2 class UPWalks
2		vg	. . 3 setvar 𝑔
3		cvv 3340	. . 3 class V
4		vf	. . . . . . 7 setvar 𝑓
5	4	cv 1631	. . . . . 6 class 𝑓
6	2	cv 1631	. . . . . . . . 9 class 𝑔
7		ciedg 26095	. . . . . . . . 9 class iEdg
8	6, 7	cfv 6049	. . . . . . . 8 class (iEdg‘𝑔)
9	8	cdm 5266	. . . . . . 7 class dom (iEdg‘𝑔)
10	9	cword 13497	. . . . . 6 class Word dom (iEdg‘𝑔)
11	5, 10	wcel 2139	. . . . 5 wff 𝑓 ∈ Word dom (iEdg‘𝑔)
12		cc0 10148	. . . . . . 7 class 0
13		chash 13331	. . . . . . . 8 class ♯
14	5, 13	cfv 6049	. . . . . . 7 class (♯‘𝑓)
15		cfz 12539	. . . . . . 7 class ...
16	12, 14, 15	co 6814	. . . . . 6 class (0...(♯‘𝑓))
17		cvtx 26094	. . . . . . 7 class Vtx
18	6, 17	cfv 6049	. . . . . 6 class (Vtx‘𝑔)
19		vp	. . . . . . 7 setvar 𝑝
20	19	cv 1631	. . . . . 6 class 𝑝
21	16, 18, 20	wf 6045	. . . . 5 wff 𝑝:(0...(♯‘𝑓))⟶(Vtx‘𝑔)
22		vk	. . . . . . . . . 10 setvar 𝑘
23	22	cv 1631	. . . . . . . . 9 class 𝑘
24	23, 5	cfv 6049	. . . . . . . 8 class (𝑓‘𝑘)
25	24, 8	cfv 6049	. . . . . . 7 class ((iEdg‘𝑔)‘(𝑓‘𝑘))
26	23, 20	cfv 6049	. . . . . . . 8 class (𝑝‘𝑘)
27		c1 10149	. . . . . . . . . 10 class 1
28		caddc 10151	. . . . . . . . . 10 class +
29	23, 27, 28	co 6814	. . . . . . . . 9 class (𝑘 + 1)
30	29, 20	cfv 6049	. . . . . . . 8 class (𝑝‘(𝑘 + 1))
31	26, 30	cpr 4323	. . . . . . 7 class {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))}
32	25, 31	wceq 1632	. . . . . 6 wff ((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))}
33		cfzo 12679	. . . . . . 7 class ..^
34	12, 14, 33	co 6814	. . . . . 6 class (0..^(♯‘𝑓))
35	32, 22, 34	wral 3050	. . . . 5 wff ∀𝑘 ∈ (0..^(♯‘𝑓))((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))}
36	11, 21, 35	w3a 1072	. . . 4 wff (𝑓 ∈ Word dom (iEdg‘𝑔) ∧ 𝑝:(0...(♯‘𝑓))⟶(Vtx‘𝑔) ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})
37	36, 4, 19	copab 4864	. . 3 class {⟨𝑓, 𝑝⟩ ∣ (𝑓 ∈ Word dom (iEdg‘𝑔) ∧ 𝑝:(0...(♯‘𝑓))⟶(Vtx‘𝑔) ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})}
38	2, 3, 37	cmpt 4881	. 2 class (𝑔 ∈ V ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓 ∈ Word dom (iEdg‘𝑔) ∧ 𝑝:(0...(♯‘𝑓))⟶(Vtx‘𝑔) ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})})
39	1, 38	wceq 1632	1 wff UPWalks = (𝑔 ∈ V ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓 ∈ Word dom (iEdg‘𝑔) ∧ 𝑝:(0...(♯‘𝑓))⟶(Vtx‘𝑔) ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})})

This definition is referenced by:  upwlksfval  42244