Theorem icoreval

Description: Value of the closed-below, open-above interval function on reals. (Contributed by ML, 26-Jul-2020)

	Ref	Expression
Assertion	icoreval	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left[A,B\right)=\left\{z\in ℝ|\left(A\le z\wedge z<B\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		ovres	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to A\left({\left[.\right)\upharpoonright }_{{ℝ}^2}\right)B=\left[A,B\right)$$
2		breq1	$$⊢x=A\to \left(x\le z\leftrightarrow A\le z\right)$$
3	2	anbi1d	$$⊢x=A\to \left(\left(x\le z\wedge z<y\right)\leftrightarrow \left(A\le z\wedge z<y\right)\right)$$
4	3	rabbidv	$$⊢x=A\to \left\{z\in ℝ|\left(x\le z\wedge z<y\right)\right\}=\left\{z\in ℝ|\left(A\le z\wedge z<y\right)\right\}$$
5		breq2	$$⊢y=B\to \left(z<y\leftrightarrow z<B\right)$$
6	5	anbi2d	$$⊢y=B\to \left(\left(A\le z\wedge z<y\right)\leftrightarrow \left(A\le z\wedge z<B\right)\right)$$
7	6	rabbidv	$$⊢y=B\to \left\{z\in ℝ|\left(A\le z\wedge z<y\right)\right\}=\left\{z\in ℝ|\left(A\le z\wedge z<B\right)\right\}$$
8		eqid	$$⊢{\left[.\right)\upharpoonright }_{{ℝ}^2}={\left[.\right)\upharpoonright }_{{ℝ}^2}$$
9	8	icorempo	$$⊢{\left[.\right)\upharpoonright }_{{ℝ}^2}=\left(x\in ℝ,y\in ℝ⟼\left\{z\in ℝ|\left(x\le z\wedge z<y\right)\right\}\right)$$
10		reex	$$⊢ℝ\in \mathrm{V}$$
11	10	rabex	$$⊢\left\{z\in ℝ|\left(A\le z\wedge z<B\right)\right\}\in \mathrm{V}$$
12	4 7 9 11	ovmpo	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to A\left({\left[.\right)\upharpoonright }_{{ℝ}^2}\right)B=\left\{z\in ℝ|\left(A\le z\wedge z<B\right)\right\}$$
13	1 12	eqtr3d	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left[A,B\right)=\left\{z\in ℝ|\left(A\le z\wedge z<B\right)\right\}$$