Theorem elicores

Description: Membership in a left-closed, right-open interval with real bounds. (Contributed by Glauco Siliprandi, 11-Oct-2020)

	Ref	Expression
Assertion	elicores	$$⊢A\in \mathrm{ran}\left({\left[.\right)\upharpoonright }_{{ℝ}^2}\right)\leftrightarrow \exists x\in ℝ\exists y\in ℝA=\left[x,y\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-ico	$$⊢\left[.\right)=\left(x\in {ℝ}^{*},y\in {ℝ}^{*}⟼\left\{z\in {ℝ}^{*}|\left(x\le z\wedge z<y\right)\right\}\right)$$
2	1	reseq1i	$$⊢{\left[.\right)\upharpoonright }_{{ℝ}^2}={\left(x\in {ℝ}^{*},y\in {ℝ}^{*}⟼\left\{z\in {ℝ}^{*}|\left(x\le z\wedge z<y\right)\right\}\right)\upharpoonright }_{{ℝ}^2}$$
3		ressxr	$$⊢ℝ\subseteq {ℝ}^{*}$$
4		resmpo	$$⊢\left(ℝ\subseteq {ℝ}^{*}\wedge ℝ\subseteq {ℝ}^{*}\right)\to {\left(x\in {ℝ}^{*},y\in {ℝ}^{*}⟼\left\{z\in {ℝ}^{*}|\left(x\le z\wedge z<y\right)\right\}\right)\upharpoonright }_{{ℝ}^2}=\left(x\in ℝ,y\in ℝ⟼\left\{z\in {ℝ}^{*}|\left(x\le z\wedge z<y\right)\right\}\right)$$
5	3 3 4	mp2an	$$⊢{\left(x\in {ℝ}^{*},y\in {ℝ}^{*}⟼\left\{z\in {ℝ}^{*}|\left(x\le z\wedge z<y\right)\right\}\right)\upharpoonright }_{{ℝ}^2}=\left(x\in ℝ,y\in ℝ⟼\left\{z\in {ℝ}^{*}|\left(x\le z\wedge z<y\right)\right\}\right)$$
6	2 5	eqtri	$$⊢{\left[.\right)\upharpoonright }_{{ℝ}^2}=\left(x\in ℝ,y\in ℝ⟼\left\{z\in {ℝ}^{*}|\left(x\le z\wedge z<y\right)\right\}\right)$$
7	6	rneqi	$$⊢\mathrm{ran}\left({\left[.\right)\upharpoonright }_{{ℝ}^2}\right)=\mathrm{ran}\left(x\in ℝ,y\in ℝ⟼\left\{z\in {ℝ}^{*}|\left(x\le z\wedge z<y\right)\right\}\right)$$
8	7	eleq2i	$$⊢A\in \mathrm{ran}\left({\left[.\right)\upharpoonright }_{{ℝ}^2}\right)\leftrightarrow A\in \mathrm{ran}\left(x\in ℝ,y\in ℝ⟼\left\{z\in {ℝ}^{*}|\left(x\le z\wedge z<y\right)\right\}\right)$$
9		eqid	$$⊢\left(x\in ℝ,y\in ℝ⟼\left\{z\in {ℝ}^{*}|\left(x\le z\wedge z<y\right)\right\}\right)=\left(x\in ℝ,y\in ℝ⟼\left\{z\in {ℝ}^{*}|\left(x\le z\wedge z<y\right)\right\}\right)$$
10		xrex	$$⊢{ℝ}^{*}\in \mathrm{V}$$
11	10	rabex	$$⊢\left\{z\in {ℝ}^{*}|\left(x\le z\wedge z<y\right)\right\}\in \mathrm{V}$$
12	9 11	elrnmpo	$$⊢A\in \mathrm{ran}\left(x\in ℝ,y\in ℝ⟼\left\{z\in {ℝ}^{*}|\left(x\le z\wedge z<y\right)\right\}\right)\leftrightarrow \exists x\in ℝ\exists y\in ℝA=\left\{z\in {ℝ}^{*}|\left(x\le z\wedge z<y\right)\right\}$$
13	3	sseli	$$⊢x\in ℝ\to x\in {ℝ}^{*}$$
14	13	adantr	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to x\in {ℝ}^{*}$$
15	3	sseli	$$⊢y\in ℝ\to y\in {ℝ}^{*}$$
16	15	adantl	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to y\in {ℝ}^{*}$$
17		icoval	$$⊢\left(x\in {ℝ}^{*}\wedge y\in {ℝ}^{*}\right)\to \left[x,y\right)=\left\{z\in {ℝ}^{*}|\left(x\le z\wedge z<y\right)\right\}$$
18	14 16 17	syl2anc	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to \left[x,y\right)=\left\{z\in {ℝ}^{*}|\left(x\le z\wedge z<y\right)\right\}$$
19	18	eqcomd	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to \left\{z\in {ℝ}^{*}|\left(x\le z\wedge z<y\right)\right\}=\left[x,y\right)$$
20	19	eqeq2d	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to \left(A=\left\{z\in {ℝ}^{*}|\left(x\le z\wedge z<y\right)\right\}\leftrightarrow A=\left[x,y\right)\right)$$
21	20	rexbidva	$$⊢x\in ℝ\to \left(\exists y\in ℝA=\left\{z\in {ℝ}^{*}|\left(x\le z\wedge z<y\right)\right\}\leftrightarrow \exists y\in ℝA=\left[x,y\right)\right)$$
22	21	rexbiia	$$⊢\exists x\in ℝ\exists y\in ℝA=\left\{z\in {ℝ}^{*}|\left(x\le z\wedge z<y\right)\right\}\leftrightarrow \exists x\in ℝ\exists y\in ℝA=\left[x,y\right)$$
23	8 12 22	3bitri	$$⊢A\in \mathrm{ran}\left({\left[.\right)\upharpoonright }_{{ℝ}^2}\right)\leftrightarrow \exists x\in ℝ\exists y\in ℝA=\left[x,y\right)$$