Description: Any subset of nonnegative extended reals has an infimum. (Contributed by Thierry Arnoux, 16-Sep-2019) (Revised by AV, 4-Oct-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | xrge0infss | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssel2 | |
|
2 | 0xr | |
|
3 | pnfxr | |
|
4 | iccgelb | |
|
5 | 2 3 4 | mp3an12 | |
6 | eliccxr | |
|
7 | xrlenlt | |
|
8 | 2 6 7 | sylancr | |
9 | 5 8 | mpbid | |
10 | 1 9 | syl | |
11 | 10 | ralrimiva | |
12 | 11 | ad3antrrr | |
13 | iccssxr | |
|
14 | ssralv | |
|
15 | 13 14 | ax-mp | |
16 | simplll | |
|
17 | 2 | a1i | |
18 | simplr | |
|
19 | 13 18 | sselid | |
20 | simpllr | |
|
21 | simpr | |
|
22 | 16 17 19 20 21 | xrlelttrd | |
23 | 22 | ex | |
24 | 23 | imim1d | |
25 | 24 | ralimdva | |
26 | 15 25 | syl5 | |
27 | 26 | adantll | |
28 | 27 | imp | |
29 | 28 | adantrl | |
30 | 29 | an32s | |
31 | 0e0iccpnf | |
|
32 | breq2 | |
|
33 | 32 | notbid | |
34 | 33 | ralbidv | |
35 | breq1 | |
|
36 | 35 | imbi1d | |
37 | 36 | ralbidv | |
38 | 34 37 | anbi12d | |
39 | 38 | rspcev | |
40 | 31 39 | mpan | |
41 | 12 30 40 | syl2anc | |
42 | simpllr | |
|
43 | simpr | |
|
44 | elxrge0 | |
|
45 | 42 43 44 | sylanbrc | |
46 | 15 | a1i | |
47 | 46 | anim2d | |
48 | 47 | adantr | |
49 | 48 | imp | |
50 | 49 | adantr | |
51 | breq2 | |
|
52 | 51 | notbid | |
53 | 52 | ralbidv | |
54 | breq1 | |
|
55 | 54 | imbi1d | |
56 | 55 | ralbidv | |
57 | 53 56 | anbi12d | |
58 | 57 | rspcev | |
59 | 45 50 58 | syl2anc | |
60 | simplr | |
|
61 | 2 | a1i | |
62 | xrletri | |
|
63 | 60 61 62 | syl2anc | |
64 | 41 59 63 | mpjaodan | |
65 | sstr | |
|
66 | 13 65 | mpan2 | |
67 | xrinfmss | |
|
68 | 66 67 | syl | |
69 | 64 68 | r19.29a | |