Metamath Proof Explorer

Definition df-wwlksnon

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)

Ref Expression
Assertion df-wwlksnon ⊢ WWalksNOn = n ∈ ℕ 0 , g ∈ V ⟼ a ∈ Vtx ⁡ g , b ∈ Vtx ⁡ g ⟼ w ∈ n WWalksN g | w ⁡ 0 = a ∧ w ⁡ n = b

Detailed syntax breakdown

Step Hyp Ref Expression
0 cwwlksnon class WWalksNOn
1 vn setvar n
2 cn0 class ℕ 0
3 vg setvar g
4 cvv class V
5 va setvar a
6 cvtx class Vtx
7 3 cv setvar g
8 7 6 cfv class Vtx ⁡ g
9 vb setvar b
10 vw setvar w
11 1 cv setvar n
12 cwwlksn class WWalksN
13 11 7 12 co class n WWalksN g
14 10 cv setvar w
15 cc0 class 0
16 15 14 cfv class w ⁡ 0
17 5 cv setvar a
18 16 17 wceq wff w ⁡ 0 = a
19 11 14 cfv class w ⁡ n
20 9 cv setvar b
21 19 20 wceq wff w ⁡ n = b
22 18 21 wa wff w ⁡ 0 = a ∧ w ⁡ n = b
23 22 10 13 crab class w ∈ n WWalksN g | w ⁡ 0 = a ∧ w ⁡ n = b
24 5 9 8 8 23 cmpo class a ∈ Vtx ⁡ g , b ∈ Vtx ⁡ g ⟼ w ∈ n WWalksN g | w ⁡ 0 = a ∧ w ⁡ n = b
25 1 3 2 4 24 cmpo class n ∈ ℕ 0 , g ∈ V ⟼ a ∈ Vtx ⁡ g , b ∈ Vtx ⁡ g ⟼ w ∈ n WWalksN g | w ⁡ 0 = a ∧ w ⁡ n = b
26 0 25 wceq wff WWalksNOn = n ∈ ℕ 0 , g ∈ V ⟼ a ∈ Vtx ⁡ g , b ∈ Vtx ⁡ g ⟼ w ∈ n WWalksN g | w ⁡ 0 = a ∧ w ⁡ n = b