Description: A version of the completeness axiom for reals. (Contributed by NM, 23-Aug-1999)
Ref | Expression | ||
---|---|---|---|
Hypothesis | sup3i.1 | |- ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) |
|
Assertion | sup3ii | |- E. x e. RR ( A. y e. A -. x < y /\ A. y e. RR ( y < x -> E. z e. A y < z ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sup3i.1 | |- ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) |
|
2 | 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. z e. A y < z ) ) ) |
|
3 | 1 2 | ax-mp | |- E. x e. RR ( A. y e. A -. x < y /\ A. y e. RR ( y < x -> E. z e. A y < z ) ) |