Theorem icof

Description: The set of left-closed right-open intervals of extended reals maps to subsets of extended reals. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Assertion	icof	$$⊢\left[.\right):{ℝ}^{*}\times {ℝ}^{*}⟶𝒫{ℝ}^{*}$$

Proof

Step	Hyp	Ref	Expression
1		eqidd	$$⊢\left(x\in {ℝ}^{*}\wedge y\in {ℝ}^{*}\right)\to \left\{z\in {ℝ}^{*}|\left(x\le z\wedge z<y\right)\right\}=\left\{z\in {ℝ}^{*}|\left(x\le z\wedge z<y\right)\right\}$$
2		ssrab2	$$⊢\left\{z\in {ℝ}^{*}|\left(x\le z\wedge z<y\right)\right\}\subseteq {ℝ}^{*}$$
3		xrex	$$⊢{ℝ}^{*}\in \mathrm{V}$$
4	3	rabex	$$⊢\left\{z\in {ℝ}^{*}|\left(x\le z\wedge z<y\right)\right\}\in \mathrm{V}$$
5	4	elpw	$$⊢\left\{z\in {ℝ}^{*}|\left(x\le z\wedge z<y\right)\right\}\in 𝒫{ℝ}^{*}\leftrightarrow \left\{z\in {ℝ}^{*}|\left(x\le z\wedge z<y\right)\right\}\subseteq {ℝ}^{*}$$
6	2 5	mpbir	$$⊢\left\{z\in {ℝ}^{*}|\left(x\le z\wedge z<y\right)\right\}\in 𝒫{ℝ}^{*}$$
7	1 6	eqeltrrdi	$$⊢\left(x\in {ℝ}^{*}\wedge y\in {ℝ}^{*}\right)\to \left\{z\in {ℝ}^{*}|\left(x\le z\wedge z<y\right)\right\}\in 𝒫{ℝ}^{*}$$
8	7	rgen2	$$⊢\forall x\in {ℝ}^{*}\forall y\in {ℝ}^{*}\left\{z\in {ℝ}^{*}|\left(x\le z\wedge z<y\right)\right\}\in 𝒫{ℝ}^{*}$$
9		df-ico	$$⊢\left[.\right)=\left(x\in {ℝ}^{*},y\in {ℝ}^{*}⟼\left\{z\in {ℝ}^{*}|\left(x\le z\wedge z<y\right)\right\}\right)$$
10	9	fmpo	$$⊢\forall x\in {ℝ}^{*}\forall y\in {ℝ}^{*}\left\{z\in {ℝ}^{*}|\left(x\le z\wedge z<y\right)\right\}\in 𝒫{ℝ}^{*}\leftrightarrow \left[.\right):{ℝ}^{*}\times {ℝ}^{*}⟶𝒫{ℝ}^{*}$$
11	8 10	mpbi	$$⊢\left[.\right):{ℝ}^{*}\times {ℝ}^{*}⟶𝒫{ℝ}^{*}$$