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)
Ref | Expression | ||
---|---|---|---|
Assertion | df-wspthsn | |- WSPathsN = ( n e. NN0 , g e. _V |-> { w e. ( n WWalksN g ) | E. f f ( SPaths ` g ) w } ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cwwspthsn | |- WSPathsN |
|
1 | vn | |- n |
|
2 | cn0 | |- NN0 |
|
3 | vg | |- g |
|
4 | cvv | |- _V |
|
5 | vw | |- w |
|
6 | 1 | cv | |- n |
7 | cwwlksn | |- WWalksN |
|
8 | 3 | cv | |- g |
9 | 6 8 7 | co | |- ( n WWalksN g ) |
10 | vf | |- f |
|
11 | 10 | cv | |- f |
12 | cspths | |- SPaths |
|
13 | 8 12 | cfv | |- ( SPaths ` g ) |
14 | 5 | cv | |- w |
15 | 11 14 13 | wbr | |- f ( SPaths ` g ) w |
16 | 15 10 | wex | |- E. f f ( SPaths ` g ) w |
17 | 16 5 9 | crab | |- { w e. ( n WWalksN g ) | E. f f ( SPaths ` g ) w } |
18 | 1 3 2 4 17 | cmpo | |- ( n e. NN0 , g e. _V |-> { w e. ( n WWalksN g ) | E. f f ( SPaths ` g ) w } ) |
19 | 0 18 | wceq | |- WSPathsN = ( n e. NN0 , g e. _V |-> { w e. ( n WWalksN g ) | E. f f ( SPaths ` g ) w } ) |