Description: Closed-below, open-above intervals of reals. (Contributed by ML, 26-Jul-2020)
Ref | Expression | ||
---|---|---|---|
Hypothesis | icorempo.1 | |
|
Assertion | icorempo | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | icorempo.1 | |
|
2 | df-ico | |
|
3 | 2 | reseq1i | |
4 | ressxr | |
|
5 | resmpo | |
|
6 | 4 4 5 | mp2an | |
7 | 3 6 | eqtri | |
8 | nfv | |
|
9 | nfrab1 | |
|
10 | nfrab1 | |
|
11 | rabid | |
|
12 | rexr | |
|
13 | nltmnf | |
|
14 | 12 13 | syl | |
15 | renemnf | |
|
16 | 15 | neneqd | |
17 | 14 16 | jca | |
18 | pm4.56 | |
|
19 | 17 18 | sylib | |
20 | mnfxr | |
|
21 | xrleloe | |
|
22 | 12 20 21 | sylancl | |
23 | 19 22 | mtbird | |
24 | breq2 | |
|
25 | 24 | notbid | |
26 | 23 25 | syl5ibrcom | |
27 | 26 | con2d | |
28 | rexr | |
|
29 | pnfnlt | |
|
30 | breq1 | |
|
31 | 30 | notbid | |
32 | 29 31 | syl5ibrcom | |
33 | 32 | con2d | |
34 | 28 33 | syl | |
35 | 27 34 | im2anan9 | |
36 | 35 | anim2d | |
37 | renepnf | |
|
38 | 37 | neneqd | |
39 | 38 | pm4.71i | |
40 | xrnemnf | |
|
41 | 40 | anbi1i | |
42 | df-ne | |
|
43 | 42 | anbi2i | |
44 | 43 | anbi1i | |
45 | pm5.61 | |
|
46 | 41 44 45 | 3bitr3i | |
47 | anass | |
|
48 | 39 46 47 | 3bitr2ri | |
49 | 36 48 | syl6ib | |
50 | 11 49 | syl5bi | |
51 | 11 | simprbi | |
52 | 51 | a1i | |
53 | 50 52 | jcad | |
54 | rabid | |
|
55 | 53 54 | syl6ibr | |
56 | rabss2 | |
|
57 | 4 56 | ax-mp | |
58 | 57 | sseli | |
59 | 55 58 | impbid1 | |
60 | 8 9 10 59 | eqrd | |
61 | 60 | mpoeq3ia | |
62 | 1 7 61 | 3eqtri | |