Description: Value of the lexicographic order on a sequence space. (Contributed by Stefan O'Rear, 18-Jan-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | wemapso.t | |
|
Assertion | wemaplem1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wemapso.t | |
|
2 | fveq1 | |
|
3 | fveq1 | |
|
4 | 2 3 | breqan12d | |
5 | fveq1 | |
|
6 | fveq1 | |
|
7 | 5 6 | eqeqan12d | |
8 | 7 | imbi2d | |
9 | 8 | ralbidv | |
10 | 4 9 | anbi12d | |
11 | 10 | rexbidv | |
12 | fveq2 | |
|
13 | fveq2 | |
|
14 | 12 13 | breq12d | |
15 | breq2 | |
|
16 | 15 | imbi1d | |
17 | 16 | ralbidv | |
18 | breq1 | |
|
19 | fveq2 | |
|
20 | fveq2 | |
|
21 | 19 20 | eqeq12d | |
22 | 18 21 | imbi12d | |
23 | 22 | cbvralvw | |
24 | 17 23 | bitrdi | |
25 | 14 24 | anbi12d | |
26 | 25 | cbvrexvw | |
27 | 11 26 | bitrdi | |
28 | 27 1 | brabga | |