Description: Define a function from open intervals to their endpoints. (Contributed by Mario Carneiro, 26-Mar-2015) (Revised by AV, 13-Sep-2020)
Ref | Expression | ||
---|---|---|---|
Hypothesis | ioorf.1 | |
|
Assertion | ioorf | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ioorf.1 | |
|
2 | ioof | |
|
3 | ffn | |
|
4 | ovelrn | |
|
5 | 2 3 4 | mp2b | |
6 | 0le0 | |
|
7 | df-br | |
|
8 | 6 7 | mpbi | |
9 | 0xr | |
|
10 | opelxpi | |
|
11 | 9 9 10 | mp2an | |
12 | 8 11 | elini | |
13 | 12 | a1i | |
14 | simplr | |
|
15 | 14 | infeq1d | |
16 | simplll | |
|
17 | simpllr | |
|
18 | simpr | |
|
19 | 18 | neqned | |
20 | 14 19 | eqnetrrd | |
21 | df-ioo | |
|
22 | idd | |
|
23 | xrltle | |
|
24 | idd | |
|
25 | xrltle | |
|
26 | 21 22 23 24 25 | ixxlb | |
27 | 16 17 20 26 | syl3anc | |
28 | 15 27 | eqtrd | |
29 | 14 | supeq1d | |
30 | 21 22 23 24 25 | ixxub | |
31 | 16 17 20 30 | syl3anc | |
32 | 29 31 | eqtrd | |
33 | 28 32 | opeq12d | |
34 | ioon0 | |
|
35 | 34 | ad2antrr | |
36 | 20 35 | mpbid | |
37 | xrltle | |
|
38 | 37 | ad2antrr | |
39 | 36 38 | mpd | |
40 | df-br | |
|
41 | 39 40 | sylib | |
42 | opelxpi | |
|
43 | 42 | ad2antrr | |
44 | 41 43 | elind | |
45 | 33 44 | eqeltrd | |
46 | 13 45 | ifclda | |
47 | 46 | ex | |
48 | 47 | rexlimivv | |
49 | 5 48 | sylbi | |
50 | 1 49 | fmpti | |