# 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 ${⊢}\mathrm{WalksOn}=\left({g}\in \mathrm{V}⟼\left({a}\in \mathrm{Vtx}\left({g}\right),{b}\in \mathrm{Vtx}\left({g}\right)⟼\left\{⟨{f},{p}⟩|\left({f}\mathrm{Walks}\left({g}\right){p}\wedge {p}\left(0\right)={a}\wedge {p}\left(\left|{f}\right|\right)={b}\right)\right\}\right)\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cwlkson ${class}\mathrm{WalksOn}$
1 vg ${setvar}{g}$
2 cvv ${class}\mathrm{V}$
3 va ${setvar}{a}$
4 cvtx ${class}\mathrm{Vtx}$
5 1 cv ${setvar}{g}$
6 5 4 cfv ${class}\mathrm{Vtx}\left({g}\right)$
7 vb ${setvar}{b}$
8 vf ${setvar}{f}$
9 vp ${setvar}{p}$
10 8 cv ${setvar}{f}$
11 cwlks ${class}\mathrm{Walks}$
12 5 11 cfv ${class}\mathrm{Walks}\left({g}\right)$
13 9 cv ${setvar}{p}$
14 10 13 12 wbr ${wff}{f}\mathrm{Walks}\left({g}\right){p}$
15 cc0 ${class}0$
16 15 13 cfv ${class}{p}\left(0\right)$
17 3 cv ${setvar}{a}$
18 16 17 wceq ${wff}{p}\left(0\right)={a}$
19 chash ${class}\left|.\right|$
20 10 19 cfv ${class}\left|{f}\right|$
21 20 13 cfv ${class}{p}\left(\left|{f}\right|\right)$
22 7 cv ${setvar}{b}$
23 21 22 wceq ${wff}{p}\left(\left|{f}\right|\right)={b}$
24 14 18 23 w3a ${wff}\left({f}\mathrm{Walks}\left({g}\right){p}\wedge {p}\left(0\right)={a}\wedge {p}\left(\left|{f}\right|\right)={b}\right)$
25 24 8 9 copab ${class}\left\{⟨{f},{p}⟩|\left({f}\mathrm{Walks}\left({g}\right){p}\wedge {p}\left(0\right)={a}\wedge {p}\left(\left|{f}\right|\right)={b}\right)\right\}$
26 3 7 6 6 25 cmpo ${class}\left({a}\in \mathrm{Vtx}\left({g}\right),{b}\in \mathrm{Vtx}\left({g}\right)⟼\left\{⟨{f},{p}⟩|\left({f}\mathrm{Walks}\left({g}\right){p}\wedge {p}\left(0\right)={a}\wedge {p}\left(\left|{f}\right|\right)={b}\right)\right\}\right)$
27 1 2 26 cmpt ${class}\left({g}\in \mathrm{V}⟼\left({a}\in \mathrm{Vtx}\left({g}\right),{b}\in \mathrm{Vtx}\left({g}\right)⟼\left\{⟨{f},{p}⟩|\left({f}\mathrm{Walks}\left({g}\right){p}\wedge {p}\left(0\right)={a}\wedge {p}\left(\left|{f}\right|\right)={b}\right)\right\}\right)\right)$
28 0 27 wceq ${wff}\mathrm{WalksOn}=\left({g}\in \mathrm{V}⟼\left({a}\in \mathrm{Vtx}\left({g}\right),{b}\in \mathrm{Vtx}\left({g}\right)⟼\left\{⟨{f},{p}⟩|\left({f}\mathrm{Walks}\left({g}\right){p}\wedge {p}\left(0\right)={a}\wedge {p}\left(\left|{f}\right|\right)={b}\right)\right\}\right)\right)$