Theorem ubico

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

	Ref	Expression
Assertion	ubico	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) → ¬ 𝐵 ∈ ( 𝐴 [,) 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		simp3	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐵 ) → 𝐵 < 𝐵 )
2		simp1	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐵 ) → 𝐵 ∈ ℝ )
3	2	ltnrd	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐵 ) → ¬ 𝐵 < 𝐵 )
4	1 3	pm2.65i	⊢ ¬ ( 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐵 )
5		elico2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) → ( 𝐵 ∈ ( 𝐴 [,) 𝐵 ) ↔ ( 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐵 ) ) )
6	4 5	mtbiri	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) → ¬ 𝐵 ∈ ( 𝐴 [,) 𝐵 ) )