df-wwlksnon

Description: Define the collection of walks of a fixed length with particular endpoints as word over the set of vertices. (Contributed by Alexander van der Vekens, 15-Feb-2018) (Revised by AV, 11-May-2021)

		Ref	Expression
	Assertion	df-wwlksnon	$⊢ WWalksNOn = (n \in ℕ_{0}, g \in V ⟼ (a \in Vtx (g), b \in Vtx (g) ⟼ \{w \in (n WWalksN g) \| (w (0) = a \land w (n) = b)\}))$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cwwlksnon	$class WWalksNOn$
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	1	cv	$setvar n$
12		cwwlksn	$class WWalksN$
13	11 7 12	co	$class (n WWalksN g)$
14	10	cv	$setvar w$
15		cc0	$class 0$
16	15 14	cfv	$class w (0)$
17	5	cv	$setvar a$
18	16 17	wceq	$wff w (0) = a$
19	11 14	cfv	$class w (n)$
20	9	cv	$setvar b$
21	19 20	wceq	$wff w (n) = b$
22	18 21	wa	$wff (w (0) = a \land w (n) = b)$
23	22 10 13	crab	$class \{w \in (n WWalksN g) \| (w (0) = a \land w (n) = b)\}$
24	5 9 8 8 23	cmpo	$class (a \in Vtx (g), b \in Vtx (g) ⟼ \{w \in (n WWalksN g) \| (w (0) = a \land w (n) = b)\})$
25	1 3 2 4 24	cmpo	$class (n \in ℕ_{0}, g \in V ⟼ (a \in Vtx (g), b \in Vtx (g) ⟼ \{w \in (n WWalksN g) \| (w (0) = a \land w (n) = b)\}))$
26	0 25	wceq	$wff WWalksNOn = (n \in ℕ_{0}, g \in V ⟼ (a \in Vtx (g), b \in Vtx (g) ⟼ \{w \in (n WWalksN g) \| (w (0) = a \land w (n) = b)\}))$

Metamath Proof Explorer

Definition df-wwlksnon

Detailed syntax breakdown