Definition df-wspthsnon 29854

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 = (𝑛 ∈ ℕ0, 𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {𝑤 ∈ (𝑎(𝑛 WWalksNOn 𝑔)𝑏) ∣ ∃𝑓 𝑓(𝑎(SPathsOn‘𝑔)𝑏)𝑤}))

Distinct variable group:   𝑎,𝑏,𝑓,𝑔,𝑛,𝑤

Detailed syntax breakdown of Definition df-wspthsnon

Step	Hyp	Ref	Expression
1		cwwspthsnon 29849	. 2 class WSPathsNOn
2		vn	. . 3 setvar 𝑛
3		vg	. . 3 setvar 𝑔
4		cn0 12526	. . 3 class ℕ0
5		cvv 3480	. . 3 class V
6		va	. . . 4 setvar 𝑎
7		vb	. . . 4 setvar 𝑏
8	3	cv 1539	. . . . 5 class 𝑔
9		cvtx 29013	. . . . 5 class Vtx
10	8, 9	cfv 6561	. . . 4 class (Vtx‘𝑔)
11		vf	. . . . . . . 8 setvar 𝑓
12	11	cv 1539	. . . . . . 7 class 𝑓
13		vw	. . . . . . . 8 setvar 𝑤
14	13	cv 1539	. . . . . . 7 class 𝑤
15	6	cv 1539	. . . . . . . 8 class 𝑎
16	7	cv 1539	. . . . . . . 8 class 𝑏
17		cspthson 29733	. . . . . . . . 9 class SPathsOn
18	8, 17	cfv 6561	. . . . . . . 8 class (SPathsOn‘𝑔)
19	15, 16, 18	co 7431	. . . . . . 7 class (𝑎(SPathsOn‘𝑔)𝑏)
20	12, 14, 19	wbr 5143	. . . . . 6 wff 𝑓(𝑎(SPathsOn‘𝑔)𝑏)𝑤
21	20, 11	wex 1779	. . . . 5 wff ∃𝑓 𝑓(𝑎(SPathsOn‘𝑔)𝑏)𝑤
22	2	cv 1539	. . . . . . 7 class 𝑛
23		cwwlksnon 29847	. . . . . . 7 class WWalksNOn
24	22, 8, 23	co 7431	. . . . . 6 class (𝑛 WWalksNOn 𝑔)
25	15, 16, 24	co 7431	. . . . 5 class (𝑎(𝑛 WWalksNOn 𝑔)𝑏)
26	21, 13, 25	crab 3436	. . . 4 class {𝑤 ∈ (𝑎(𝑛 WWalksNOn 𝑔)𝑏) ∣ ∃𝑓 𝑓(𝑎(SPathsOn‘𝑔)𝑏)𝑤}
27	6, 7, 10, 10, 26	cmpo 7433	. . 3 class (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {𝑤 ∈ (𝑎(𝑛 WWalksNOn 𝑔)𝑏) ∣ ∃𝑓 𝑓(𝑎(SPathsOn‘𝑔)𝑏)𝑤})
28	2, 3, 4, 5, 27	cmpo 7433	. 2 class (𝑛 ∈ ℕ0, 𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {𝑤 ∈ (𝑎(𝑛 WWalksNOn 𝑔)𝑏) ∣ ∃𝑓 𝑓(𝑎(SPathsOn‘𝑔)𝑏)𝑤}))
29	1, 28	wceq 1540	1 wff WSPathsNOn = (𝑛 ∈ ℕ0, 𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {𝑤 ∈ (𝑎(𝑛 WWalksNOn 𝑔)𝑏) ∣ ∃𝑓 𝑓(𝑎(SPathsOn‘𝑔)𝑏)𝑤}))

This definition is referenced by:  wspthsnon  29872  iswspthsnon  29876  wspthnonp  29879