Theorem iccin

Description: Intersection of two closed intervals of extended reals. (Contributed by Zhi Wang, 9-Sep-2024)

	Ref	Expression
Assertion	iccin	$$⊢\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-icc	$$⊢\left[.\right]=\left(x\in {ℝ}^{*},y\in {ℝ}^{*}⟼\left\{z\in {ℝ}^{*}|\left(x\le z\wedge z\le y\right)\right\}\right)$$
2		xrmaxle	$$⊢\left(A\in {ℝ}^{*}\wedge C\in {ℝ}^{*}\wedge z\in {ℝ}^{*}\right)\to \left(if\left(A\le C,C,A\right)\le z\leftrightarrow \left(A\le z\wedge C\le z\right)\right)$$
3		xrlemin	$$⊢\left(z\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\wedge D\in {ℝ}^{*}\right)\to \left(z\le if\left(B\le D,B,D\right)\leftrightarrow \left(z\le B\wedge z\le 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]$$