df-wlkson

Description: Define the collection of walks with particular endpoints (in a hypergraph). The predicate F ( A ( WalksOnG ) B ) P can be read as "The pair <. F , P >. represents a walk from vertex A to vertex B in a graph G ", see also iswlkon . This corresponds to the "x0-x(l)-walks", see Definition in Bollobas p. 5. (Contributed by Alexander van der Vekens and Mario Carneiro, 4-Oct-2017) (Revised by AV, 28-Dec-2020)

		Ref	Expression
	Assertion	df-wlkson	$⊢ WalksOn = (g \in V ⟼ (a \in Vtx (g), b \in Vtx (g) ⟼ \{⟨f, p⟩ \| (f Walks (g) p \land p (0) = a \land p (\|f\|) = b)\}))$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cwlkson	$class WalksOn$
1		vg	$setvar g$
2		cvv	$class V$
3		va	$setvar a$
4		cvtx	$class Vtx$
5	1	cv	$setvar g$
6	5 4	cfv	$class Vtx (g)$
7		vb	$setvar b$
8		vf	$setvar f$
9		vp	$setvar p$
10	8	cv	$setvar f$
11		cwlks	$class Walks$
12	5 11	cfv	$class Walks (g)$
13	9	cv	$setvar p$
14	10 13 12	wbr	$wff f Walks (g) p$
15		cc0	$class 0$
16	15 13	cfv	$class p (0)$
17	3	cv	$setvar a$
18	16 17	wceq	$wff p (0) = a$
19		chash	$class \|.\|$
20	10 19	cfv	$class \|f\|$
21	20 13	cfv	$class p (\|f\|)$
22	7	cv	$setvar b$
23	21 22	wceq	$wff p (\|f\|) = b$
24	14 18 23	w3a	$wff (f Walks (g) p \land p (0) = a \land p (\|f\|) = b)$
25	24 8 9	copab	$class \{⟨f, p⟩ \| (f Walks (g) p \land p (0) = a \land p (\|f\|) = b)\}$
26	3 7 6 6 25	cmpo	$class (a \in Vtx (g), b \in Vtx (g) ⟼ \{⟨f, p⟩ \| (f Walks (g) p \land p (0) = a \land p (\|f\|) = b)\})$
27	1 2 26	cmpt	$class (g \in V ⟼ (a \in Vtx (g), b \in Vtx (g) ⟼ \{⟨f, p⟩ \| (f Walks (g) p \land p (0) = a \land p (\|f\|) = b)\}))$
28	0 27	wceq	$wff WalksOn = (g \in V ⟼ (a \in Vtx (g), b \in Vtx (g) ⟼ \{⟨f, p⟩ \| (f Walks (g) p \land p (0) = a \land p (\|f\|) = b)\}))$

Metamath Proof Explorer

Definition df-wlkson

Detailed syntax breakdown