Theorem ioossico

Description: An open interval is a subset of its closure-below. (Contributed by Thierry Arnoux, 3-Mar-2017)

	Ref	Expression
Assertion	ioossico	$$⊢\left(A,B\right)\subseteq \left[A,B\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-ioo	$$⊢\left(.\right)=\left(a\in {ℝ}^{*},b\in {ℝ}^{*}⟼\left\{x\in {ℝ}^{*}|\left(a<x\wedge x<b\right)\right\}\right)$$
2		df-ico	$$⊢\left[.\right)=\left(a\in {ℝ}^{*},b\in {ℝ}^{*}⟼\left\{x\in {ℝ}^{*}|\left(a\le x\wedge x<b\right)\right\}\right)$$
3		xrltle	$$⊢\left(A\in {ℝ}^{*}\wedge w\in {ℝ}^{*}\right)\to \left(A<w\to A\le w\right)$$
4		idd	$$⊢\left(w\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(w<B\to w<B\right)$$
5	1 2 3 4	ixxssixx	$$⊢\left(A,B\right)\subseteq \left[A,B\right)$$