Theorem icoreelrn

Description: A class abstraction which is an element of the set of closed-below, open-above intervals of reals. (Contributed by ML, 1-Aug-2020)

	Ref	Expression
Hypothesis	icoreelrn.1	$$⊢I=\left[.\right)\left[{ℝ}^2\right]$$
Assertion	icoreelrn	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left\{z\in ℝ|\left(A\le z\wedge z<B\right)\right\}\in I$$

Proof

Step	Hyp	Ref	Expression
1		icoreelrn.1	$$⊢I=\left[.\right)\left[{ℝ}^2\right]$$
2		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\}$$
3		simpl	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to A\in ℝ$$
4		simpr	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to B\in ℝ$$
5		df-ico	$$⊢\left[.\right)=\left(a\in {ℝ}^{*},b\in {ℝ}^{*}⟼\left\{z\in {ℝ}^{*}|\left(a\le z\wedge z<b\right)\right\}\right)$$
6	5	ixxf	$$⊢\left[.\right):{ℝ}^{*}\times {ℝ}^{*}⟶𝒫{ℝ}^{*}$$
7		ffun	$$⊢\left[.\right):{ℝ}^{*}\times {ℝ}^{*}⟶𝒫{ℝ}^{*}\to \mathrm{Fun}\left[.\right)$$
8	6 7	mp1i	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \mathrm{Fun}\left[.\right)$$
9		rexpssxrxp	$$⊢{ℝ}^2\subseteq {ℝ}^{*}\times {ℝ}^{*}$$
10	6	fdmi	$$⊢\mathrm{dom}\left[.\right)={ℝ}^{*}\times {ℝ}^{*}$$
11	9 10	sseqtrri	$$⊢{ℝ}^2\subseteq \mathrm{dom}\left[.\right)$$
12	11	a1i	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to {ℝ}^2\subseteq \mathrm{dom}\left[.\right)$$
13	3 4 8 12	elovimad	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left[A,B\right)\in \left[.\right)\left[{ℝ}^2\right]$$
14	13 1	eleqtrrdi	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left[A,B\right)\in I$$
15	2 14	eqeltrrd	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left\{z\in ℝ|\left(A\le z\wedge z<B\right)\right\}\in I$$