Theorem iooin

Description: Intersection of two open intervals of extended reals. (Contributed by NM, 7-Feb-2007) (Revised by Mario Carneiro, 3-Nov-2013)

	Ref	Expression
Assertion	iooin	$$⊢\left(\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\wedge \left(C\in {ℝ}^{*}\wedge D\in {ℝ}^{*}\right)\right)\to \left(A,B\right)\cap \left(C,D\right)=\left(if\left(A\le C,C,A\right),if\left(B\le D,B,D\right)\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		xrmaxlt	$$⊢\left(A\in {ℝ}^{*}\wedge C\in {ℝ}^{*}\wedge z\in {ℝ}^{*}\right)\to \left(if\left(A\le C,C,A\right)<z\leftrightarrow \left(A<z\wedge C<z\right)\right)$$
3		xrltmin	$$⊢\left(z\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\wedge D\in {ℝ}^{*}\right)\to \left(z<if\left(B\le D,B,D\right)\leftrightarrow \left(z<B\wedge z<D\right)\right)$$
4	1 2 3	ixxin	$$⊢\left(\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\wedge \left(C\in {ℝ}^{*}\wedge D\in {ℝ}^{*}\right)\right)\to \left(A,B\right)\cap \left(C,D\right)=\left(if\left(A\le C,C,A\right),if\left(B\le D,B,D\right)\right)$$