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	⊢ ( 𝐴 ∈ ( topGen ‘ ran (,) ) ↔ ( 𝐴 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ ℝ+ ( ( 𝑥 − 𝑦 ) (,) ( 𝑥 + 𝑦 ) ) ⊆ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) )
2	1	rexmet	⊢ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ∈ ( ∞Met ‘ ℝ )
3		eqid	⊢ ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) )
4	1 3	tgioo	⊢ ( topGen ‘ ran (,) ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) )
5	4	elmopn2	⊢ ( ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ∈ ( ∞Met ‘ ℝ ) → ( 𝐴 ∈ ( topGen ‘ ran (,) ) ↔ ( 𝐴 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ ℝ+ ( 𝑥 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑦 ) ⊆ 𝐴 ) ) )
6	2 5	ax-mp	⊢ ( 𝐴 ∈ ( topGen ‘ ran (,) ) ↔ ( 𝐴 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ ℝ+ ( 𝑥 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑦 ) ⊆ 𝐴 ) )
7		ssel2	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℝ )
8		rpre	⊢ ( 𝑦 ∈ ℝ+ → 𝑦 ∈ ℝ )
9	1	bl2ioo	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑦 ) = ( ( 𝑥 − 𝑦 ) (,) ( 𝑥 + 𝑦 ) ) )
10	8 9	sylan2	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) → ( 𝑥 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑦 ) = ( ( 𝑥 − 𝑦 ) (,) ( 𝑥 + 𝑦 ) ) )
11	10	sseq1d	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ+ ) → ( ( 𝑥 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑦 ) ⊆ 𝐴 ↔ ( ( 𝑥 − 𝑦 ) (,) ( 𝑥 + 𝑦 ) ) ⊆ 𝐴 ) )
12	11	rexbidva	⊢ ( 𝑥 ∈ ℝ → ( ∃ 𝑦 ∈ ℝ+ ( 𝑥 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑦 ) ⊆ 𝐴 ↔ ∃ 𝑦 ∈ ℝ+ ( ( 𝑥 − 𝑦 ) (,) ( 𝑥 + 𝑦 ) ) ⊆ 𝐴 ) )
13	7 12	syl	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ 𝐴 ) → ( ∃ 𝑦 ∈ ℝ+ ( 𝑥 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑦 ) ⊆ 𝐴 ↔ ∃ 𝑦 ∈ ℝ+ ( ( 𝑥 − 𝑦 ) (,) ( 𝑥 + 𝑦 ) ) ⊆ 𝐴 ) )
14	13	ralbidva	⊢ ( 𝐴 ⊆ ℝ → ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ ℝ+ ( 𝑥 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑦 ) ⊆ 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ ℝ+ ( ( 𝑥 − 𝑦 ) (,) ( 𝑥 + 𝑦 ) ) ⊆ 𝐴 ) )
15	14	pm5.32i	⊢ ( ( 𝐴 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ ℝ+ ( 𝑥 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑦 ) ⊆ 𝐴 ) ↔ ( 𝐴 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ ℝ+ ( ( 𝑥 − 𝑦 ) (,) ( 𝑥 + 𝑦 ) ) ⊆ 𝐴 ) )
16	6 15	bitri	⊢ ( 𝐴 ∈ ( topGen ‘ ran (,) ) ↔ ( 𝐴 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ ℝ+ ( ( 𝑥 − 𝑦 ) (,) ( 𝑥 + 𝑦 ) ) ⊆ 𝐴 ) )