Step |
Hyp |
Ref |
Expression |
1 |
|
xrsupssd.1 |
|- ( ph -> B C_ C ) |
2 |
|
xrsupssd.2 |
|- ( ph -> C C_ RR* ) |
3 |
|
xrltso |
|- < Or RR* |
4 |
3
|
a1i |
|- ( ph -> < Or RR* ) |
5 |
1 2
|
sstrd |
|- ( ph -> B C_ RR* ) |
6 |
|
xrsupss |
|- ( B C_ RR* -> E. x e. RR* ( A. y e. B -. x < y /\ A. y e. RR* ( y < x -> E. z e. B y < z ) ) ) |
7 |
5 6
|
syl |
|- ( ph -> E. x e. RR* ( A. y e. B -. x < y /\ A. y e. RR* ( y < x -> E. z e. B y < z ) ) ) |
8 |
|
xrsupss |
|- ( C C_ RR* -> E. x e. RR* ( A. y e. C -. x < y /\ A. y e. RR* ( y < x -> E. z e. C y < z ) ) ) |
9 |
2 8
|
syl |
|- ( ph -> E. x e. RR* ( A. y e. C -. x < y /\ A. y e. RR* ( y < x -> E. z e. C y < z ) ) ) |
10 |
4 1 2 7 9
|
supssd |
|- ( ph -> -. sup ( C , RR* , < ) < sup ( B , RR* , < ) ) |
11 |
4 7
|
supcl |
|- ( ph -> sup ( B , RR* , < ) e. RR* ) |
12 |
4 9
|
supcl |
|- ( ph -> sup ( C , RR* , < ) e. RR* ) |
13 |
|
xrlenlt |
|- ( ( sup ( B , RR* , < ) e. RR* /\ sup ( C , RR* , < ) e. RR* ) -> ( sup ( B , RR* , < ) <_ sup ( C , RR* , < ) <-> -. sup ( C , RR* , < ) < sup ( B , RR* , < ) ) ) |
14 |
11 12 13
|
syl2anc |
|- ( ph -> ( sup ( B , RR* , < ) <_ sup ( C , RR* , < ) <-> -. sup ( C , RR* , < ) < sup ( B , RR* , < ) ) ) |
15 |
10 14
|
mpbird |
|- ( ph -> sup ( B , RR* , < ) <_ sup ( C , RR* , < ) ) |