Description: The set of s-walks of edges (in a hypergraph). (Contributed by AV, 4-Jan-2021)
Ref | Expression | ||
---|---|---|---|
Hypothesis | ewlksfval.i | |
|
Assertion | ewlksfval | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ewlksfval.i | |
|
2 | df-ewlks | |
|
3 | 2 | a1i | |
4 | fvexd | |
|
5 | simpr | |
|
6 | fveq2 | |
|
7 | 6 | adantr | |
8 | 7 | adantr | |
9 | 5 8 | eqtrd | |
10 | 9 | dmeqd | |
11 | wrdeq | |
|
12 | 10 11 | syl | |
13 | 12 | eleq2d | |
14 | simpr | |
|
15 | 14 | adantr | |
16 | 9 | fveq1d | |
17 | 9 | fveq1d | |
18 | 16 17 | ineq12d | |
19 | 18 | fveq2d | |
20 | 15 19 | breq12d | |
21 | 20 | ralbidv | |
22 | 13 21 | anbi12d | |
23 | 4 22 | sbcied | |
24 | 23 | abbidv | |
25 | 24 | adantl | |
26 | elex | |
|
27 | 26 | adantr | |
28 | simpr | |
|
29 | df-rab | |
|
30 | fvex | |
|
31 | 30 | dmex | |
32 | 31 | wrdexi | |
33 | 32 | rabex | |
34 | 33 | a1i | |
35 | 29 34 | eqeltrrid | |
36 | 3 25 27 28 35 | ovmpod | |
37 | 1 | eqcomi | |
38 | 37 | a1i | |
39 | 38 | dmeqd | |
40 | wrdeq | |
|
41 | 39 40 | syl | |
42 | 41 | eleq2d | |
43 | 38 | fveq1d | |
44 | 38 | fveq1d | |
45 | 43 44 | ineq12d | |
46 | 45 | fveq2d | |
47 | 46 | breq2d | |
48 | 47 | ralbidv | |
49 | 42 48 | anbi12d | |
50 | 49 | abbidv | |
51 | 36 50 | eqtrd | |