Definition df-wwlksnon 26724

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

Assertion

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

Distinct variable group:   a, b, g, n, w

Detailed syntax breakdown of Definition df-wwlksnon

Step	Hyp	Ref	Expression
1		cwwlksnon 26719	. 2 class WWalksNOn
2		vn	. . 3 setvar n
3		vg	. . 3 setvar g
4		cn0 11292	. . 3 class NN0
5		cvv 3200	. . 3 class _V
6		va	. . . 4 setvar a
7		vb	. . . 4 setvar b
8	3	cv 1482	. . . . 5 class g
9		cvtx 25874	. . . . 5 class Vtx
10	8, 9	cfv 5888	. . . 4 class (Vtx ` g )
11		cc0 9936	. . . . . . . 8 class 0
12		vw	. . . . . . . . 9 setvar w
13	12	cv 1482	. . . . . . . 8 class w
14	11, 13	cfv 5888	. . . . . . 7 class ( w ` 0 )
15	6	cv 1482	. . . . . . 7 class a
16	14, 15	wceq 1483	. . . . . 6 wff ( w ` 0 ) = a
17	2	cv 1482	. . . . . . . 8 class n
18	17, 13	cfv 5888	. . . . . . 7 class ( w ` n )
19	7	cv 1482	. . . . . . 7 class b
20	18, 19	wceq 1483	. . . . . 6 wff ( w ` n ) = b
21	16, 20	wa 384	. . . . 5 wff ( ( w ` 0 ) = a /\ ( w ` n ) = b )
22		cwwlksn 26718	. . . . . 6 class WWalksN
23	17, 8, 22	co 6650	. . . . 5 class ( n WWalksN g )
24	21, 12, 23	crab 2916	. . . 4 class { w e. ( n WWalksN g ) | ( ( w ` 0 ) = a /\ ( w ` n ) = b ) }
25	6, 7, 10, 10, 24	cmpt2 6652	. . 3 class ( a e. (Vtx ` g ) , b e. (Vtx ` g ) |-> { w e. ( n WWalksN g ) | ( ( w ` 0 ) = a /\ ( w ` n ) = b ) } )
26	2, 3, 4, 5, 25	cmpt2 6652	. 2 class ( 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 ) } ) )
27	1, 26	wceq 1483	1 wff 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 ) } ) )

This definition is referenced by:  wwlksnon  26738  iswwlksnon  26740  iswspthsnon  26741  wwlksnon0  26812  wwlks2onv  26847