Definition df-wwlksnon 41035

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 41030	. 2 class WWalksNOn
2		vn	. . 3 setvar 𝑛
3		vg	. . 3 setvar 𝑔
4		cn0 11169	. . 3 class ℕ0
5		cvv 3173	. . 3 class V
6		va	. . . 4 setvar 𝑎
7		vb	. . . 4 setvar 𝑏
8	3	cv 1474	. . . . 5 class 𝑔
9		cvtx 25673	. . . . 5 class Vtx
10	8, 9	cfv 5804	. . . 4 class (Vtx‘𝑔)
11		cc0 9815	. . . . . . . 8 class 0
12		vw	. . . . . . . . 9 setvar 𝑤
13	12	cv 1474	. . . . . . . 8 class 𝑤
14	11, 13	cfv 5804	. . . . . . 7 class (𝑤‘0)
15	6	cv 1474	. . . . . . 7 class 𝑎
16	14, 15	wceq 1475	. . . . . 6 wff (𝑤‘0) = 𝑎
17	2	cv 1474	. . . . . . . 8 class 𝑛
18	17, 13	cfv 5804	. . . . . . 7 class (𝑤‘𝑛)
19	7	cv 1474	. . . . . . 7 class 𝑏
20	18, 19	wceq 1475	. . . . . 6 wff (𝑤‘𝑛) = 𝑏
21	16, 20	wa 383	. . . . 5 wff ((𝑤‘0) = 𝑎 ∧ (𝑤‘𝑛) = 𝑏)
22		cwwlksn 41029	. . . . . 6 class WWalkSN
23	17, 8, 22	co 6549	. . . . 5 class (𝑛 WWalkSN 𝑔)
24	21, 12, 23	crab 2900	. . . 4 class {𝑤 ∈ (𝑛 WWalkSN 𝑔) ∣ ((𝑤‘0) = 𝑎 ∧ (𝑤‘𝑛) = 𝑏)}
25	6, 7, 10, 10, 24	cmpt2 6551	. . 3 class (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {𝑤 ∈ (𝑛 WWalkSN 𝑔) ∣ ((𝑤‘0) = 𝑎 ∧ (𝑤‘𝑛) = 𝑏)})
26	2, 3, 4, 5, 25	cmpt2 6551	. 2 class (𝑛 ∈ ℕ0, 𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {𝑤 ∈ (𝑛 WWalkSN 𝑔) ∣ ((𝑤‘0) = 𝑎 ∧ (𝑤‘𝑛) = 𝑏)}))
27	1, 26	wceq 1475	1 wff WWalksNOn = (𝑛 ∈ ℕ0, 𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {𝑤 ∈ (𝑛 WWalkSN 𝑔) ∣ ((𝑤‘0) = 𝑎 ∧ (𝑤‘𝑛) = 𝑏)}))

This definition is referenced by:  wwlksnon  41049  iswwlksnon  41051  iswspthsnon  41052  wwlksnon0  41123  wwlks2onv  41158