Description: A word over the set of vertices representing a walk (in an undirected graph). (Contributed by Alexander van der Vekens, 15-Jul-2018) (Revised by AV, 8-Apr-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | wwlks.v | |
|
wwlks.e | |
||
Assertion | iswwlks | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wwlks.v | |
|
2 | wwlks.e | |
|
3 | neeq1 | |
|
4 | fveq2 | |
|
5 | 4 | oveq1d | |
6 | 5 | oveq2d | |
7 | fveq1 | |
|
8 | fveq1 | |
|
9 | 7 8 | preq12d | |
10 | 9 | eleq1d | |
11 | 6 10 | raleqbidv | |
12 | 3 11 | anbi12d | |
13 | 12 | elrab | |
14 | 1 2 | wwlks | |
15 | 14 | eleq2i | |
16 | 3anan12 | |
|
17 | 13 15 16 | 3bitr4i | |