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