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 ) , < ) ) |