Metamath Proof Explorer


Definition df-wspthsnon

Description: Define the collection of simple paths of a fixed length with particular endpoints 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-wspthsnon
|- WSPathsNOn = ( n e. NN0 , g e. _V |-> ( a e. ( Vtx ` g ) , b e. ( Vtx ` g ) |-> { w e. ( a ( n WWalksNOn g ) b ) | E. f f ( a ( SPathsOn ` g ) b ) w } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cwwspthsnon
 |-  WSPathsNOn
1 vn
 |-  n
2 cn0
 |-  NN0
3 vg
 |-  g
4 cvv
 |-  _V
5 va
 |-  a
6 cvtx
 |-  Vtx
7 3 cv
 |-  g
8 7 6 cfv
 |-  ( Vtx ` g )
9 vb
 |-  b
10 vw
 |-  w
11 5 cv
 |-  a
12 1 cv
 |-  n
13 cwwlksnon
 |-  WWalksNOn
14 12 7 13 co
 |-  ( n WWalksNOn g )
15 9 cv
 |-  b
16 11 15 14 co
 |-  ( a ( n WWalksNOn g ) b )
17 vf
 |-  f
18 17 cv
 |-  f
19 cspthson
 |-  SPathsOn
20 7 19 cfv
 |-  ( SPathsOn ` g )
21 11 15 20 co
 |-  ( a ( SPathsOn ` g ) b )
22 10 cv
 |-  w
23 18 22 21 wbr
 |-  f ( a ( SPathsOn ` g ) b ) w
24 23 17 wex
 |-  E. f f ( a ( SPathsOn ` g ) b ) w
25 24 10 16 crab
 |-  { w e. ( a ( n WWalksNOn g ) b ) | E. f f ( a ( SPathsOn ` g ) b ) w }
26 5 9 8 8 25 cmpo
 |-  ( a e. ( Vtx ` g ) , b e. ( Vtx ` g ) |-> { w e. ( a ( n WWalksNOn g ) b ) | E. f f ( a ( SPathsOn ` g ) b ) w } )
27 1 3 2 4 26 cmpo
 |-  ( n e. NN0 , g e. _V |-> ( a e. ( Vtx ` g ) , b e. ( Vtx ` g ) |-> { w e. ( a ( n WWalksNOn g ) b ) | E. f f ( a ( SPathsOn ` g ) b ) w } ) )
28 0 27 wceq
 |-  WSPathsNOn = ( n e. NN0 , g e. _V |-> ( a e. ( Vtx ` g ) , b e. ( Vtx ` g ) |-> { w e. ( a ( n WWalksNOn g ) b ) | E. f f ( a ( SPathsOn ` g ) b ) w } ) )