Definition df-wspthsn 29354

Description: Define the collection of simple paths of a fixed length 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-wspthsn	⊢ WSPathsN = (𝑛 ∈ ℕ0, 𝑔 ∈ V ↦ {𝑤 ∈ (𝑛 WWalksN 𝑔) ∣ ∃𝑓 𝑓(SPaths‘𝑔)𝑤})

Distinct variable group:   𝑓,𝑔,𝑛,𝑤

Detailed syntax breakdown of Definition df-wspthsn

Step	Hyp	Ref	Expression
1		cwwspthsn 29349	. 2 class WSPathsN
2		vn	. . 3 setvar 𝑛
3		vg	. . 3 setvar 𝑔
4		cn0 12476	. . 3 class ℕ0
5		cvv 3472	. . 3 class V
6		vf	. . . . . . 7 setvar 𝑓
7	6	cv 1538	. . . . . 6 class 𝑓
8		vw	. . . . . . 7 setvar 𝑤
9	8	cv 1538	. . . . . 6 class 𝑤
10	3	cv 1538	. . . . . . 7 class 𝑔
11		cspths 29237	. . . . . . 7 class SPaths
12	10, 11	cfv 6542	. . . . . 6 class (SPaths‘𝑔)
13	7, 9, 12	wbr 5147	. . . . 5 wff 𝑓(SPaths‘𝑔)𝑤
14	13, 6	wex 1779	. . . 4 wff ∃𝑓 𝑓(SPaths‘𝑔)𝑤
15	2	cv 1538	. . . . 5 class 𝑛
16		cwwlksn 29347	. . . . 5 class WWalksN
17	15, 10, 16	co 7411	. . . 4 class (𝑛 WWalksN 𝑔)
18	14, 8, 17	crab 3430	. . 3 class {𝑤 ∈ (𝑛 WWalksN 𝑔) ∣ ∃𝑓 𝑓(SPaths‘𝑔)𝑤}
19	2, 3, 4, 5, 18	cmpo 7413	. 2 class (𝑛 ∈ ℕ0, 𝑔 ∈ V ↦ {𝑤 ∈ (𝑛 WWalksN 𝑔) ∣ ∃𝑓 𝑓(SPaths‘𝑔)𝑤})
20	1, 19	wceq 1539	1 wff WSPathsN = (𝑛 ∈ ℕ0, 𝑔 ∈ V ↦ {𝑤 ∈ (𝑛 WWalksN 𝑔) ∣ ∃𝑓 𝑓(SPaths‘𝑔)𝑤})

This definition is referenced by:  wspthsn  29369  wspthnp  29371