Theorem supxrub

Description: A member of a set of extended reals is less than or equal to the set's supremum. (Contributed by NM, 7-Feb-2006)

	Ref	Expression
Assertion	supxrub	⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ∈ 𝐴 ) → 𝐵 ≤ sup ( 𝐴 , ℝ* , < ) )

Proof

Step	Hyp	Ref	Expression
1		ssel2	⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ∈ 𝐴 ) → 𝐵 ∈ ℝ* )
2		supxrcl	⊢ ( 𝐴 ⊆ ℝ* → sup ( 𝐴 , ℝ* , < ) ∈ ℝ* )
3	2	adantr	⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ∈ 𝐴 ) → sup ( 𝐴 , ℝ* , < ) ∈ ℝ* )
4		xrltso	⊢ < Or ℝ*
5	4	a1i	⊢ ( 𝐴 ⊆ ℝ* → < Or ℝ* )
6		xrsupss	⊢ ( 𝐴 ⊆ ℝ* → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) )
7	5 6	supub	⊢ ( 𝐴 ⊆ ℝ* → ( 𝐵 ∈ 𝐴 → ¬ sup ( 𝐴 , ℝ* , < ) < 𝐵 ) )
8	7	imp	⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ∈ 𝐴 ) → ¬ sup ( 𝐴 , ℝ* , < ) < 𝐵 )
9	1 3 8	xrnltled	⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ∈ 𝐴 ) → 𝐵 ≤ sup ( 𝐴 , ℝ* , < ) )