Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-wspthsn Structured version   Visualization version   GIF version

Definition df-wspthsn 41036
 Description: Define the collection of simple paths of a fixed length as word over the set of vertices. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 11-May-2021.)
Assertion
Ref Expression
df-wspthsn WSPathsN = (𝑛 ∈ ℕ0, 𝑔 ∈ V ↦ {𝑤 ∈ (𝑛 WWalkSN 𝑔) ∣ ∃𝑓 𝑓(SPathS‘𝑔)𝑤})
Distinct variable group:   𝑓,𝑔,𝑛,𝑤

Detailed syntax breakdown of Definition df-wspthsn
StepHypRef Expression
1 cwwspthsn 41031 . 2 class WSPathsN
2 vn . . 3 setvar 𝑛
3 vg . . 3 setvar 𝑔
4 cn0 11169 . . 3 class 0
5 cvv 3173 . . 3 class V
6 vf . . . . . . 7 setvar 𝑓
76cv 1474 . . . . . 6 class 𝑓
8 vw . . . . . . 7 setvar 𝑤
98cv 1474 . . . . . 6 class 𝑤
103cv 1474 . . . . . . 7 class 𝑔
11 cspths 40920 . . . . . . 7 class SPathS
1210, 11cfv 5804 . . . . . 6 class (SPathS‘𝑔)
137, 9, 12wbr 4583 . . . . 5 wff 𝑓(SPathS‘𝑔)𝑤
1413, 6wex 1695 . . . 4 wff 𝑓 𝑓(SPathS‘𝑔)𝑤
152cv 1474 . . . . 5 class 𝑛
16 cwwlksn 41029 . . . . 5 class WWalkSN
1715, 10, 16co 6549 . . . 4 class (𝑛 WWalkSN 𝑔)
1814, 8, 17crab 2900 . . 3 class {𝑤 ∈ (𝑛 WWalkSN 𝑔) ∣ ∃𝑓 𝑓(SPathS‘𝑔)𝑤}
192, 3, 4, 5, 18cmpt2 6551 . 2 class (𝑛 ∈ ℕ0, 𝑔 ∈ V ↦ {𝑤 ∈ (𝑛 WWalkSN 𝑔) ∣ ∃𝑓 𝑓(SPathS‘𝑔)𝑤})
201, 19wceq 1475 1 wff WSPathsN = (𝑛 ∈ ℕ0, 𝑔 ∈ V ↦ {𝑤 ∈ (𝑛 WWalkSN 𝑔) ∣ ∃𝑓 𝑓(SPathS‘𝑔)𝑤})
 Colors of variables: wff setvar class This definition is referenced by:  wspthsn  41046  wspthnp  41048  wspn0  41131
 Copyright terms: Public domain W3C validator