Metamath Proof Explorer

Theorem suprnubii

Description: An upper bound is not less than the supremum of a nonempty bounded set of reals. (Contributed by NM, 15-Oct-2004) (Revised by Mario Carneiro, 6-Sep-2014)

		Ref	Expression
	Hypothesis	sup3i.1	\|- ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x )
	Assertion	suprnubii	\|- ( B e. RR -> ( -. B < sup ( A , RR , < ) <-> A. z e. A -. B < z ) )

Proof

Step	Hyp	Ref	Expression
1		sup3i.1	\|- ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x )
2		suprnub	\|- ( ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ B e. RR ) -> ( -. B < sup ( A , RR , < ) <-> A. z e. A -. B < z ) )
3	1 2	mpan	\|- ( B e. RR -> ( -. B < sup ( A , RR , < ) <-> A. z e. A -. B < z ) )

Step

Hyp

Ref

Expression

sup3i.1

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

suprnub

 |-  ( ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <_ x ) /\ B e. RR ) -> ( -. B < sup ( A , RR , < ) <-> A. z e. A -. B < z ) )

1 2

mpan

 |-  ( B e. RR -> ( -. B < sup ( A , RR , < ) <-> A. z e. A -. B < z ) )