Definition df-wlkson 26496

Description: Define the collection of walks with particular endpoints (in a hypergraph). The predicate F ( A (WalksOn ` G ) 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 26553. 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.)

Assertion

Ref	Expression
df-wlkson	|- WalksOn = ( g e. _V |-> ( a e. (Vtx ` g ) , b e. (Vtx ` g ) |-> { <. f , p >. | ( f (Walks ` g ) p /\ ( p ` 0 ) = a /\ ( p ` ( # ` f ) ) = b ) } ) )

Distinct variable groups:   f, g, p   a, b, f, g, p

Detailed syntax breakdown of Definition df-wlkson

Step	Hyp	Ref	Expression
1		cwlkson 26493	. 2 class WalksOn
2		vg	. . 3 setvar g
3		cvv 3200	. . 3 class _V
4		va	. . . 4 setvar a
5		vb	. . . 4 setvar b
6	2	cv 1482	. . . . 5 class g
7		cvtx 25874	. . . . 5 class Vtx
8	6, 7	cfv 5888	. . . 4 class (Vtx ` g )
9		vf	. . . . . . . 8 setvar f
10	9	cv 1482	. . . . . . 7 class f
11		vp	. . . . . . . 8 setvar p
12	11	cv 1482	. . . . . . 7 class p
13		cwlks 26492	. . . . . . . 8 class Walks
14	6, 13	cfv 5888	. . . . . . 7 class (Walks ` g )
15	10, 12, 14	wbr 4653	. . . . . 6 wff f (Walks ` g ) p
16		cc0 9936	. . . . . . . 8 class 0
17	16, 12	cfv 5888	. . . . . . 7 class ( p ` 0 )
18	4	cv 1482	. . . . . . 7 class a
19	17, 18	wceq 1483	. . . . . 6 wff ( p ` 0 ) = a
20		chash 13117	. . . . . . . . 9 class #
21	10, 20	cfv 5888	. . . . . . . 8 class ( # ` f )
22	21, 12	cfv 5888	. . . . . . 7 class ( p ` ( # ` f ) )
23	5	cv 1482	. . . . . . 7 class b
24	22, 23	wceq 1483	. . . . . 6 wff ( p ` ( # ` f ) ) = b
25	15, 19, 24	w3a 1037	. . . . 5 wff ( f (Walks ` g ) p /\ ( p ` 0 ) = a /\ ( p ` ( # ` f ) ) = b )
26	25, 9, 11	copab 4712	. . . 4 class { <. f , p >. | ( f (Walks ` g ) p /\ ( p ` 0 ) = a /\ ( p ` ( # ` f ) ) = b ) }
27	4, 5, 8, 8, 26	cmpt2 6652	. . 3 class ( a e. (Vtx ` g ) , b e. (Vtx ` g ) |-> { <. f , p >. | ( f (Walks ` g ) p /\ ( p ` 0 ) = a /\ ( p ` ( # ` f ) ) = b ) } )
28	2, 3, 27	cmpt 4729	. 2 class ( g e. _V |-> ( a e. (Vtx ` g ) , b e. (Vtx ` g ) |-> { <. f , p >. | ( f (Walks ` g ) p /\ ( p ` 0 ) = a /\ ( p ` ( # ` f ) ) = b ) } ) )
29	1, 28	wceq 1483	1 wff WalksOn = ( g e. _V |-> ( a e. (Vtx ` g ) , b e. (Vtx ` g ) |-> { <. f , p >. | ( f (Walks ` g ) p /\ ( p ` 0 ) = a /\ ( p ` ( # ` f ) ) = b ) } ) )

This definition is referenced by:  wlkson  26552  wlkonprop  26554