Metamath Proof Explorer


Theorem wksfval

Description: The set of walks (in an undirected graph). (Contributed by AV, 30-Dec-2020)

Ref Expression
Hypotheses wksfval.v V = Vtx G
wksfval.i I = iEdg G
Assertion wksfval G W Walks G = f p | f Word dom I p : 0 f V k 0 ..^ f if- p k = p k + 1 I f k = p k p k p k + 1 I f k

Proof

Step Hyp Ref Expression
1 wksfval.v V = Vtx G
2 wksfval.i I = iEdg G
3 df-wlks Walks = g V f p | f Word dom iEdg g p : 0 f Vtx g k 0 ..^ f if- p k = p k + 1 iEdg g f k = p k p k p k + 1 iEdg g f k
4 fveq2 g = G iEdg g = iEdg G
5 4 2 eqtr4di g = G iEdg g = I
6 5 dmeqd g = G dom iEdg g = dom I
7 wrdeq dom iEdg g = dom I Word dom iEdg g = Word dom I
8 6 7 syl g = G Word dom iEdg g = Word dom I
9 8 eleq2d g = G f Word dom iEdg g f Word dom I
10 fveq2 g = G Vtx g = Vtx G
11 10 1 eqtr4di g = G Vtx g = V
12 11 feq3d g = G p : 0 f Vtx g p : 0 f V
13 5 fveq1d g = G iEdg g f k = I f k
14 13 eqeq1d g = G iEdg g f k = p k I f k = p k
15 13 sseq2d g = G p k p k + 1 iEdg g f k p k p k + 1 I f k
16 14 15 ifpbi23d g = G if- p k = p k + 1 iEdg g f k = p k p k p k + 1 iEdg g f k if- p k = p k + 1 I f k = p k p k p k + 1 I f k
17 16 ralbidv g = G k 0 ..^ f if- p k = p k + 1 iEdg g f k = p k p k p k + 1 iEdg g f k k 0 ..^ f if- p k = p k + 1 I f k = p k p k p k + 1 I f k
18 9 12 17 3anbi123d g = G f Word dom iEdg g p : 0 f Vtx g k 0 ..^ f if- p k = p k + 1 iEdg g f k = p k p k p k + 1 iEdg g f k f Word dom I p : 0 f V k 0 ..^ f if- p k = p k + 1 I f k = p k p k p k + 1 I f k
19 18 opabbidv g = G f p | f Word dom iEdg g p : 0 f Vtx g k 0 ..^ f if- p k = p k + 1 iEdg g f k = p k p k p k + 1 iEdg g f k = f p | f Word dom I p : 0 f V k 0 ..^ f if- p k = p k + 1 I f k = p k p k p k + 1 I f k
20 elex G W G V
21 3anass f Word dom I p : 0 f V k 0 ..^ f if- p k = p k + 1 I f k = p k p k p k + 1 I f k f Word dom I p : 0 f V k 0 ..^ f if- p k = p k + 1 I f k = p k p k p k + 1 I f k
22 21 opabbii f p | f Word dom I p : 0 f V k 0 ..^ f if- p k = p k + 1 I f k = p k p k p k + 1 I f k = f p | f Word dom I p : 0 f V k 0 ..^ f if- p k = p k + 1 I f k = p k p k p k + 1 I f k
23 2 fvexi I V
24 23 dmex dom I V
25 wrdexg dom I V Word dom I V
26 24 25 mp1i G W Word dom I V
27 ovex 0 f V
28 1 fvexi V V
29 28 a1i G W f Word dom I V V
30 mapex 0 f V V V p | p : 0 f V V
31 27 29 30 sylancr G W f Word dom I p | p : 0 f V V
32 simpl p : 0 f V k 0 ..^ f if- p k = p k + 1 I f k = p k p k p k + 1 I f k p : 0 f V
33 32 ss2abi p | p : 0 f V k 0 ..^ f if- p k = p k + 1 I f k = p k p k p k + 1 I f k p | p : 0 f V
34 33 a1i G W f Word dom I p | p : 0 f V k 0 ..^ f if- p k = p k + 1 I f k = p k p k p k + 1 I f k p | p : 0 f V
35 31 34 ssexd G W f Word dom I p | p : 0 f V k 0 ..^ f if- p k = p k + 1 I f k = p k p k p k + 1 I f k V
36 26 35 opabex3d G W f p | f Word dom I p : 0 f V k 0 ..^ f if- p k = p k + 1 I f k = p k p k p k + 1 I f k V
37 22 36 eqeltrid G W f p | f Word dom I p : 0 f V k 0 ..^ f if- p k = p k + 1 I f k = p k p k p k + 1 I f k V
38 3 19 20 37 fvmptd3 G W Walks G = f p | f Word dom I p : 0 f V k 0 ..^ f if- p k = p k + 1 I f k = p k p k p k + 1 I f k