Metamath Proof Explorer


Theorem suprubii

Description: A member of a nonempty bounded set of reals is less than or equal to the set's upper bound. (Contributed by NM, 12-Sep-1999)

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

Proof

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