Definition df-wlkon 25291

Description: Define the collection of walks with particular endpoints (in an un- directed graph). 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.)

Assertion

Ref	Expression
df-wlkon	|- WalkOn = ( v e. _V , e e. _V |-> ( a e. v , b e. v |-> { <. f , p >. | ( f ( v Walks e ) p /\ ( p ` 0 ) = a /\ ( p ` ( # ` f ) ) = b ) } ) )

Distinct variable groups:   v, e, f, p   a, b, e, f, p, v

Detailed syntax breakdown of Definition df-wlkon

Step	Hyp	Ref	Expression
1		cwlkon 25279	. 2 class WalkOn
2		vv	. . 3 setvar v
3		ve	. . 3 setvar e
4		cvv 3057	. . 3 class _V
5		va	. . . 4 setvar a
6		vb	. . . 4 setvar b
7	2	cv 1454	. . . 4 class v
8		vf	. . . . . . . 8 setvar f
9	8	cv 1454	. . . . . . 7 class f
10		vp	. . . . . . . 8 setvar p
11	10	cv 1454	. . . . . . 7 class p
12	3	cv 1454	. . . . . . . 8 class e
13		cwalk 25275	. . . . . . . 8 class Walks
14	7, 12, 13	co 6315	. . . . . . 7 class ( v Walks e )
15	9, 11, 14	wbr 4416	. . . . . 6 wff f ( v Walks e ) p
16		cc0 9565	. . . . . . . 8 class 0
17	16, 11	cfv 5601	. . . . . . 7 class ( p ` 0 )
18	5	cv 1454	. . . . . . 7 class a
19	17, 18	wceq 1455	. . . . . 6 wff ( p ` 0 ) = a
20		chash 12547	. . . . . . . . 9 class #
21	9, 20	cfv 5601	. . . . . . . 8 class ( # ` f )
22	21, 11	cfv 5601	. . . . . . 7 class ( p ` ( # ` f ) )
23	6	cv 1454	. . . . . . 7 class b
24	22, 23	wceq 1455	. . . . . 6 wff ( p ` ( # ` f ) ) = b
25	15, 19, 24	w3a 991	. . . . 5 wff ( f ( v Walks e ) p /\ ( p ` 0 ) = a /\ ( p ` ( # ` f ) ) = b )
26	25, 8, 10	copab 4474	. . . 4 class { <. f , p >. | ( f ( v Walks e ) p /\ ( p ` 0 ) = a /\ ( p ` ( # ` f ) ) = b ) }
27	5, 6, 7, 7, 26	cmpt2 6317	. . 3 class ( a e. v , b e. v |-> { <. f , p >. | ( f ( v Walks e ) p /\ ( p ` 0 ) = a /\ ( p ` ( # ` f ) ) = b ) } )
28	2, 3, 4, 4, 27	cmpt2 6317	. 2 class ( v e. _V , e e. _V |-> ( a e. v , b e. v |-> { <. f , p >. | ( f ( v Walks e ) p /\ ( p ` 0 ) = a /\ ( p ` ( # ` f ) ) = b ) } ) )
29	1, 28	wceq 1455	1 wff WalkOn = ( v e. _V , e e. _V |-> ( a e. v , b e. v |-> { <. f , p >. | ( f ( v Walks e ) p /\ ( p ` 0 ) = a /\ ( p ` ( # ` f ) ) = b ) } ) )

This definition is referenced by:  wlkon  25310  wlkonprop  25312