Definition df-wlkson 27376

Description: Define the collection of walks with particular endpoints (in a hypergraph). The predicate 𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 can be read as "The pair ⟨𝐹, 𝑃⟩ represents a walk from vertex 𝐴 to vertex 𝐵 in a graph 𝐺", see also iswlkon 27433. This corresponds to the "x0-x(l)-walks", see Definition in [Bollobas] p. 5. (Contributed by Alexander van der Vekens and Mario Carneiro, 4-Oct-2017.) (Revised by AV, 28-Dec-2020.)

Assertion

Ref	Expression
df-wlkson	⊢ WalksOn = (𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(Walks‘𝑔)𝑝 ∧ (𝑝‘0) = 𝑎 ∧ (𝑝‘(♯‘𝑓)) = 𝑏)}))

Distinct variable groups:   𝑓,𝑔,𝑝   𝑎,𝑏,𝑓,𝑔,𝑝

Detailed syntax breakdown of Definition df-wlkson

Step	Hyp	Ref	Expression
1		cwlkson 27373	. 2 class WalksOn
2		vg	. . 3 setvar 𝑔
3		cvv 3494	. . 3 class V
4		va	. . . 4 setvar 𝑎
5		vb	. . . 4 setvar 𝑏
6	2	cv 1532	. . . . 5 class 𝑔
7		cvtx 26775	. . . . 5 class Vtx
8	6, 7	cfv 6349	. . . 4 class (Vtx‘𝑔)
9		vf	. . . . . . . 8 setvar 𝑓
10	9	cv 1532	. . . . . . 7 class 𝑓
11		vp	. . . . . . . 8 setvar 𝑝
12	11	cv 1532	. . . . . . 7 class 𝑝
13		cwlks 27372	. . . . . . . 8 class Walks
14	6, 13	cfv 6349	. . . . . . 7 class (Walks‘𝑔)
15	10, 12, 14	wbr 5058	. . . . . 6 wff 𝑓(Walks‘𝑔)𝑝
16		cc0 10531	. . . . . . . 8 class 0
17	16, 12	cfv 6349	. . . . . . 7 class (𝑝‘0)
18	4	cv 1532	. . . . . . 7 class 𝑎
19	17, 18	wceq 1533	. . . . . 6 wff (𝑝‘0) = 𝑎
20		chash 13684	. . . . . . . . 9 class ♯
21	10, 20	cfv 6349	. . . . . . . 8 class (♯‘𝑓)
22	21, 12	cfv 6349	. . . . . . 7 class (𝑝‘(♯‘𝑓))
23	5	cv 1532	. . . . . . 7 class 𝑏
24	22, 23	wceq 1533	. . . . . 6 wff (𝑝‘(♯‘𝑓)) = 𝑏
25	15, 19, 24	w3a 1083	. . . . 5 wff (𝑓(Walks‘𝑔)𝑝 ∧ (𝑝‘0) = 𝑎 ∧ (𝑝‘(♯‘𝑓)) = 𝑏)
26	25, 9, 11	copab 5120	. . . 4 class {⟨𝑓, 𝑝⟩ ∣ (𝑓(Walks‘𝑔)𝑝 ∧ (𝑝‘0) = 𝑎 ∧ (𝑝‘(♯‘𝑓)) = 𝑏)}
27	4, 5, 8, 8, 26	cmpo 7152	. . 3 class (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(Walks‘𝑔)𝑝 ∧ (𝑝‘0) = 𝑎 ∧ (𝑝‘(♯‘𝑓)) = 𝑏)})
28	2, 3, 27	cmpt 5138	. 2 class (𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(Walks‘𝑔)𝑝 ∧ (𝑝‘0) = 𝑎 ∧ (𝑝‘(♯‘𝑓)) = 𝑏)}))
29	1, 28	wceq 1533	1 wff WalksOn = (𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(Walks‘𝑔)𝑝 ∧ (𝑝‘0) = 𝑎 ∧ (𝑝‘(♯‘𝑓)) = 𝑏)}))

This definition is referenced by:  wlkson  27432  wlkonprop  27434