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