Description: Two ways to write a strictly increasing function on the reals. (Contributed by Mario Carneiro, 9-Sep-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | leiso | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-le | |
|
2 | 1 | ineq1i | |
3 | indif1 | |
|
4 | 2 3 | eqtri | |
5 | xpss12 | |
|
6 | 5 | anidms | |
7 | sseqin2 | |
|
8 | 6 7 | sylib | |
9 | 8 | difeq1d | |
10 | 4 9 | eqtr2id | |
11 | isoeq2 | |
|
12 | 10 11 | syl | |
13 | 1 | ineq1i | |
14 | indif1 | |
|
15 | 13 14 | eqtri | |
16 | xpss12 | |
|
17 | 16 | anidms | |
18 | sseqin2 | |
|
19 | 17 18 | sylib | |
20 | 19 | difeq1d | |
21 | 15 20 | eqtr2id | |
22 | isoeq3 | |
|
23 | 21 22 | syl | |
24 | 12 23 | sylan9bb | |
25 | isocnv2 | |
|
26 | eqid | |
|
27 | eqid | |
|
28 | 26 27 | isocnv3 | |
29 | 25 28 | bitri | |
30 | isores1 | |
|
31 | isores2 | |
|
32 | 30 31 | bitri | |
33 | 24 29 32 | 3bitr4g | |