opnrebl2

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

		Ref	Expression
	Assertion	opnrebl2	$⊢ A \in topGen (ran (.)) \leftrightarrow (A \subseteq ℝ \land \forall x \in A \forall y \in ℝ^{+} \exists z \in ℝ^{+} (z \leq y \land (x - z, x + z) \subseteq A))$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ {(abs \circ -) ↾}_{ℝ^{2}} = {(abs \circ -) ↾}_{ℝ^{2}}$
2	1	rexmet	$⊢ {(abs \circ -) ↾}_{ℝ^{2}} \in ∞Met (ℝ)$
3		eqid	$⊢ MetOpen ({(abs \circ -) ↾}_{ℝ^{2}}) = MetOpen ({(abs \circ -) ↾}_{ℝ^{2}})$
4	1 3	tgioo	$⊢ topGen (ran (.)) = MetOpen ({(abs \circ -) ↾}_{ℝ^{2}})$
5	4	mopnss	$⊢ ({(abs \circ -) ↾}_{ℝ^{2}} \in ∞Met (ℝ) \land A \in topGen (ran (.))) \to A \subseteq ℝ$
6	2 5	mpan	$⊢ A \in topGen (ran (.)) \to A \subseteq ℝ$
7	4	mopni3	$⊢ (({(abs \circ -) ↾}_{ℝ^{2}} \in ∞Met (ℝ) \land A \in topGen (ran (.)) \land x \in A) \land y \in ℝ^{+}) \to \exists z \in ℝ^{+} (z < y \land x ball ({(abs \circ -) ↾}_{ℝ^{2}}) z \subseteq A)$
8	7	ex	$⊢ ({(abs \circ -) ↾}_{ℝ^{2}} \in ∞Met (ℝ) \land A \in topGen (ran (.)) \land x \in A) \to (y \in ℝ^{+} \to \exists z \in ℝ^{+} (z < y \land x ball ({(abs \circ -) ↾}_{ℝ^{2}}) z \subseteq A))$
9	2 8	mp3an1	$⊢ (A \in topGen (ran (.)) \land x \in A) \to (y \in ℝ^{+} \to \exists z \in ℝ^{+} (z < y \land x ball ({(abs \circ -) ↾}_{ℝ^{2}}) z \subseteq A))$
10	6	sselda	$⊢ (A \in topGen (ran (.)) \land x \in A) \to x \in ℝ$
11		rpre	$⊢ z \in ℝ^{+} \to z \in ℝ$
12	1	bl2ioo	$⊢ (x \in ℝ \land z \in ℝ) \to x ball ({(abs \circ -) ↾}_{ℝ^{2}}) z = (x - z, x + z)$
13	11 12	sylan2	$⊢ (x \in ℝ \land z \in ℝ^{+}) \to x ball ({(abs \circ -) ↾}_{ℝ^{2}}) z = (x - z, x + z)$
14	13	sseq1d	$⊢ (x \in ℝ \land z \in ℝ^{+}) \to (x ball ({(abs \circ -) ↾}_{ℝ^{2}}) z \subseteq A \leftrightarrow (x - z, x + z) \subseteq A)$
15	14	anbi2d	$⊢ (x \in ℝ \land z \in ℝ^{+}) \to ((z < y \land x ball ({(abs \circ -) ↾}_{ℝ^{2}}) z \subseteq A) \leftrightarrow (z < y \land (x - z, x + z) \subseteq A))$
16	15	rexbidva	$⊢ x \in ℝ \to (\exists z \in ℝ^{+} (z < y \land x ball ({(abs \circ -) ↾}_{ℝ^{2}}) z \subseteq A) \leftrightarrow \exists z \in ℝ^{+} (z < y \land (x - z, x + z) \subseteq A))$
17	16	biimpd	$⊢ x \in ℝ \to (\exists z \in ℝ^{+} (z < y \land x ball ({(abs \circ -) ↾}_{ℝ^{2}}) z \subseteq A) \to \exists z \in ℝ^{+} (z < y \land (x - z, x + z) \subseteq A))$
18		rpre	$⊢ y \in ℝ^{+} \to y \in ℝ$
19		ltle	$⊢ (z \in ℝ \land y \in ℝ) \to (z < y \to z \leq y)$
20	11 18 19	syl2anr	$⊢ (y \in ℝ^{+} \land z \in ℝ^{+}) \to (z < y \to z \leq y)$
21	20	anim1d	$⊢ (y \in ℝ^{+} \land z \in ℝ^{+}) \to ((z < y \land (x - z, x + z) \subseteq A) \to (z \leq y \land (x - z, x + z) \subseteq A))$
22	21	reximdva	$⊢ y \in ℝ^{+} \to (\exists z \in ℝ^{+} (z < y \land (x - z, x + z) \subseteq A) \to \exists z \in ℝ^{+} (z \leq y \land (x - z, x + z) \subseteq A))$
23	17 22	syl9	$⊢ x \in ℝ \to (y \in ℝ^{+} \to (\exists z \in ℝ^{+} (z < y \land x ball ({(abs \circ -) ↾}_{ℝ^{2}}) z \subseteq A) \to \exists z \in ℝ^{+} (z \leq y \land (x - z, x + z) \subseteq A)))$
24	10 23	syl	$⊢ (A \in topGen (ran (.)) \land x \in A) \to (y \in ℝ^{+} \to (\exists z \in ℝ^{+} (z < y \land x ball ({(abs \circ -) ↾}_{ℝ^{2}}) z \subseteq A) \to \exists z \in ℝ^{+} (z \leq y \land (x - z, x + z) \subseteq A)))$
25	9 24	mpdd	$⊢ (A \in topGen (ran (.)) \land x \in A) \to (y \in ℝ^{+} \to \exists z \in ℝ^{+} (z \leq y \land (x - z, x + z) \subseteq A))$
26	25	expimpd	$⊢ A \in topGen (ran (.)) \to ((x \in A \land y \in ℝ^{+}) \to \exists z \in ℝ^{+} (z \leq y \land (x - z, x + z) \subseteq A))$
27	26	ralrimivv	$⊢ A \in topGen (ran (.)) \to \forall x \in A \forall y \in ℝ^{+} \exists z \in ℝ^{+} (z \leq y \land (x - z, x + z) \subseteq A)$
28	6 27	jca	$⊢ A \in topGen (ran (.)) \to (A \subseteq ℝ \land \forall x \in A \forall y \in ℝ^{+} \exists z \in ℝ^{+} (z \leq y \land (x - z, x + z) \subseteq A))$
29		ssel2	$⊢ (A \subseteq ℝ \land x \in A) \to x \in ℝ$
30		1rp	$⊢ 1 \in ℝ^{+}$
31		simpr	$⊢ (z \leq y \land (x - z, x + z) \subseteq A) \to (x - z, x + z) \subseteq A$
32	31	reximi	$⊢ \exists z \in ℝ^{+} (z \leq y \land (x - z, x + z) \subseteq A) \to \exists z \in ℝ^{+} (x - z, x + z) \subseteq A$
33	32	ralimi	$⊢ \forall y \in ℝ^{+} \exists z \in ℝ^{+} (z \leq y \land (x - z, x + z) \subseteq A) \to \forall y \in ℝ^{+} \exists z \in ℝ^{+} (x - z, x + z) \subseteq A$
34		biidd	$⊢ y = 1 \to (\exists z \in ℝ^{+} (x - z, x + z) \subseteq A \leftrightarrow \exists z \in ℝ^{+} (x - z, x + z) \subseteq A)$
35	34	rspcv	$⊢ 1 \in ℝ^{+} \to (\forall y \in ℝ^{+} \exists z \in ℝ^{+} (x - z, x + z) \subseteq A \to \exists z \in ℝ^{+} (x - z, x + z) \subseteq A)$
36	30 33 35	mpsyl	$⊢ \forall y \in ℝ^{+} \exists z \in ℝ^{+} (z \leq y \land (x - z, x + z) \subseteq A) \to \exists z \in ℝ^{+} (x - z, x + z) \subseteq A$
37	14	rexbidva	$⊢ x \in ℝ \to (\exists z \in ℝ^{+} x ball ({(abs \circ -) ↾}_{ℝ^{2}}) z \subseteq A \leftrightarrow \exists z \in ℝ^{+} (x - z, x + z) \subseteq A)$
38	36 37	imbitrrid	$⊢ x \in ℝ \to (\forall y \in ℝ^{+} \exists z \in ℝ^{+} (z \leq y \land (x - z, x + z) \subseteq A) \to \exists z \in ℝ^{+} x ball ({(abs \circ -) ↾}_{ℝ^{2}}) z \subseteq A)$
39	29 38	syl	$⊢ (A \subseteq ℝ \land x \in A) \to (\forall y \in ℝ^{+} \exists z \in ℝ^{+} (z \leq y \land (x - z, x + z) \subseteq A) \to \exists z \in ℝ^{+} x ball ({(abs \circ -) ↾}_{ℝ^{2}}) z \subseteq A)$
40	39	ralimdva	$⊢ A \subseteq ℝ \to (\forall x \in A \forall y \in ℝ^{+} \exists z \in ℝ^{+} (z \leq y \land (x - z, x + z) \subseteq A) \to \forall x \in A \exists z \in ℝ^{+} x ball ({(abs \circ -) ↾}_{ℝ^{2}}) z \subseteq A)$
41	40	imdistani	$⊢ (A \subseteq ℝ \land \forall x \in A \forall y \in ℝ^{+} \exists z \in ℝ^{+} (z \leq y \land (x - z, x + z) \subseteq A)) \to (A \subseteq ℝ \land \forall x \in A \exists z \in ℝ^{+} x ball ({(abs \circ -) ↾}_{ℝ^{2}}) z \subseteq A)$
42	4	elmopn2	$⊢ {(abs \circ -) ↾}_{ℝ^{2}} \in ∞Met (ℝ) \to (A \in topGen (ran (.)) \leftrightarrow (A \subseteq ℝ \land \forall x \in A \exists z \in ℝ^{+} x ball ({(abs \circ -) ↾}_{ℝ^{2}}) z \subseteq A))$
43	2 42	ax-mp	$⊢ A \in topGen (ran (.)) \leftrightarrow (A \subseteq ℝ \land \forall x \in A \exists z \in ℝ^{+} x ball ({(abs \circ -) ↾}_{ℝ^{2}}) z \subseteq A)$
44	41 43	sylibr	$⊢ (A \subseteq ℝ \land \forall x \in A \forall y \in ℝ^{+} \exists z \in ℝ^{+} (z \leq y \land (x - z, x + z) \subseteq A)) \to A \in topGen (ran (.))$
45	28 44	impbii	$⊢ A \in topGen (ran (.)) \leftrightarrow (A \subseteq ℝ \land \forall x \in A \forall y \in ℝ^{+} \exists z \in ℝ^{+} (z \leq y \land (x - z, x + z) \subseteq A))$

Metamath Proof Explorer

Theorem opnrebl2

Proof