Definition df-wspthsn 41036

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 41031	. 2 class WSPathsN
2		vn	. . 3 setvar 𝑛
3		vg	. . 3 setvar 𝑔
4		cn0 11169	. . 3 class ℕ0
5		cvv 3173	. . 3 class V
6		vf	. . . . . . 7 setvar 𝑓
7	6	cv 1474	. . . . . 6 class 𝑓
8		vw	. . . . . . 7 setvar 𝑤
9	8	cv 1474	. . . . . 6 class 𝑤
10	3	cv 1474	. . . . . . 7 class 𝑔
11		cspths 40920	. . . . . . 7 class SPathS
12	10, 11	cfv 5804	. . . . . 6 class (SPathS‘𝑔)
13	7, 9, 12	wbr 4583	. . . . 5 wff 𝑓(SPathS‘𝑔)𝑤
14	13, 6	wex 1695	. . . 4 wff ∃𝑓 𝑓(SPathS‘𝑔)𝑤
15	2	cv 1474	. . . . 5 class 𝑛
16		cwwlksn 41029	. . . . 5 class WWalkSN
17	15, 10, 16	co 6549	. . . 4 class (𝑛 WWalkSN 𝑔)
18	14, 8, 17	crab 2900	. . 3 class {𝑤 ∈ (𝑛 WWalkSN 𝑔) ∣ ∃𝑓 𝑓(SPathS‘𝑔)𝑤}
19	2, 3, 4, 5, 18	cmpt2 6551	. 2 class (𝑛 ∈ ℕ0, 𝑔 ∈ V ↦ {𝑤 ∈ (𝑛 WWalkSN 𝑔) ∣ ∃𝑓 𝑓(SPathS‘𝑔)𝑤})
20	1, 19	wceq 1475	1 wff WSPathsN = (𝑛 ∈ ℕ0, 𝑔 ∈ V ↦ {𝑤 ∈ (𝑛 WWalkSN 𝑔) ∣ ∃𝑓 𝑓(SPathS‘𝑔)𝑤})

This definition is referenced by:  wspthsn  41046  wspthnp  41048  wspn0  41131