Metamath Proof Explorer

Definition df-wwlksnon

Description: Define the collection of walks of a fixed length with particular endpoints as word over the set of vertices. (Contributed by Alexander van der Vekens, 15-Feb-2018) (Revised by AV, 11-May-2021)

Ref Expression
Assertion df-wwlksnon 
|- WWalksNOn = ( n e. NN0 , g e. _V |-> ( a e. ( Vtx ` g ) , b e. ( Vtx ` g ) |-> { w e. ( n WWalksN g ) | ( ( w ` 0 ) = a /\ ( w ` n ) = b ) } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cwwlksnon 
 |-  WWalksNOn
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 1 cv 
 |-  n
12 cwwlksn 
 |-  WWalksN
13 11 7 12 co 
 |-  ( n WWalksN g )
14 10 cv 
 |-  w
15 cc0 
 |-  0
16 15 14 cfv 
 |-  ( w ` 0 )
17 5 cv 
 |-  a
18 16 17 wceq 
 |-  ( w ` 0 ) = a
19 11 14 cfv 
 |-  ( w ` n )
20 9 cv 
 |-  b
21 19 20 wceq 
 |-  ( w ` n ) = b
22 18 21 wa 
 |-  ( ( w ` 0 ) = a /\ ( w ` n ) = b )
23 22 10 13 crab 
 |-  { w e. ( n WWalksN g ) | ( ( w ` 0 ) = a /\ ( w ` n ) = b ) }
24 5 9 8 8 23 cmpo 
 |-  ( a e. ( Vtx ` g ) , b e. ( Vtx ` g ) |-> { w e. ( n WWalksN g ) | ( ( w ` 0 ) = a /\ ( w ` n ) = b ) } )
25 1 3 2 4 24 cmpo 
 |-  ( n e. NN0 , g e. _V |-> ( a e. ( Vtx ` g ) , b e. ( Vtx ` g ) |-> { w e. ( n WWalksN g ) | ( ( w ` 0 ) = a /\ ( w ` n ) = b ) } ) )
26 0 25 wceq 
 |-  WWalksNOn = ( n e. NN0 , g e. _V |-> ( a e. ( Vtx ` g ) , b e. ( Vtx ` g ) |-> { w e. ( n WWalksN g ) | ( ( w ` 0 ) = a /\ ( w ` n ) = b ) } ) )