Metamath Proof Explorer


Theorem sup3ii

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

Proof

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