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 \in ℕ_{0}, g \in V ⟼ (a \in Vtx (g), b \in Vtx (g) ⟼ \{w \in (a (n WWalksNOn g) b) \| \exists 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 \exists f f (a SPathsOn (g) b) w$
25	24 10 16	crab	$class \{w \in (a (n WWalksNOn g) b) \| \exists f f (a SPathsOn (g) b) w\}$
26	5 9 8 8 25	cmpo	$class (a \in Vtx (g), b \in Vtx (g) ⟼ \{w \in (a (n WWalksNOn g) b) \| \exists f f (a SPathsOn (g) b) w\})$
27	1 3 2 4 26	cmpo	$class (n \in ℕ_{0}, g \in V ⟼ (a \in Vtx (g), b \in Vtx (g) ⟼ \{w \in (a (n WWalksNOn g) b) \| \exists f f (a SPathsOn (g) b) w\}))$
28	0 27	wceq	$wff WSPathsNOn = (n \in ℕ_{0}, g \in V ⟼ (a \in Vtx (g), b \in Vtx (g) ⟼ \{w \in (a (n WWalksNOn g) b) \| \exists f f (a SPathsOn (g) b) w\}))$

Metamath Proof Explorer

Definition df-wspthsnon

Detailed syntax breakdown