Definition df-wspthsn 29853

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 29848	. 2 class WSPathsN
2		vn	. . 3 setvar 𝑛
3		vg	. . 3 setvar 𝑔
4		cn0 12526	. . 3 class ℕ0
5		cvv 3480	. . 3 class V
6		vf	. . . . . . 7 setvar 𝑓
7	6	cv 1539	. . . . . 6 class 𝑓
8		vw	. . . . . . 7 setvar 𝑤
9	8	cv 1539	. . . . . 6 class 𝑤
10	3	cv 1539	. . . . . . 7 class 𝑔
11		cspths 29731	. . . . . . 7 class SPaths
12	10, 11	cfv 6561	. . . . . 6 class (SPaths‘𝑔)
13	7, 9, 12	wbr 5143	. . . . 5 wff 𝑓(SPaths‘𝑔)𝑤
14	13, 6	wex 1779	. . . 4 wff ∃𝑓 𝑓(SPaths‘𝑔)𝑤
15	2	cv 1539	. . . . 5 class 𝑛
16		cwwlksn 29846	. . . . 5 class WWalksN
17	15, 10, 16	co 7431	. . . 4 class (𝑛 WWalksN 𝑔)
18	14, 8, 17	crab 3436	. . 3 class {𝑤 ∈ (𝑛 WWalksN 𝑔) ∣ ∃𝑓 𝑓(SPaths‘𝑔)𝑤}
19	2, 3, 4, 5, 18	cmpo 7433	. 2 class (𝑛 ∈ ℕ0, 𝑔 ∈ V ↦ {𝑤 ∈ (𝑛 WWalksN 𝑔) ∣ ∃𝑓 𝑓(SPaths‘𝑔)𝑤})
20	1, 19	wceq 1540	1 wff WSPathsN = (𝑛 ∈ ℕ0, 𝑔 ∈ V ↦ {𝑤 ∈ (𝑛 WWalksN 𝑔) ∣ ∃𝑓 𝑓(SPaths‘𝑔)𝑤})

This definition is referenced by:  wspthsn  29868  wspthnp  29870