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

Definition df-wspthsn 29087
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 29082 . 2 class WSPathsN
2 vn . . 3 setvar 𝑛
3 vg . . 3 setvar 𝑔
4 cn0 12472 . . 3 class β„•0
5 cvv 3475 . . 3 class V
6 vf . . . . . . 7 setvar 𝑓
76cv 1541 . . . . . 6 class 𝑓
8 vw . . . . . . 7 setvar 𝑀
98cv 1541 . . . . . 6 class 𝑀
103cv 1541 . . . . . . 7 class 𝑔
11 cspths 28970 . . . . . . 7 class SPaths
1210, 11cfv 6544 . . . . . 6 class (SPathsβ€˜π‘”)
137, 9, 12wbr 5149 . . . . 5 wff 𝑓(SPathsβ€˜π‘”)𝑀
1413, 6wex 1782 . . . 4 wff βˆƒπ‘“ 𝑓(SPathsβ€˜π‘”)𝑀
152cv 1541 . . . . 5 class 𝑛
16 cwwlksn 29080 . . . . 5 class WWalksN
1715, 10, 16co 7409 . . . 4 class (𝑛 WWalksN 𝑔)
1814, 8, 17crab 3433 . . 3 class {𝑀 ∈ (𝑛 WWalksN 𝑔) ∣ βˆƒπ‘“ 𝑓(SPathsβ€˜π‘”)𝑀}
192, 3, 4, 5, 18cmpo 7411 . 2 class (𝑛 ∈ β„•0, 𝑔 ∈ V ↦ {𝑀 ∈ (𝑛 WWalksN 𝑔) ∣ βˆƒπ‘“ 𝑓(SPathsβ€˜π‘”)𝑀})
201, 19wceq 1542 1 wff WSPathsN = (𝑛 ∈ β„•0, 𝑔 ∈ V ↦ {𝑀 ∈ (𝑛 WWalksN 𝑔) ∣ βˆƒπ‘“ 𝑓(SPathsβ€˜π‘”)𝑀})
Colors of variables: wff setvar class
This definition is referenced by:  wspthsn  29102  wspthnp  29104
  Copyright terms: Public domain W3C validator