Metamath Proof Explorer


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 ( 𝜑𝐵𝑆 )