Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-wwlksnon Structured version   Visualization version   GIF version

Definition df-wwlksnon 26935
 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
StepHypRef Expression
1 cwwlksnon 26930 . 2 class WWalksNOn
2 vn . . 3 setvar 𝑛
3 vg . . 3 setvar 𝑔
4 cn0 11484 . . 3 class 0
5 cvv 3340 . . 3 class V
6 va . . . 4 setvar 𝑎
7 vb . . . 4 setvar 𝑏
83cv 1631 . . . . 5 class 𝑔
9 cvtx 26073 . . . . 5 class Vtx
108, 9cfv 6049 . . . 4 class (Vtx‘𝑔)
11 cc0 10128 . . . . . . . 8 class 0
12 vw . . . . . . . . 9 setvar 𝑤
1312cv 1631 . . . . . . . 8 class 𝑤
1411, 13cfv 6049 . . . . . . 7 class (𝑤‘0)
156cv 1631 . . . . . . 7 class 𝑎
1614, 15wceq 1632 . . . . . 6 wff (𝑤‘0) = 𝑎
172cv 1631 . . . . . . . 8 class 𝑛
1817, 13cfv 6049 . . . . . . 7 class (𝑤𝑛)
197cv 1631 . . . . . . 7 class 𝑏
2018, 19wceq 1632 . . . . . 6 wff (𝑤𝑛) = 𝑏
2116, 20wa 383 . . . . 5 wff ((𝑤‘0) = 𝑎 ∧ (𝑤𝑛) = 𝑏)
22 cwwlksn 26929 . . . . . 6 class WWalksN
2317, 8, 22co 6813 . . . . 5 class (𝑛 WWalksN 𝑔)
2421, 12, 23crab 3054 . . . 4 class {𝑤 ∈ (𝑛 WWalksN 𝑔) ∣ ((𝑤‘0) = 𝑎 ∧ (𝑤𝑛) = 𝑏)}
256, 7, 10, 10, 24cmpt2 6815 . . 3 class (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {𝑤 ∈ (𝑛 WWalksN 𝑔) ∣ ((𝑤‘0) = 𝑎 ∧ (𝑤𝑛) = 𝑏)})
262, 3, 4, 5, 25cmpt2 6815 . 2 class (𝑛 ∈ ℕ0, 𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {𝑤 ∈ (𝑛 WWalksN 𝑔) ∣ ((𝑤‘0) = 𝑎 ∧ (𝑤𝑛) = 𝑏)}))
271, 26wceq 1632 1 wff WWalksNOn = (𝑛 ∈ ℕ0, 𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {𝑤 ∈ (𝑛 WWalksN 𝑔) ∣ ((𝑤‘0) = 𝑎 ∧ (𝑤𝑛) = 𝑏)}))
 Colors of variables: wff setvar class This definition is referenced by:  wwlksnon  26955  iswwlksnon  26957  iswwlksnonOLD  26958  wwlksnon0  26959  wwlksonvtx  26960  iswspthsnonOLD  26962
 Copyright terms: Public domain W3C validator