Definition df-upwlks 48927

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 pseudographs 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 48926	. 2 class UPWalks
2		vg	. . 3 setvar 𝑔
3		cvv 3455	. . 3 class V
4		vf	. . . . . . 7 setvar 𝑓
5	4	cv 1569	. . . . . 6 class 𝑓
6	2	cv 1569	. . . . . . . . 9 class 𝑔
7		ciedg 29356	. . . . . . . . 9 class iEdg
8	6, 7	cfv 6536	. . . . . . . 8 class (iEdg‘𝑔)
9	8	cdm 5661	. . . . . . 7 class dom (iEdg‘𝑔)
10	9	cword 14555	. . . . . 6 class Word dom (iEdg‘𝑔)
11	5, 10	wcel 2143	. . . . 5 wff 𝑓 ∈ Word dom (iEdg‘𝑔)
12		cc0 11104	. . . . . . 7 class 0
13		chash 14371	. . . . . . . 8 class ♯
14	5, 13	cfv 6536	. . . . . . 7 class (♯‘𝑓)
15		cfz 13539	. . . . . . 7 class ...
16	12, 14, 15	co 7410	. . . . . 6 class (0...(♯‘𝑓))
17		cvtx 29355	. . . . . . 7 class Vtx
18	6, 17	cfv 6536	. . . . . 6 class (Vtx‘𝑔)
19		vp	. . . . . . 7 setvar 𝑝
20	19	cv 1569	. . . . . 6 class 𝑝
21	16, 18, 20	wf 6532	. . . . 5 wff 𝑝:(0...(♯‘𝑓))⟶(Vtx‘𝑔)
22		vk	. . . . . . . . . 10 setvar 𝑘
23	22	cv 1569	. . . . . . . . 9 class 𝑘
24	23, 5	cfv 6536	. . . . . . . 8 class (𝑓‘𝑘)
25	24, 8	cfv 6536	. . . . . . 7 class ((iEdg‘𝑔)‘(𝑓‘𝑘))
26	23, 20	cfv 6536	. . . . . . . 8 class (𝑝‘𝑘)
27		c1 11105	. . . . . . . . . 10 class 1
28		caddc 11107	. . . . . . . . . 10 class +
29	23, 27, 28	co 7410	. . . . . . . . 9 class (𝑘 + 1)
30	29, 20	cfv 6536	. . . . . . . 8 class (𝑝‘(𝑘 + 1))
31	26, 30	cpr 4591	. . . . . . 7 class {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))}
32	25, 31	wceq 1570	. . . . . 6 wff ((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))}
33		cfzo 13687	. . . . . . 7 class ..^
34	12, 14, 33	co 7410	. . . . . 6 class (0..^(♯‘𝑓))
35	32, 22, 34	wral 3079	. . . . 5 wff ∀𝑘 ∈ (0..^(♯‘𝑓))((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))}
36	11, 21, 35	w3a 1103	. . . 4 wff (𝑓 ∈ Word dom (iEdg‘𝑔) ∧ 𝑝:(0...(♯‘𝑓))⟶(Vtx‘𝑔) ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})
37	36, 4, 19	copab 5173	. . 3 class {⟨𝑓, 𝑝⟩ ∣ (𝑓 ∈ Word dom (iEdg‘𝑔) ∧ 𝑝:(0...(♯‘𝑓))⟶(Vtx‘𝑔) ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})}
38	2, 3, 37	cmpt 5192	. 2 class (𝑔 ∈ V ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓 ∈ Word dom (iEdg‘𝑔) ∧ 𝑝:(0...(♯‘𝑓))⟶(Vtx‘𝑔) ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})})
39	1, 38	wceq 1570	1 wff UPWalks = (𝑔 ∈ V ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓 ∈ Word dom (iEdg‘𝑔) ∧ 𝑝:(0...(♯‘𝑓))⟶(Vtx‘𝑔) ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})})

This definition is used by:  upwlksfval  48928