Metamath Proof Explorer


Definition df-wspthsn

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 } )

Detailed syntax breakdown

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 } )