Metamath Proof Explorer

Definition df-wspthsn

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)

Ref Expression
Assertion df-wspthsn ⊢ WSPathsN = n ∈ ℕ 0 , g ∈ V ⟼ w ∈ n WWalksN g | ∃ f f SPaths ⁡ g w

Detailed syntax breakdown

Step Hyp Ref Expression
0 cwwspthsn class WSPathsN
1 vn setvar n
2 cn0 class ℕ 0
3 vg setvar g
4 cvv class V
5 vw setvar w
6 1 cv setvar n
7 cwwlksn class WWalksN
8 3 cv setvar g
9 6 8 7 co class n WWalksN g
10 vf setvar f
11 10 cv setvar f
12 cspths class SPaths
13 8 12 cfv class SPaths ⁡ g
14 5 cv setvar w
15 11 14 13 wbr wff f SPaths ⁡ g w
16 15 10 wex wff ∃ f f SPaths ⁡ g w
17 16 5 9 crab class w ∈ n WWalksN g | ∃ f f SPaths ⁡ g w
18 1 3 2 4 17 cmpo class n ∈ ℕ 0 , g ∈ V ⟼ w ∈ n WWalksN g | ∃ f f SPaths ⁡ g w
19 0 18 wceq wff WSPathsN = n ∈ ℕ 0 , g ∈ V ⟼ w ∈ n WWalksN g | ∃ f f SPaths ⁡ g w