Step |
Hyp |
Ref |
Expression |
1 |
|
ltso |
|- < Or RR |
2 |
1
|
a1i |
|- ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> < Or RR ) |
3 |
|
sup3 |
|- ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> E. x e. RR ( A. y e. A -. x < y /\ A. y e. RR ( y < x -> E. w e. A y < w ) ) ) |
4 |
|
simp1 |
|- ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) -> A C_ RR ) |
5 |
2 3 4
|
suplub2 |
|- ( ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ B e. RR ) -> ( B < sup ( A , RR , < ) <-> E. w e. A B < w ) ) |
6 |
|
breq2 |
|- ( w = z -> ( B < w <-> B < z ) ) |
7 |
6
|
cbvrexvw |
|- ( E. w e. A B < w <-> E. z e. A B < z ) |
8 |
5 7
|
bitrdi |
|- ( ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ B e. RR ) -> ( B < sup ( A , RR , < ) <-> E. z e. A B < z ) ) |