Description: If x is less than y then a strictly monotone function's value will be strictly less at x than at y . (Contributed by Andrew Salmon, 22-Nov-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | smoel | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | smodm | |
|
2 | ordtr1 | |
|
3 | 2 | ancomsd | |
4 | 3 | expdimp | |
5 | 1 4 | sylan | |
6 | df-smo | |
|
7 | eleq1 | |
|
8 | fveq2 | |
|
9 | 8 | eleq1d | |
10 | 7 9 | imbi12d | |
11 | eleq2 | |
|
12 | fveq2 | |
|
13 | 12 | eleq2d | |
14 | 11 13 | imbi12d | |
15 | 10 14 | rspc2v | |
16 | 15 | ancoms | |
17 | 16 | com12 | |
18 | 17 | 3ad2ant3 | |
19 | 6 18 | sylbi | |
20 | 19 | expdimp | |
21 | 5 20 | syld | |
22 | 21 | pm2.43d | |
23 | 22 | 3impia | |