Definition df-wlkon 26042

Description: Define the collection of walks with particular endpoints (in an un- directed graph). 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.)

Assertion

Ref	Expression
df-wlkon	⊢ WalkOn = (𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝑣 Walks 𝑒)𝑝 ∧ (𝑝‘0) = 𝑎 ∧ (𝑝‘(#‘𝑓)) = 𝑏)}))

Distinct variable groups:   𝑣,𝑒,𝑓,𝑝   𝑎,𝑏,𝑒,𝑓,𝑝,𝑣

Detailed syntax breakdown of Definition df-wlkon

Step	Hyp	Ref	Expression
1		cwlkon 26030	. 2 class WalkOn
2		vv	. . 3 setvar 𝑣
3		ve	. . 3 setvar 𝑒
4		cvv 3173	. . 3 class V
5		va	. . . 4 setvar 𝑎
6		vb	. . . 4 setvar 𝑏
7	2	cv 1474	. . . 4 class 𝑣
8		vf	. . . . . . . 8 setvar 𝑓
9	8	cv 1474	. . . . . . 7 class 𝑓
10		vp	. . . . . . . 8 setvar 𝑝
11	10	cv 1474	. . . . . . 7 class 𝑝
12	3	cv 1474	. . . . . . . 8 class 𝑒
13		cwalk 26026	. . . . . . . 8 class Walks
14	7, 12, 13	co 6549	. . . . . . 7 class (𝑣 Walks 𝑒)
15	9, 11, 14	wbr 4583	. . . . . 6 wff 𝑓(𝑣 Walks 𝑒)𝑝
16		cc0 9815	. . . . . . . 8 class 0
17	16, 11	cfv 5804	. . . . . . 7 class (𝑝‘0)
18	5	cv 1474	. . . . . . 7 class 𝑎
19	17, 18	wceq 1475	. . . . . 6 wff (𝑝‘0) = 𝑎
20		chash 12979	. . . . . . . . 9 class #
21	9, 20	cfv 5804	. . . . . . . 8 class (#‘𝑓)
22	21, 11	cfv 5804	. . . . . . 7 class (𝑝‘(#‘𝑓))
23	6	cv 1474	. . . . . . 7 class 𝑏
24	22, 23	wceq 1475	. . . . . 6 wff (𝑝‘(#‘𝑓)) = 𝑏
25	15, 19, 24	w3a 1031	. . . . 5 wff (𝑓(𝑣 Walks 𝑒)𝑝 ∧ (𝑝‘0) = 𝑎 ∧ (𝑝‘(#‘𝑓)) = 𝑏)
26	25, 8, 10	copab 4642	. . . 4 class {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝑣 Walks 𝑒)𝑝 ∧ (𝑝‘0) = 𝑎 ∧ (𝑝‘(#‘𝑓)) = 𝑏)}
27	5, 6, 7, 7, 26	cmpt2 6551	. . 3 class (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝑣 Walks 𝑒)𝑝 ∧ (𝑝‘0) = 𝑎 ∧ (𝑝‘(#‘𝑓)) = 𝑏)})
28	2, 3, 4, 4, 27	cmpt2 6551	. 2 class (𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝑣 Walks 𝑒)𝑝 ∧ (𝑝‘0) = 𝑎 ∧ (𝑝‘(#‘𝑓)) = 𝑏)}))
29	1, 28	wceq 1475	1 wff WalkOn = (𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(𝑣 Walks 𝑒)𝑝 ∧ (𝑝‘0) = 𝑎 ∧ (𝑝‘(#‘𝑓)) = 𝑏)}))

This definition is referenced by:  wlkon  26061  wlkonprop  26063