Theorem icoub

Description: A left-closed, right-open interval does not contain its upper bound. (Contributed by Glauco Siliprandi, 17-Aug-2020)

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

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ( 𝐴 [,) 𝐵 ) ) → 𝐴 ∈ ℝ* )
2		icossxr	⊢ ( 𝐴 [,) 𝐵 ) ⊆ ℝ*
3		id	⊢ ( 𝐵 ∈ ( 𝐴 [,) 𝐵 ) → 𝐵 ∈ ( 𝐴 [,) 𝐵 ) )
4	2 3	sselid	⊢ ( 𝐵 ∈ ( 𝐴 [,) 𝐵 ) → 𝐵 ∈ ℝ* )
5	4	adantl	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ( 𝐴 [,) 𝐵 ) ) → 𝐵 ∈ ℝ* )
6		simpr	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ( 𝐴 [,) 𝐵 ) ) → 𝐵 ∈ ( 𝐴 [,) 𝐵 ) )
7		icoltub	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐵 ∈ ( 𝐴 [,) 𝐵 ) ) → 𝐵 < 𝐵 )
8	1 5 6 7	syl3anc	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ( 𝐴 [,) 𝐵 ) ) → 𝐵 < 𝐵 )
9		xrltnr	⊢ ( 𝐵 ∈ ℝ* → ¬ 𝐵 < 𝐵 )
10	4 9	syl	⊢ ( 𝐵 ∈ ( 𝐴 [,) 𝐵 ) → ¬ 𝐵 < 𝐵 )
11	10	adantl	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ( 𝐴 [,) 𝐵 ) ) → ¬ 𝐵 < 𝐵 )
12	8 11	pm2.65da	⊢ ( 𝐴 ∈ ℝ* → ¬ 𝐵 ∈ ( 𝐴 [,) 𝐵 ) )