Description: Conditions for a function (sequence of hyperedges) to be an s-walk of edges. (Contributed by AV, 4-Jan-2021)
Ref | Expression | ||
---|---|---|---|
Hypothesis | ewlksfval.i | |
|
Assertion | isewlk | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ewlksfval.i | |
|
2 | 1 | ewlksfval | |
3 | 2 | 3adant3 | |
4 | 3 | eleq2d | |
5 | eleq1 | |
|
6 | fveq2 | |
|
7 | 6 | oveq2d | |
8 | fveq1 | |
|
9 | 8 | fveq2d | |
10 | fveq1 | |
|
11 | 10 | fveq2d | |
12 | 9 11 | ineq12d | |
13 | 12 | fveq2d | |
14 | 13 | breq2d | |
15 | 7 14 | raleqbidv | |
16 | 5 15 | anbi12d | |
17 | 16 | elabg | |
18 | 17 | 3ad2ant3 | |
19 | 4 18 | bitrd | |