Definition df-wlkon 23420

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 23408	. 2 class WalkOn
2		vv	. . 3 setvar v
3		ve	. . 3 setvar e
4		cvv 2971	. . 3 class _V
5		va	. . . 4 setvar a
6		vb	. . . 4 setvar b
7	2	cv 1368	. . . 4 class v
8		vf	. . . . . . . 8 setvar f
9	8	cv 1368	. . . . . . 7 class f
10		vp	. . . . . . . 8 setvar p
11	10	cv 1368	. . . . . . 7 class p
12	3	cv 1368	. . . . . . . 8 class e
13		cwalk 23404	. . . . . . . 8 class Walks
14	7, 12, 13	co 6090	. . . . . . 7 class ( v Walks e )
15	9, 11, 14	wbr 4291	. . . . . 6 wff f ( v Walks e ) p
16		cc0 9281	. . . . . . . 8 class 0
17	16, 11	cfv 5417	. . . . . . 7 class ( p ` 0 )
18	5	cv 1368	. . . . . . 7 class a
19	17, 18	wceq 1369	. . . . . 6 wff ( p ` 0 ) = a
20		chash 12102	. . . . . . . . 9 class #
21	9, 20	cfv 5417	. . . . . . . 8 class ( # ` f )
22	21, 11	cfv 5417	. . . . . . 7 class ( p ` ( # ` f ) )
23	6	cv 1368	. . . . . . 7 class b
24	22, 23	wceq 1369	. . . . . 6 wff ( p ` ( # ` f ) ) = b
25	15, 19, 24	w3a 965	. . . . 5 wff ( f ( v Walks e ) p /\ ( p ` 0 ) = a /\ ( p ` ( # ` f ) ) = b )
26	25, 8, 10	copab 4348	. . . 4 class { <. f , p >. | ( f ( v Walks e ) p /\ ( p ` 0 ) = a /\ ( p ` ( # ` f ) ) = b ) }
27	5, 6, 7, 7, 26	cmpt2 6092	. . 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 6092	. 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 1369	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  23428  wlkonprop  23430