Theorem ioossioc

Description: An open interval is a subset of its right closure. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Assertion	ioossioc	$$⊢\left(A,B\right)\subseteq \left(A,B\right]$$

Proof

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