Metamath Proof Explorer

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 (,) ) ↔ ( 𝐴 βŠ† ℝ ∧ βˆ€ π‘₯ ∈ 𝐴 βˆƒ 𝑦 ∈ ℝ+ ( ( π‘₯ βˆ’ 𝑦 ) (,) ( π‘₯ + 𝑦 ) ) βŠ† 𝐴 ) )