Metamath Proof Explorer


Theorem upwlksfval

Description: The set of simple walks (in an undirected graph). (Contributed by Alexander van der Vekens, 19-Oct-2017) (Revised by AV, 28-Dec-2020)

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

Proof

Step Hyp Ref Expression
1 upwlksfval.v V = Vtx G
2 upwlksfval.i I = iEdg G
3 df-upwlks UPWalks = g V f p | f Word dom iEdg g p : 0 f Vtx g k 0 ..^ f iEdg g f k = p k p k + 1
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 p k + 1 I f k = p k p k + 1
15 14 ralbidv g = G k 0 ..^ f iEdg g f k = p k p k + 1 k 0 ..^ f I f k = p k p k + 1
16 9 12 15 3anbi123d g = G f Word dom iEdg g p : 0 f Vtx g k 0 ..^ f iEdg g f k = p k p k + 1 f Word dom I p : 0 f V k 0 ..^ f I f k = p k p k + 1
17 16 opabbidv g = G f p | f Word dom iEdg g p : 0 f Vtx g k 0 ..^ f iEdg g f k = p k p k + 1 = f p | f Word dom I p : 0 f V k 0 ..^ f I f k = p k p k + 1
18 elex G W G V
19 3anass f Word dom I p : 0 f V k 0 ..^ f I f k = p k p k + 1 f Word dom I p : 0 f V k 0 ..^ f I f k = p k p k + 1
20 19 opabbii f p | f Word dom I p : 0 f V k 0 ..^ f I f k = p k p k + 1 = f p | f Word dom I p : 0 f V k 0 ..^ f I f k = p k p k + 1
21 2 fvexi I V
22 21 dmex dom I V
23 wrdexg dom I V Word dom I V
24 22 23 mp1i G W Word dom I V
25 ovex 0 f V
26 1 fvexi V V
27 26 a1i G W f Word dom I V V
28 mapex 0 f V V V p | p : 0 f V V
29 25 27 28 sylancr G W f Word dom I p | p : 0 f V V
30 simpl p : 0 f V k 0 ..^ f I f k = p k p k + 1 p : 0 f V
31 30 ss2abi p | p : 0 f V k 0 ..^ f I f k = p k p k + 1 p | p : 0 f V
32 31 a1i G W f Word dom I p | p : 0 f V k 0 ..^ f I f k = p k p k + 1 p | p : 0 f V
33 29 32 ssexd G W f Word dom I p | p : 0 f V k 0 ..^ f I f k = p k p k + 1 V
34 24 33 opabex3d G W f p | f Word dom I p : 0 f V k 0 ..^ f I f k = p k p k + 1 V
35 20 34 eqeltrid G W f p | f Word dom I p : 0 f V k 0 ..^ f I f k = p k p k + 1 V
36 3 17 18 35 fvmptd3 G W UPWalks G = f p | f Word dom I p : 0 f V k 0 ..^ f I f k = p k p k + 1