Description: An upper bound is not less than the supremum of a nonempty bounded set of reals. (Contributed by NM, 15-Nov-2004) (Revised by Mario Carneiro, 6-Sep-2014)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | suprnub | ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) ∧ 𝐵 ∈ ℝ ) → ( ¬ 𝐵 < sup ( 𝐴 , ℝ , < ) ↔ ∀ 𝑧 ∈ 𝐴 ¬ 𝐵 < 𝑧 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | suprlub | ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) ∧ 𝐵 ∈ ℝ ) → ( 𝐵 < sup ( 𝐴 , ℝ , < ) ↔ ∃ 𝑧 ∈ 𝐴 𝐵 < 𝑧 ) ) | |
| 2 | 1 | notbid | ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) ∧ 𝐵 ∈ ℝ ) → ( ¬ 𝐵 < sup ( 𝐴 , ℝ , < ) ↔ ¬ ∃ 𝑧 ∈ 𝐴 𝐵 < 𝑧 ) ) |
| 3 | ralnex | ⊢ ( ∀ 𝑧 ∈ 𝐴 ¬ 𝐵 < 𝑧 ↔ ¬ ∃ 𝑧 ∈ 𝐴 𝐵 < 𝑧 ) | |
| 4 | 2 3 | bitr4di | ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) ∧ 𝐵 ∈ ℝ ) → ( ¬ 𝐵 < sup ( 𝐴 , ℝ , < ) ↔ ∀ 𝑧 ∈ 𝐴 ¬ 𝐵 < 𝑧 ) ) |