This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) } ) )