Definition 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 e. _V |-> ( a e. ( Vtx ` g ) , b e. ( Vtx ` g ) |-> { <. f , p >. | ( f ( Walks ` g ) p /\ ( p ` 0 ) = a /\ ( p ` ( # ` f ) ) = b ) } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cwlkson	|- WalksOn
1		vg	|- g
2		cvv	|- _V
3		va	|- a
4		cvtx	|- Vtx
5	1	cv	|- g
6	5 4	cfv	|- ( Vtx ` g )
7		vb	|- b
8		vf	|- f
9		vp	|- p
10	8	cv	|- f
11		cwlks	|- Walks
12	5 11	cfv	|- ( Walks ` g )
13	9	cv	|- p
14	10 13 12	wbr	|- f ( Walks ` g ) p
15		cc0	|- 0
16	15 13	cfv	|- ( p ` 0 )
17	3	cv	|- a
18	16 17	wceq	|- ( p ` 0 ) = a
19		chash	|- #
20	10 19	cfv	|- ( # ` f )
21	20 13	cfv	|- ( p ` ( # ` f ) )
22	7	cv	|- b
23	21 22	wceq	|- ( p ` ( # ` f ) ) = b
24	14 18 23	w3a	|- ( f ( Walks ` g ) p /\ ( p ` 0 ) = a /\ ( p ` ( # ` f ) ) = b )
25	24 8 9	copab	|- { <. f , p >. | ( f ( Walks ` g ) p /\ ( p ` 0 ) = a /\ ( p ` ( # ` f ) ) = b ) }
26	3 7 6 6 25	cmpo	|- ( a e. ( Vtx ` g ) , b e. ( Vtx ` g ) |-> { <. f , p >. | ( f ( Walks ` g ) p /\ ( p ` 0 ) = a /\ ( p ` ( # ` f ) ) = b ) } )
27	1 2 26	cmpt	|- ( g e. _V |-> ( a e. ( Vtx ` g ) , b e. ( Vtx ` g ) |-> { <. f , p >. | ( f ( Walks ` g ) p /\ ( p ` 0 ) = a /\ ( p ` ( # ` f ) ) = b ) } ) )
28	0 27	wceq	|- WalksOn = ( g e. _V |-> ( a e. ( Vtx ` g ) , b e. ( Vtx ` g ) |-> { <. f , p >. | ( f ( Walks ` g ) p /\ ( p ` 0 ) = a /\ ( p ` ( # ` f ) ) = b ) } ) )