Metamath Proof Explorer

Theorem infxrge0glb

Description: The infimum of a set of nonnegative extended reals is the greatest 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 infxrge0glb 
|- ( ph -> ( inf ( A , ( 0 [,] +oo ) , < ) < B <-> E. x e. A x < B ) )

Proof

Step Hyp Ref Expression
1 infxrge0glb.a 
 |-  ( ph -> A C_ ( 0 [,] +oo ) )
2 infxrge0glb.b 
 |-  ( ph -> B e. ( 0 [,] +oo ) )
3 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
4 xrltso 
 |-  < Or RR*
5 soss 
 |-  ( ( 0 [,] +oo ) C_ RR* -> ( < Or RR* -> < Or ( 0 [,] +oo ) ) )
6 3 4 5 mp2 
 |-  < Or ( 0 [,] +oo )
7 6 a1i 
 |-  ( ph -> < Or ( 0 [,] +oo ) )
8 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 ) ) )
9 1 8 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 ) ) )
10 7 9 1 infglbb 
 |-  ( ( ph /\ B e. ( 0 [,] +oo ) ) -> ( inf ( A , ( 0 [,] +oo ) , < ) < B <-> E. z e. A z < B ) )
11 2 10 mpdan 
 |-  ( ph -> ( inf ( A , ( 0 [,] +oo ) , < ) < B <-> E. z e. A z < B ) )
12 breq1 
 |-  ( x = z -> ( x < B <-> z < B ) )
13 12 cbvrexvw 
 |-  ( E. x e. A x < B <-> E. z e. A z < B )
14 11 13 bitr4di 
 |-  ( ph -> ( inf ( A , ( 0 [,] +oo ) , < ) < B <-> E. x e. A x < B ) )