Theorem supxrlub

Description: The supremum of a set of extended reals is less than or equal to an upper bound. (Contributed by Mario Carneiro, 13-Sep-2015)

	Ref	Expression
Assertion	supxrlub	⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐵 < sup ( 𝐴 , ℝ* , < ) ↔ ∃ 𝑥 ∈ 𝐴 𝐵 < 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		xrltso	⊢ < Or ℝ*
2	1	a1i	⊢ ( 𝐴 ⊆ ℝ* → < Or ℝ* )
3		xrsupss	⊢ ( 𝐴 ⊆ ℝ* → ∃ 𝑦 ∈ ℝ* ( ∀ 𝑧 ∈ 𝐴 ¬ 𝑦 < 𝑧 ∧ ∀ 𝑧 ∈ ℝ* ( 𝑧 < 𝑦 → ∃ 𝑥 ∈ 𝐴 𝑧 < 𝑥 ) ) )
4		id	⊢ ( 𝐴 ⊆ ℝ* → 𝐴 ⊆ ℝ* )
5	2 3 4	suplub2	⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐵 < sup ( 𝐴 , ℝ* , < ) ↔ ∃ 𝑥 ∈ 𝐴 𝐵 < 𝑥 ) )