Metamath Proof Explorer

Theorem ubico

Description: A right-open interval does not contain its right endpoint. (Contributed by Thierry Arnoux, 5-Apr-2017)

Ref Expression
Assertion ubico ⊢ A ∈ ℝ ∧ B ∈ ℝ * → ¬ B ∈ A B

Proof

Step Hyp Ref Expression
1 simp3 ⊢ B ∈ ℝ ∧ A ≤ B ∧ B < B → B < B
2 simp1 ⊢ B ∈ ℝ ∧ A ≤ B ∧ B < B → B ∈ ℝ
3 2 ltnrd ⊢ B ∈ ℝ ∧ A ≤ B ∧ B < B → ¬ B < B
4 1 3 pm2.65i ⊢ ¬ B ∈ ℝ ∧ A ≤ B ∧ B < B
5 elico2 ⊢ A ∈ ℝ ∧ B ∈ ℝ * → B ∈ A B ↔ B ∈ ℝ ∧ A ≤ B ∧ B < B
6 4 5 mtbiri ⊢ A ∈ ℝ ∧ B ∈ ℝ * → ¬ B ∈ A B