Metamath Proof Explorer


Theorem ubioc1

Description: The upper bound belongs to an open-below, closed-above interval. See ubicc2 . (Contributed by FL, 29-May-2014)

Ref Expression
Assertion ubioc1 ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴 < 𝐵 ) → 𝐵 ∈ ( 𝐴 (,] 𝐵 ) )

Proof

Step Hyp Ref Expression
1 simp2 ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴 < 𝐵 ) → 𝐵 ∈ ℝ* )
2 simp3 ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴 < 𝐵 ) → 𝐴 < 𝐵 )
3 xrleid ( 𝐵 ∈ ℝ*𝐵𝐵 )
4 3 3ad2ant2 ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴 < 𝐵 ) → 𝐵𝐵 )
5 elioc1 ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) → ( 𝐵 ∈ ( 𝐴 (,] 𝐵 ) ↔ ( 𝐵 ∈ ℝ*𝐴 < 𝐵𝐵𝐵 ) ) )
6 5 3adant3 ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴 < 𝐵 ) → ( 𝐵 ∈ ( 𝐴 (,] 𝐵 ) ↔ ( 𝐵 ∈ ℝ*𝐴 < 𝐵𝐵𝐵 ) ) )
7 1 2 4 6 mpbir3and ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴 < 𝐵 ) → 𝐵 ∈ ( 𝐴 (,] 𝐵 ) )