Metamath Proof Explorer


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 sseldi ( 𝐵 ∈ ( 𝐴 [,) 𝐵 ) → 𝐵 ∈ ℝ* )
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 ( 𝐴 ∈ ℝ* → ¬ 𝐵 ∈ ( 𝐴 [,) 𝐵 ) )