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

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

Step

Hyp

Ref

Expression

sup3i.1

 |-  ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x )

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

1 2

 |-  E. x e. RR ( A. y e. A -. x < y /\ A. y e. RR ( y < x -> E. z e. A y < z ) )