Definition df-wspthsnon 26726

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

Assertion

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

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

Detailed syntax breakdown of Definition df-wspthsnon

Step	Hyp	Ref	Expression
1		cwwspthsnon 26721	. 2 class WSPathsNOn
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		vf	. . . . . . . 8 setvar f
12	11	cv 1482	. . . . . . 7 class f
13		vw	. . . . . . . 8 setvar w
14	13	cv 1482	. . . . . . 7 class w
15	6	cv 1482	. . . . . . . 8 class a
16	7	cv 1482	. . . . . . . 8 class b
17		cspthson 26611	. . . . . . . . 9 class SPathsOn
18	8, 17	cfv 5888	. . . . . . . 8 class (SPathsOn ` g )
19	15, 16, 18	co 6650	. . . . . . 7 class ( a (SPathsOn ` g ) b )
20	12, 14, 19	wbr 4653	. . . . . 6 wff f ( a (SPathsOn ` g ) b ) w
21	20, 11	wex 1704	. . . . 5 wff E. f f ( a (SPathsOn ` g ) b ) w
22	2	cv 1482	. . . . . . 7 class n
23		cwwlksnon 26719	. . . . . . 7 class WWalksNOn
24	22, 8, 23	co 6650	. . . . . 6 class ( n WWalksNOn g )
25	15, 16, 24	co 6650	. . . . 5 class ( a ( n WWalksNOn g ) b )
26	21, 13, 25	crab 2916	. . . 4 class { w e. ( a ( n WWalksNOn g ) b ) | E. f f ( a (SPathsOn ` g ) b ) w }
27	6, 7, 10, 10, 26	cmpt2 6652	. . 3 class ( a e. (Vtx ` g ) , b e. (Vtx ` g ) |-> { w e. ( a ( n WWalksNOn g ) b ) | E. f f ( a (SPathsOn ` g ) b ) w } )
28	2, 3, 4, 5, 27	cmpt2 6652	. 2 class ( 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 } ) )
29	1, 28	wceq 1483	1 wff 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 } ) )

This definition is referenced by:  wspthsnon  26739  iswspthsnon  26741  wspthnonp  26744