Theorem opnrebl

Description: A set is open in the standard topology of the reals precisely when every point can be enclosed in an open ball. (Contributed by Jeff Hankins, 23-Sep-2013) (Proof shortened by Mario Carneiro, 30-Jan-2014)

	Ref	Expression
Assertion	opnrebl	$$⊢A\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\leftrightarrow \left(A\subseteq ℝ\wedge \forall x\in A\exists y\in {ℝ}^{+}\left(x-y,x+y\right)\subseteq A\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢{\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}={\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}$$
2	1	rexmet	$$⊢{\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}\in \mathrm{\infty Met}\left(ℝ\right)$$
3		eqid	$$⊢\mathrm{MetOpen}\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}\right)=\mathrm{MetOpen}\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}\right)$$
4	1 3	tgioo	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{MetOpen}\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}\right)$$
5	4	elmopn2	$$⊢{\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}\in \mathrm{\infty Met}\left(ℝ\right)\to \left(A\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\leftrightarrow \left(A\subseteq ℝ\wedge \forall x\in A\exists y\in {ℝ}^{+}x\mathrm{ball}\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}\right)y\subseteq A\right)\right)$$
6	2 5	ax-mp	$$⊢A\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\leftrightarrow \left(A\subseteq ℝ\wedge \forall x\in A\exists y\in {ℝ}^{+}x\mathrm{ball}\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}\right)y\subseteq A\right)$$
7		ssel2	$$⊢\left(A\subseteq ℝ\wedge x\in A\right)\to x\in ℝ$$
8		rpre	$$⊢y\in {ℝ}^{+}\to y\in ℝ$$
9	1	bl2ioo	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to x\mathrm{ball}\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}\right)y=\left(x-y,x+y\right)$$
10	8 9	sylan2	$$⊢\left(x\in ℝ\wedge y\in {ℝ}^{+}\right)\to x\mathrm{ball}\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}\right)y=\left(x-y,x+y\right)$$
11	10	sseq1d	$$⊢\left(x\in ℝ\wedge y\in {ℝ}^{+}\right)\to \left(x\mathrm{ball}\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}\right)y\subseteq A\leftrightarrow \left(x-y,x+y\right)\subseteq A\right)$$
12	11	rexbidva	$$⊢x\in ℝ\to \left(\exists y\in {ℝ}^{+}x\mathrm{ball}\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}\right)y\subseteq A\leftrightarrow \exists y\in {ℝ}^{+}\left(x-y,x+y\right)\subseteq A\right)$$
13	7 12	syl	$$⊢\left(A\subseteq ℝ\wedge x\in A\right)\to \left(\exists y\in {ℝ}^{+}x\mathrm{ball}\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}\right)y\subseteq A\leftrightarrow \exists y\in {ℝ}^{+}\left(x-y,x+y\right)\subseteq A\right)$$
14	13	ralbidva	$$⊢A\subseteq ℝ\to \left(\forall x\in A\exists y\in {ℝ}^{+}x\mathrm{ball}\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}\right)y\subseteq A\leftrightarrow \forall x\in A\exists y\in {ℝ}^{+}\left(x-y,x+y\right)\subseteq A\right)$$
15	14	pm5.32i	$$⊢\left(A\subseteq ℝ\wedge \forall x\in A\exists y\in {ℝ}^{+}x\mathrm{ball}\left({\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}\right)y\subseteq A\right)\leftrightarrow \left(A\subseteq ℝ\wedge \forall x\in A\exists y\in {ℝ}^{+}\left(x-y,x+y\right)\subseteq A\right)$$
16	6 15	bitri	$$⊢A\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\leftrightarrow \left(A\subseteq ℝ\wedge \forall x\in A\exists y\in {ℝ}^{+}\left(x-y,x+y\right)\subseteq A\right)$$