Description: Construct lexicographic order on a function space based on a well-ordering of the indices and a total ordering of the values.
Without totality on the values or least differing indices, the best we can prove here is a partial order. (Contributed by Stefan O'Rear, 18-Jan-2015) (Revised by AV, 21-Jul-2024)
Ref | Expression | ||
---|---|---|---|
Hypothesis | wemapso.t | |
|
Assertion | wemappo | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wemapso.t | |
|
2 | simpllr | |
|
3 | elmapi | |
|
4 | 3 | adantl | |
5 | 4 | ffvelrnda | |
6 | poirr | |
|
7 | 2 5 6 | syl2anc | |
8 | 7 | intnanrd | |
9 | 8 | nrexdv | |
10 | 1 | wemaplem1 | |
11 | 10 | el2v | |
12 | 9 11 | sylnibr | |
13 | simplr1 | |
|
14 | simplr2 | |
|
15 | simplr3 | |
|
16 | simplll | |
|
17 | simpllr | |
|
18 | simprl | |
|
19 | simprr | |
|
20 | 1 13 14 15 16 17 18 19 | wemaplem3 | |
21 | 20 | ex | |
22 | 12 21 | ispod | |