Metamath Proof Explorer


Theorem xrge0infss

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 A0+∞x0+∞yA¬y<xy0+∞x<yzAz<y

Proof

Step Hyp Ref Expression
1 ssel2 A0+∞yAy0+∞
2 0xr 0*
3 pnfxr +∞*
4 iccgelb 0*+∞*y0+∞0y
5 2 3 4 mp3an12 y0+∞0y
6 eliccxr y0+∞y*
7 xrlenlt 0*y*0y¬y<0
8 2 6 7 sylancr y0+∞0y¬y<0
9 5 8 mpbid y0+∞¬y<0
10 1 9 syl A0+∞yA¬y<0
11 10 ralrimiva A0+∞yA¬y<0
12 11 ad3antrrr A0+∞w*yA¬y<wy*w<yzAz<yw0yA¬y<0
13 iccssxr 0+∞*
14 ssralv 0+∞*y*w<yzAz<yy0+∞w<yzAz<y
15 13 14 ax-mp y*w<yzAz<yy0+∞w<yzAz<y
16 simplll w*w0y0+∞0<yw*
17 2 a1i w*w0y0+∞0<y0*
18 simplr w*w0y0+∞0<yy0+∞
19 13 18 sselid w*w0y0+∞0<yy*
20 simpllr w*w0y0+∞0<yw0
21 simpr w*w0y0+∞0<y0<y
22 16 17 19 20 21 xrlelttrd w*w0y0+∞0<yw<y
23 22 ex w*w0y0+∞0<yw<y
24 23 imim1d w*w0y0+∞w<yzAz<y0<yzAz<y
25 24 ralimdva w*w0y0+∞w<yzAz<yy0+∞0<yzAz<y
26 15 25 syl5 w*w0y*w<yzAz<yy0+∞0<yzAz<y
27 26 adantll A0+∞w*w0y*w<yzAz<yy0+∞0<yzAz<y
28 27 imp A0+∞w*w0y*w<yzAz<yy0+∞0<yzAz<y
29 28 adantrl A0+∞w*w0yA¬y<wy*w<yzAz<yy0+∞0<yzAz<y
30 29 an32s A0+∞w*yA¬y<wy*w<yzAz<yw0y0+∞0<yzAz<y
31 0e0iccpnf 00+∞
32 breq2 x=0y<xy<0
33 32 notbid x=0¬y<x¬y<0
34 33 ralbidv x=0yA¬y<xyA¬y<0
35 breq1 x=0x<y0<y
36 35 imbi1d x=0x<yzAz<y0<yzAz<y
37 36 ralbidv x=0y0+∞x<yzAz<yy0+∞0<yzAz<y
38 34 37 anbi12d x=0yA¬y<xy0+∞x<yzAz<yyA¬y<0y0+∞0<yzAz<y
39 38 rspcev 00+∞yA¬y<0y0+∞0<yzAz<yx0+∞yA¬y<xy0+∞x<yzAz<y
40 31 39 mpan yA¬y<0y0+∞0<yzAz<yx0+∞yA¬y<xy0+∞x<yzAz<y
41 12 30 40 syl2anc A0+∞w*yA¬y<wy*w<yzAz<yw0x0+∞yA¬y<xy0+∞x<yzAz<y
42 simpllr A0+∞w*yA¬y<wy*w<yzAz<y0ww*
43 simpr A0+∞w*yA¬y<wy*w<yzAz<y0w0w
44 elxrge0 w0+∞w*0w
45 42 43 44 sylanbrc A0+∞w*yA¬y<wy*w<yzAz<y0ww0+∞
46 15 a1i A0+∞y*w<yzAz<yy0+∞w<yzAz<y
47 46 anim2d A0+∞yA¬y<wy*w<yzAz<yyA¬y<wy0+∞w<yzAz<y
48 47 adantr A0+∞w*yA¬y<wy*w<yzAz<yyA¬y<wy0+∞w<yzAz<y
49 48 imp A0+∞w*yA¬y<wy*w<yzAz<yyA¬y<wy0+∞w<yzAz<y
50 49 adantr A0+∞w*yA¬y<wy*w<yzAz<y0wyA¬y<wy0+∞w<yzAz<y
51 breq2 x=wy<xy<w
52 51 notbid x=w¬y<x¬y<w
53 52 ralbidv x=wyA¬y<xyA¬y<w
54 breq1 x=wx<yw<y
55 54 imbi1d x=wx<yzAz<yw<yzAz<y
56 55 ralbidv x=wy0+∞x<yzAz<yy0+∞w<yzAz<y
57 53 56 anbi12d x=wyA¬y<xy0+∞x<yzAz<yyA¬y<wy0+∞w<yzAz<y
58 57 rspcev w0+∞yA¬y<wy0+∞w<yzAz<yx0+∞yA¬y<xy0+∞x<yzAz<y
59 45 50 58 syl2anc A0+∞w*yA¬y<wy*w<yzAz<y0wx0+∞yA¬y<xy0+∞x<yzAz<y
60 simplr A0+∞w*yA¬y<wy*w<yzAz<yw*
61 2 a1i A0+∞w*yA¬y<wy*w<yzAz<y0*
62 xrletri w*0*w00w
63 60 61 62 syl2anc A0+∞w*yA¬y<wy*w<yzAz<yw00w
64 41 59 63 mpjaodan A0+∞w*yA¬y<wy*w<yzAz<yx0+∞yA¬y<xy0+∞x<yzAz<y
65 sstr A0+∞0+∞*A*
66 13 65 mpan2 A0+∞A*
67 xrinfmss A*w*yA¬y<wy*w<yzAz<y
68 66 67 syl A0+∞w*yA¬y<wy*w<yzAz<y
69 64 68 r19.29a A0+∞x0+∞yA¬y<xy0+∞x<yzAz<y