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

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

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 ) /\ B e. A ) -> B <_ sup ( A , RR , < ) )

1 2

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