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

Metamath Proof Explorer

Theorem xrge0infssd

Description: Inequality deduction for infimum of a nonnegative extended real subset. (Contributed by Thierry Arnoux, 16-Sep-2019) (Revised by AV, 4-Oct-2020)

Ref Expression
Hypotheses xrge0infssd.1 
|- ( ph -> C C_ B )
xrge0infssd.2 
|- ( ph -> B C_ ( 0 [,] +oo ) )
Assertion xrge0infssd 
|- ( ph -> inf ( B , ( 0 [,] +oo ) , < ) <_ inf ( C , ( 0 [,] +oo ) , < ) )

Proof

Step Hyp Ref Expression
1 xrge0infssd.1 
 |-  ( ph -> C C_ B )
2 xrge0infssd.2 
 |-  ( ph -> B C_ ( 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 
 |-  ( B C_ ( 0 [,] +oo ) -> E. x e. ( 0 [,] +oo ) ( A. y e. B -. y < x /\ A. y e. ( 0 [,] +oo ) ( x < y -> E. z e. B z < y ) ) )
9 2 8 syl 
 |-  ( ph -> E. x e. ( 0 [,] +oo ) ( A. y e. B -. y < x /\ A. y e. ( 0 [,] +oo ) ( x < y -> E. z e. B z < y ) ) )
10 7 9 infcl 
 |-  ( ph -> inf ( B , ( 0 [,] +oo ) , < ) e. ( 0 [,] +oo ) )
11 3 10 sselid 
 |-  ( ph -> inf ( B , ( 0 [,] +oo ) , < ) e. RR* )
12 1 2 sstrd 
 |-  ( ph -> C C_ ( 0 [,] +oo ) )
13 xrge0infss 
 |-  ( C C_ ( 0 [,] +oo ) -> E. x e. ( 0 [,] +oo ) ( A. y e. C -. y < x /\ A. y e. ( 0 [,] +oo ) ( x < y -> E. z e. C z < y ) ) )
14 12 13 syl 
 |-  ( ph -> E. x e. ( 0 [,] +oo ) ( A. y e. C -. y < x /\ A. y e. ( 0 [,] +oo ) ( x < y -> E. z e. C z < y ) ) )
15 7 14 infcl 
 |-  ( ph -> inf ( C , ( 0 [,] +oo ) , < ) e. ( 0 [,] +oo ) )
16 3 15 sselid 
 |-  ( ph -> inf ( C , ( 0 [,] +oo ) , < ) e. RR* )
17 7 1 14 9 infssd 
 |-  ( ph -> -. inf ( C , ( 0 [,] +oo ) , < ) < inf ( B , ( 0 [,] +oo ) , < ) )
18 11 16 17 xrnltled 
 |-  ( ph -> inf ( B , ( 0 [,] +oo ) , < ) <_ inf ( C , ( 0 [,] +oo ) , < ) )