Metamath Proof Explorer

Definition df-wspthsnon

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)

Ref Expression
Assertion df-wspthsnon ⊢ WSPathsNOn = n ∈ ℕ 0 , g ∈ V ⟼ a ∈ Vtx ⁡ g , b ∈ Vtx ⁡ g ⟼ w ∈ a n WWalksNOn g b | ∃ f f a SPathsOn ⁡ g b w

Detailed syntax breakdown

Step Hyp Ref Expression
0 cwwspthsnon class WSPathsNOn
1 vn setvar n
2 cn0 class ℕ 0
3 vg setvar g
4 cvv class V
5 va setvar a
6 cvtx class Vtx
7 3 cv setvar g
8 7 6 cfv class Vtx ⁡ g
9 vb setvar b
10 vw setvar w
11 5 cv setvar a
12 1 cv setvar n
13 cwwlksnon class WWalksNOn
14 12 7 13 co class n WWalksNOn g
15 9 cv setvar b
16 11 15 14 co class a n WWalksNOn g b
17 vf setvar f
18 17 cv setvar f
19 cspthson class SPathsOn
20 7 19 cfv class SPathsOn ⁡ g
21 11 15 20 co class a SPathsOn ⁡ g b
22 10 cv setvar w
23 18 22 21 wbr wff f a SPathsOn ⁡ g b w
24 23 17 wex wff ∃ f f a SPathsOn ⁡ g b w
25 24 10 16 crab class w ∈ a n WWalksNOn g b | ∃ f f a SPathsOn ⁡ g b w
26 5 9 8 8 25 cmpo class a ∈ Vtx ⁡ g , b ∈ Vtx ⁡ g ⟼ w ∈ a n WWalksNOn g b | ∃ f f a SPathsOn ⁡ g b w
27 1 3 2 4 26 cmpo class n ∈ ℕ 0 , g ∈ V ⟼ a ∈ Vtx ⁡ g , b ∈ Vtx ⁡ g ⟼ w ∈ a n WWalksNOn g b | ∃ f f a SPathsOn ⁡ g b w
28 0 27 wceq wff WSPathsNOn = n ∈ ℕ 0 , g ∈ V ⟼ a ∈ Vtx ⁡ g , b ∈ Vtx ⁡ g ⟼ w ∈ a n WWalksNOn g b | ∃ f f a SPathsOn ⁡ g b w