Theorem supxrubd

Description: A member of a set of extended reals is less than or equal to the set's supremum. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	supxrubd.1	⊢ ( 𝜑 → 𝐴 ⊆ ℝ* )
	supxrubd.2	⊢ ( 𝜑 → 𝐵 ∈ 𝐴 )
	supxrubd.3	⊢ 𝑆 = sup ( 𝐴 , ℝ* , < )
Assertion	supxrubd	⊢ ( 𝜑 → 𝐵 ≤ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		supxrubd.1	⊢ ( 𝜑 → 𝐴 ⊆ ℝ* )
2		supxrubd.2	⊢ ( 𝜑 → 𝐵 ∈ 𝐴 )
3		supxrubd.3	⊢ 𝑆 = sup ( 𝐴 , ℝ* , < )
4		supxrub	⊢ ( ( 𝐴 ⊆ ℝ* ∧ 𝐵 ∈ 𝐴 ) → 𝐵 ≤ sup ( 𝐴 , ℝ* , < ) )
5	1 2 4	syl2anc	⊢ ( 𝜑 → 𝐵 ≤ sup ( 𝐴 , ℝ* , < ) )
6	5 3	breqtrrdi	⊢ ( 𝜑 → 𝐵 ≤ 𝑆 )