Metamath Proof Explorer

Theorem 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 ( 𝐴 ∈ ( 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 mopnss ⊢ ( ( ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ∈ ( ∞Met ‘ ℝ ) ∧ 𝐴 ∈ ( topGen ‘ ran (,) ) ) → 𝐴 ⊆ ℝ )
6 2 5 mpan ⊢ ( 𝐴 ∈ ( topGen ‘ ran (,) ) → 𝐴 ⊆ ℝ )
7 4 mopni3 ⊢ ( ( ( ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ∈ ( ∞Met ‘ ℝ ) ∧ 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑧 ∈ ℝ+ ( 𝑧 < 𝑦 ∧ ( 𝑥 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑧 ) ⊆ 𝐴 ) )
8 7 ex ⊢ ( ( ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ∈ ( ∞Met ‘ ℝ ) ∧ 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 ∈ ℝ+ → ∃ 𝑧 ∈ ℝ+ ( 𝑧 < 𝑦 ∧ ( 𝑥 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑧 ) ⊆ 𝐴 ) ) )
9 2 8 mp3an1 ⊢ ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 ∈ ℝ+ → ∃ 𝑧 ∈ ℝ+ ( 𝑧 < 𝑦 ∧ ( 𝑥 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑧 ) ⊆ 𝐴 ) ) )
10 6 sselda ⊢ ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℝ )
11 rpre ⊢ ( 𝑧 ∈ ℝ+ → 𝑧 ∈ ℝ )
12 1 bl2ioo ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( 𝑥 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑧 ) = ( ( 𝑥 − 𝑧 ) (,) ( 𝑥 + 𝑧 ) ) )
13 11 12 sylan2 ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ+ ) → ( 𝑥 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑧 ) = ( ( 𝑥 − 𝑧 ) (,) ( 𝑥 + 𝑧 ) ) )
14 13 sseq1d ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ+ ) → ( ( 𝑥 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑧 ) ⊆ 𝐴 ↔ ( ( 𝑥 − 𝑧 ) (,) ( 𝑥 + 𝑧 ) ) ⊆ 𝐴 ) )
15 14 anbi2d ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑧 ∈ ℝ+ ) → ( ( 𝑧 < 𝑦 ∧ ( 𝑥 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑧 ) ⊆ 𝐴 ) ↔ ( 𝑧 < 𝑦 ∧ ( ( 𝑥 − 𝑧 ) (,) ( 𝑥 + 𝑧 ) ) ⊆ 𝐴 ) ) )
16 15 rexbidva ⊢ ( 𝑥 ∈ ℝ → ( ∃ 𝑧 ∈ ℝ+ ( 𝑧 < 𝑦 ∧ ( 𝑥 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑧 ) ⊆ 𝐴 ) ↔ ∃ 𝑧 ∈ ℝ+ ( 𝑧 < 𝑦 ∧ ( ( 𝑥 − 𝑧 ) (,) ( 𝑥 + 𝑧 ) ) ⊆ 𝐴 ) ) )
17 16 biimpd ⊢ ( 𝑥 ∈ ℝ → ( ∃ 𝑧 ∈ ℝ+ ( 𝑧 < 𝑦 ∧ ( 𝑥 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑧 ) ⊆ 𝐴 ) → ∃ 𝑧 ∈ ℝ+ ( 𝑧 < 𝑦 ∧ ( ( 𝑥 − 𝑧 ) (,) ( 𝑥 + 𝑧 ) ) ⊆ 𝐴 ) ) )
18 rpre ⊢ ( 𝑦 ∈ ℝ+ → 𝑦 ∈ ℝ )
19 ltle ⊢ ( ( 𝑧 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑧 < 𝑦 → 𝑧 ≤ 𝑦 ) )
20 11 18 19 syl2anr ⊢ ( ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) → ( 𝑧 < 𝑦 → 𝑧 ≤ 𝑦 ) )
21 20 anim1d ⊢ ( ( 𝑦 ∈ ℝ+ ∧ 𝑧 ∈ ℝ+ ) → ( ( 𝑧 < 𝑦 ∧ ( ( 𝑥 − 𝑧 ) (,) ( 𝑥 + 𝑧 ) ) ⊆ 𝐴 ) → ( 𝑧 ≤ 𝑦 ∧ ( ( 𝑥 − 𝑧 ) (,) ( 𝑥 + 𝑧 ) ) ⊆ 𝐴 ) ) )
22 21 reximdva ⊢ ( 𝑦 ∈ ℝ+ → ( ∃ 𝑧 ∈ ℝ+ ( 𝑧 < 𝑦 ∧ ( ( 𝑥 − 𝑧 ) (,) ( 𝑥 + 𝑧 ) ) ⊆ 𝐴 ) → ∃ 𝑧 ∈ ℝ+ ( 𝑧 ≤ 𝑦 ∧ ( ( 𝑥 − 𝑧 ) (,) ( 𝑥 + 𝑧 ) ) ⊆ 𝐴 ) ) )
23 17 22 syl9 ⊢ ( 𝑥 ∈ ℝ → ( 𝑦 ∈ ℝ+ → ( ∃ 𝑧 ∈ ℝ+ ( 𝑧 < 𝑦 ∧ ( 𝑥 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑧 ) ⊆ 𝐴 ) → ∃ 𝑧 ∈ ℝ+ ( 𝑧 ≤ 𝑦 ∧ ( ( 𝑥 − 𝑧 ) (,) ( 𝑥 + 𝑧 ) ) ⊆ 𝐴 ) ) ) )
24 10 23 syl ⊢ ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 ∈ ℝ+ → ( ∃ 𝑧 ∈ ℝ+ ( 𝑧 < 𝑦 ∧ ( 𝑥 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑧 ) ⊆ 𝐴 ) → ∃ 𝑧 ∈ ℝ+ ( 𝑧 ≤ 𝑦 ∧ ( ( 𝑥 − 𝑧 ) (,) ( 𝑥 + 𝑧 ) ) ⊆ 𝐴 ) ) ) )
25 9 24 mpdd ⊢ ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 ∈ ℝ+ → ∃ 𝑧 ∈ ℝ+ ( 𝑧 ≤ 𝑦 ∧ ( ( 𝑥 − 𝑧 ) (,) ( 𝑥 + 𝑧 ) ) ⊆ 𝐴 ) ) )
26 25 expimpd ⊢ ( 𝐴 ∈ ( topGen ‘ ran (,) ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑧 ∈ ℝ+ ( 𝑧 ≤ 𝑦 ∧ ( ( 𝑥 − 𝑧 ) (,) ( 𝑥 + 𝑧 ) ) ⊆ 𝐴 ) ) )
27 26 ralrimivv ⊢ ( 𝐴 ∈ ( topGen ‘ ran (,) ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ( 𝑧 ≤ 𝑦 ∧ ( ( 𝑥 − 𝑧 ) (,) ( 𝑥 + 𝑧 ) ) ⊆ 𝐴 ) )
28 6 27 jca ⊢ ( 𝐴 ∈ ( topGen ‘ ran (,) ) → ( 𝐴 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ( 𝑧 ≤ 𝑦 ∧ ( ( 𝑥 − 𝑧 ) (,) ( 𝑥 + 𝑧 ) ) ⊆ 𝐴 ) ) )
29 ssel2 ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℝ )
30 1rp ⊢ 1 ∈ ℝ+
31 simpr ⊢ ( ( 𝑧 ≤ 𝑦 ∧ ( ( 𝑥 − 𝑧 ) (,) ( 𝑥 + 𝑧 ) ) ⊆ 𝐴 ) → ( ( 𝑥 − 𝑧 ) (,) ( 𝑥 + 𝑧 ) ) ⊆ 𝐴 )
32 31 reximi ⊢ ( ∃ 𝑧 ∈ ℝ+ ( 𝑧 ≤ 𝑦 ∧ ( ( 𝑥 − 𝑧 ) (,) ( 𝑥 + 𝑧 ) ) ⊆ 𝐴 ) → ∃ 𝑧 ∈ ℝ+ ( ( 𝑥 − 𝑧 ) (,) ( 𝑥 + 𝑧 ) ) ⊆ 𝐴 )
33 32 ralimi ⊢ ( ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ( 𝑧 ≤ 𝑦 ∧ ( ( 𝑥 − 𝑧 ) (,) ( 𝑥 + 𝑧 ) ) ⊆ 𝐴 ) → ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ( ( 𝑥 − 𝑧 ) (,) ( 𝑥 + 𝑧 ) ) ⊆ 𝐴 )
34 biidd ⊢ ( 𝑦 = 1 → ( ∃ 𝑧 ∈ ℝ+ ( ( 𝑥 − 𝑧 ) (,) ( 𝑥 + 𝑧 ) ) ⊆ 𝐴 ↔ ∃ 𝑧 ∈ ℝ+ ( ( 𝑥 − 𝑧 ) (,) ( 𝑥 + 𝑧 ) ) ⊆ 𝐴 ) )
35 34 rspcv ⊢ ( 1 ∈ ℝ+ → ( ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ( ( 𝑥 − 𝑧 ) (,) ( 𝑥 + 𝑧 ) ) ⊆ 𝐴 → ∃ 𝑧 ∈ ℝ+ ( ( 𝑥 − 𝑧 ) (,) ( 𝑥 + 𝑧 ) ) ⊆ 𝐴 ) )
36 30 33 35 mpsyl ⊢ ( ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ( 𝑧 ≤ 𝑦 ∧ ( ( 𝑥 − 𝑧 ) (,) ( 𝑥 + 𝑧 ) ) ⊆ 𝐴 ) → ∃ 𝑧 ∈ ℝ+ ( ( 𝑥 − 𝑧 ) (,) ( 𝑥 + 𝑧 ) ) ⊆ 𝐴 )
37 14 rexbidva ⊢ ( 𝑥 ∈ ℝ → ( ∃ 𝑧 ∈ ℝ+ ( 𝑥 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑧 ) ⊆ 𝐴 ↔ ∃ 𝑧 ∈ ℝ+ ( ( 𝑥 − 𝑧 ) (,) ( 𝑥 + 𝑧 ) ) ⊆ 𝐴 ) )
38 36 37 syl5ibr ⊢ ( 𝑥 ∈ ℝ → ( ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ( 𝑧 ≤ 𝑦 ∧ ( ( 𝑥 − 𝑧 ) (,) ( 𝑥 + 𝑧 ) ) ⊆ 𝐴 ) → ∃ 𝑧 ∈ ℝ+ ( 𝑥 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑧 ) ⊆ 𝐴 ) )
39 29 38 syl ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ( 𝑧 ≤ 𝑦 ∧ ( ( 𝑥 − 𝑧 ) (,) ( 𝑥 + 𝑧 ) ) ⊆ 𝐴 ) → ∃ 𝑧 ∈ ℝ+ ( 𝑥 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑧 ) ⊆ 𝐴 ) )
40 39 ralimdva ⊢ ( 𝐴 ⊆ ℝ → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ( 𝑧 ≤ 𝑦 ∧ ( ( 𝑥 − 𝑧 ) (,) ( 𝑥 + 𝑧 ) ) ⊆ 𝐴 ) → ∀ 𝑥 ∈ 𝐴 ∃ 𝑧 ∈ ℝ+ ( 𝑥 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑧 ) ⊆ 𝐴 ) )
41 40 imdistani ⊢ ( ( 𝐴 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ( 𝑧 ≤ 𝑦 ∧ ( ( 𝑥 − 𝑧 ) (,) ( 𝑥 + 𝑧 ) ) ⊆ 𝐴 ) ) → ( 𝐴 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑧 ∈ ℝ+ ( 𝑥 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑧 ) ⊆ 𝐴 ) )
42 4 elmopn2 ⊢ ( ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ∈ ( ∞Met ‘ ℝ ) → ( 𝐴 ∈ ( topGen ‘ ran (,) ) ↔ ( 𝐴 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑧 ∈ ℝ+ ( 𝑥 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑧 ) ⊆ 𝐴 ) ) )
43 2 42 ax-mp ⊢ ( 𝐴 ∈ ( topGen ‘ ran (,) ) ↔ ( 𝐴 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑧 ∈ ℝ+ ( 𝑥 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑧 ) ⊆ 𝐴 ) )
44 41 43 sylibr ⊢ ( ( 𝐴 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ( 𝑧 ≤ 𝑦 ∧ ( ( 𝑥 − 𝑧 ) (,) ( 𝑥 + 𝑧 ) ) ⊆ 𝐴 ) ) → 𝐴 ∈ ( topGen ‘ ran (,) ) )
45 28 44 impbii ⊢ ( 𝐴 ∈ ( topGen ‘ ran (,) ) ↔ ( 𝐴 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ( 𝑧 ≤ 𝑦 ∧ ( ( 𝑥 − 𝑧 ) (,) ( 𝑥 + 𝑧 ) ) ⊆ 𝐴 ) ) )