Definition df-wlkson 26496

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 26553. 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 26493	. 2 class WalksOn
2		vg	. . 3 setvar 𝑔
3		cvv 3200	. . 3 class V
4		va	. . . 4 setvar 𝑎
5		vb	. . . 4 setvar 𝑏
6	2	cv 1482	. . . . 5 class 𝑔
7		cvtx 25874	. . . . 5 class Vtx
8	6, 7	cfv 5888	. . . 4 class (Vtx‘𝑔)
9		vf	. . . . . . . 8 setvar 𝑓
10	9	cv 1482	. . . . . . 7 class 𝑓
11		vp	. . . . . . . 8 setvar 𝑝
12	11	cv 1482	. . . . . . 7 class 𝑝
13		cwlks 26492	. . . . . . . 8 class Walks
14	6, 13	cfv 5888	. . . . . . 7 class (Walks‘𝑔)
15	10, 12, 14	wbr 4653	. . . . . 6 wff 𝑓(Walks‘𝑔)𝑝
16		cc0 9936	. . . . . . . 8 class 0
17	16, 12	cfv 5888	. . . . . . 7 class (𝑝‘0)
18	4	cv 1482	. . . . . . 7 class 𝑎
19	17, 18	wceq 1483	. . . . . 6 wff (𝑝‘0) = 𝑎
20		chash 13117	. . . . . . . . 9 class #
21	10, 20	cfv 5888	. . . . . . . 8 class (#‘𝑓)
22	21, 12	cfv 5888	. . . . . . 7 class (𝑝‘(#‘𝑓))
23	5	cv 1482	. . . . . . 7 class 𝑏
24	22, 23	wceq 1483	. . . . . 6 wff (𝑝‘(#‘𝑓)) = 𝑏
25	15, 19, 24	w3a 1037	. . . . 5 wff (𝑓(Walks‘𝑔)𝑝 ∧ (𝑝‘0) = 𝑎 ∧ (𝑝‘(#‘𝑓)) = 𝑏)
26	25, 9, 11	copab 4712	. . . 4 class {⟨𝑓, 𝑝⟩ ∣ (𝑓(Walks‘𝑔)𝑝 ∧ (𝑝‘0) = 𝑎 ∧ (𝑝‘(#‘𝑓)) = 𝑏)}
27	4, 5, 8, 8, 26	cmpt2 6652	. . 3 class (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(Walks‘𝑔)𝑝 ∧ (𝑝‘0) = 𝑎 ∧ (𝑝‘(#‘𝑓)) = 𝑏)})
28	2, 3, 27	cmpt 4729	. 2 class (𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(Walks‘𝑔)𝑝 ∧ (𝑝‘0) = 𝑎 ∧ (𝑝‘(#‘𝑓)) = 𝑏)}))
29	1, 28	wceq 1483	1 wff WalksOn = (𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(Walks‘𝑔)𝑝 ∧ (𝑝‘0) = 𝑎 ∧ (𝑝‘(#‘𝑓)) = 𝑏)}))

This definition is referenced by:  wlkson  26552  wlkonprop  26554