Definition df-wwlksnon 29819

Description: Define the collection of walks of a fixed length with particular endpoints as word over the set of vertices. (Contributed by Alexander van der Vekens, 15-Feb-2018.) (Revised by AV, 11-May-2021.)

Assertion

Ref	Expression
df-wwlksnon	⊢ WWalksNOn = (𝑛 ∈ ℕ0, 𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {𝑤 ∈ (𝑛 WWalksN 𝑔) ∣ ((𝑤‘0) = 𝑎 ∧ (𝑤‘𝑛) = 𝑏)}))

Distinct variable group:   𝑎,𝑏,𝑔,𝑛,𝑤

Detailed syntax breakdown of Definition df-wwlksnon

Step	Hyp	Ref	Expression
1		cwwlksnon 29814	. 2 class WWalksNOn
2		vn	. . 3 setvar 𝑛
3		vg	. . 3 setvar 𝑔
4		cn0 12506	. . 3 class ℕ0
5		cvv 3464	. . 3 class V
6		va	. . . 4 setvar 𝑎
7		vb	. . . 4 setvar 𝑏
8	3	cv 1539	. . . . 5 class 𝑔
9		cvtx 28980	. . . . 5 class Vtx
10	8, 9	cfv 6536	. . . 4 class (Vtx‘𝑔)
11		cc0 11134	. . . . . . . 8 class 0
12		vw	. . . . . . . . 9 setvar 𝑤
13	12	cv 1539	. . . . . . . 8 class 𝑤
14	11, 13	cfv 6536	. . . . . . 7 class (𝑤‘0)
15	6	cv 1539	. . . . . . 7 class 𝑎
16	14, 15	wceq 1540	. . . . . 6 wff (𝑤‘0) = 𝑎
17	2	cv 1539	. . . . . . . 8 class 𝑛
18	17, 13	cfv 6536	. . . . . . 7 class (𝑤‘𝑛)
19	7	cv 1539	. . . . . . 7 class 𝑏
20	18, 19	wceq 1540	. . . . . 6 wff (𝑤‘𝑛) = 𝑏
21	16, 20	wa 395	. . . . 5 wff ((𝑤‘0) = 𝑎 ∧ (𝑤‘𝑛) = 𝑏)
22		cwwlksn 29813	. . . . . 6 class WWalksN
23	17, 8, 22	co 7410	. . . . 5 class (𝑛 WWalksN 𝑔)
24	21, 12, 23	crab 3420	. . . 4 class {𝑤 ∈ (𝑛 WWalksN 𝑔) ∣ ((𝑤‘0) = 𝑎 ∧ (𝑤‘𝑛) = 𝑏)}
25	6, 7, 10, 10, 24	cmpo 7412	. . 3 class (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {𝑤 ∈ (𝑛 WWalksN 𝑔) ∣ ((𝑤‘0) = 𝑎 ∧ (𝑤‘𝑛) = 𝑏)})
26	2, 3, 4, 5, 25	cmpo 7412	. 2 class (𝑛 ∈ ℕ0, 𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {𝑤 ∈ (𝑛 WWalksN 𝑔) ∣ ((𝑤‘0) = 𝑎 ∧ (𝑤‘𝑛) = 𝑏)}))
27	1, 26	wceq 1540	1 wff WWalksNOn = (𝑛 ∈ ℕ0, 𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {𝑤 ∈ (𝑛 WWalksN 𝑔) ∣ ((𝑤‘0) = 𝑎 ∧ (𝑤‘𝑛) = 𝑏)}))

This definition is referenced by:  wwlksnon  29838  iswwlksnon  29840  wwlksnon0  29841  wwlksonvtx  29842