This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem infxrge0gelb

Description: The infimum of a set of nonnegative extended reals is greater than or equal to a lower bound. (Contributed by Thierry Arnoux, 19-Jul-2020) (Revised by AV, 4-Oct-2020)

Ref Expression
Hypotheses infxrge0glb.a 
|- ( ph -> A C_ ( 0 [,] +oo ) )
infxrge0glb.b 
|- ( ph -> B e. ( 0 [,] +oo ) )
Assertion infxrge0gelb 
|- ( ph -> ( B <_ inf ( A , ( 0 [,] +oo ) , < ) <-> A. x e. A B <_ x ) )

Proof

Step Hyp Ref Expression
1 infxrge0glb.a 
 |-  ( ph -> A C_ ( 0 [,] +oo ) )
2 infxrge0glb.b 
 |-  ( ph -> B e. ( 0 [,] +oo ) )
3 1 2 infxrge0glb 
 |-  ( ph -> ( inf ( A , ( 0 [,] +oo ) , < ) < B <-> E. x e. A x < B ) )
4 3 notbid 
 |-  ( ph -> ( -. inf ( A , ( 0 [,] +oo ) , < ) < B <-> -. E. x e. A x < B ) )
5 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
6 5 2 sselid 
 |-  ( ph -> B e. RR* )
7 xrltso 
 |-  < Or RR*
8 soss 
 |-  ( ( 0 [,] +oo ) C_ RR* -> ( < Or RR* -> < Or ( 0 [,] +oo ) ) )
9 5 7 8 mp2 
 |-  < Or ( 0 [,] +oo )
10 9 a1i 
 |-  ( ph -> < Or ( 0 [,] +oo ) )
11 xrge0infss 
 |-  ( A C_ ( 0 [,] +oo ) -> E. x e. ( 0 [,] +oo ) ( A. y e. A -. y < x /\ A. y e. ( 0 [,] +oo ) ( x < y -> E. z e. A z < y ) ) )
12 1 11 syl 
 |-  ( ph -> E. x e. ( 0 [,] +oo ) ( A. y e. A -. y < x /\ A. y e. ( 0 [,] +oo ) ( x < y -> E. z e. A z < y ) ) )
13 10 12 infcl 
 |-  ( ph -> inf ( A , ( 0 [,] +oo ) , < ) e. ( 0 [,] +oo ) )
14 5 13 sselid 
 |-  ( ph -> inf ( A , ( 0 [,] +oo ) , < ) e. RR* )
15 6 14 xrlenltd 
 |-  ( ph -> ( B <_ inf ( A , ( 0 [,] +oo ) , < ) <-> -. inf ( A , ( 0 [,] +oo ) , < ) < B ) )
16 6 adantr 
 |-  ( ( ph /\ x e. A ) -> B e. RR* )
17 1 5 sstrdi 
 |-  ( ph -> A C_ RR* )
18 17 sselda 
 |-  ( ( ph /\ x e. A ) -> x e. RR* )
19 16 18 xrlenltd 
 |-  ( ( ph /\ x e. A ) -> ( B <_ x <-> -. x < B ) )
20 19 ralbidva 
 |-  ( ph -> ( A. x e. A B <_ x <-> A. x e. A -. x < B ) )
21 ralnex 
 |-  ( A. x e. A -. x < B <-> -. E. x e. A x < B )
22 20 21 bitrdi 
 |-  ( ph -> ( A. x e. A B <_ x <-> -. E. x e. A x < B ) )
23 4 15 22 3bitr4d 
 |-  ( ph -> ( B <_ inf ( A , ( 0 [,] +oo ) , < ) <-> A. x e. A B <_ x ) )