Metamath Proof Explorer

Theorem blssioo

Description: The balls of the standard real metric space are included in the open real intervals. (Contributed by NM, 8-May-2007) (Revised by Mario Carneiro, 13-Nov-2013)

Ref Expression
Hypothesis remet.1 ⊒ 𝐷 = ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) )
Assertion blssioo ran ( ball β€˜ 𝐷 ) βŠ† ran (,)

Proof

Step Hyp Ref Expression
1 remet.1 ⊒ 𝐷 = ( ( abs ∘ βˆ’ ) β†Ύ ( ℝ Γ— ℝ ) )
2 1 rexmet ⊒ 𝐷 ∈ ( ∞Met β€˜ ℝ )
3 blrn ⊒ ( 𝐷 ∈ ( ∞Met β€˜ ℝ ) β†’ ( 𝑧 ∈ ran ( ball β€˜ 𝐷 ) ↔ βˆƒ 𝑦 ∈ ℝ βˆƒ π‘Ÿ ∈ ℝ* 𝑧 = ( 𝑦 ( ball β€˜ 𝐷 ) π‘Ÿ ) ) )
4 2 3 ax-mp ⊒ ( 𝑧 ∈ ran ( ball β€˜ 𝐷 ) ↔ βˆƒ 𝑦 ∈ ℝ βˆƒ π‘Ÿ ∈ ℝ* 𝑧 = ( 𝑦 ( ball β€˜ 𝐷 ) π‘Ÿ ) )
5 elxr ⊒ ( π‘Ÿ ∈ ℝ* ↔ ( π‘Ÿ ∈ ℝ ∨ π‘Ÿ = +∞ ∨ π‘Ÿ = -∞ ) )
6 1 bl2ioo ⊒ ( ( 𝑦 ∈ ℝ ∧ π‘Ÿ ∈ ℝ ) β†’ ( 𝑦 ( ball β€˜ 𝐷 ) π‘Ÿ ) = ( ( 𝑦 βˆ’ π‘Ÿ ) (,) ( 𝑦 + π‘Ÿ ) ) )
7 resubcl ⊒ ( ( 𝑦 ∈ ℝ ∧ π‘Ÿ ∈ ℝ ) β†’ ( 𝑦 βˆ’ π‘Ÿ ) ∈ ℝ )
8 readdcl ⊒ ( ( 𝑦 ∈ ℝ ∧ π‘Ÿ ∈ ℝ ) β†’ ( 𝑦 + π‘Ÿ ) ∈ ℝ )
9 ioof ⊒ (,) : ( ℝ* Γ— ℝ* ) ⟢ 𝒫 ℝ
10 ffn ⊒ ( (,) : ( ℝ* Γ— ℝ* ) ⟢ 𝒫 ℝ β†’ (,) Fn ( ℝ* Γ— ℝ* ) )
11 9 10 ax-mp ⊒ (,) Fn ( ℝ* Γ— ℝ* )
12 rexr ⊒ ( ( 𝑦 βˆ’ π‘Ÿ ) ∈ ℝ β†’ ( 𝑦 βˆ’ π‘Ÿ ) ∈ ℝ* )
13 rexr ⊒ ( ( 𝑦 + π‘Ÿ ) ∈ ℝ β†’ ( 𝑦 + π‘Ÿ ) ∈ ℝ* )
14 fnovrn ⊒ ( ( (,) Fn ( ℝ* Γ— ℝ* ) ∧ ( 𝑦 βˆ’ π‘Ÿ ) ∈ ℝ* ∧ ( 𝑦 + π‘Ÿ ) ∈ ℝ* ) β†’ ( ( 𝑦 βˆ’ π‘Ÿ ) (,) ( 𝑦 + π‘Ÿ ) ) ∈ ran (,) )
15 11 12 13 14 mp3an3an ⊒ ( ( ( 𝑦 βˆ’ π‘Ÿ ) ∈ ℝ ∧ ( 𝑦 + π‘Ÿ ) ∈ ℝ ) β†’ ( ( 𝑦 βˆ’ π‘Ÿ ) (,) ( 𝑦 + π‘Ÿ ) ) ∈ ran (,) )
16 7 8 15 syl2anc ⊒ ( ( 𝑦 ∈ ℝ ∧ π‘Ÿ ∈ ℝ ) β†’ ( ( 𝑦 βˆ’ π‘Ÿ ) (,) ( 𝑦 + π‘Ÿ ) ) ∈ ran (,) )
17 6 16 eqeltrd ⊒ ( ( 𝑦 ∈ ℝ ∧ π‘Ÿ ∈ ℝ ) β†’ ( 𝑦 ( ball β€˜ 𝐷 ) π‘Ÿ ) ∈ ran (,) )
18 oveq2 ⊒ ( π‘Ÿ = +∞ β†’ ( 𝑦 ( ball β€˜ 𝐷 ) π‘Ÿ ) = ( 𝑦 ( ball β€˜ 𝐷 ) +∞ ) )
19 1 remet ⊒ 𝐷 ∈ ( Met β€˜ ℝ )
20 blpnf ⊒ ( ( 𝐷 ∈ ( Met β€˜ ℝ ) ∧ 𝑦 ∈ ℝ ) β†’ ( 𝑦 ( ball β€˜ 𝐷 ) +∞ ) = ℝ )
21 19 20 mpan ⊒ ( 𝑦 ∈ ℝ β†’ ( 𝑦 ( ball β€˜ 𝐷 ) +∞ ) = ℝ )
22 18 21 sylan9eqr ⊒ ( ( 𝑦 ∈ ℝ ∧ π‘Ÿ = +∞ ) β†’ ( 𝑦 ( ball β€˜ 𝐷 ) π‘Ÿ ) = ℝ )
23 ioomax ⊒ ( -∞ (,) +∞ ) = ℝ
24 ioorebas ⊒ ( -∞ (,) +∞ ) ∈ ran (,)
25 23 24 eqeltrri ⊒ ℝ ∈ ran (,)
26 22 25 eqeltrdi ⊒ ( ( 𝑦 ∈ ℝ ∧ π‘Ÿ = +∞ ) β†’ ( 𝑦 ( ball β€˜ 𝐷 ) π‘Ÿ ) ∈ ran (,) )
27 oveq2 ⊒ ( π‘Ÿ = -∞ β†’ ( 𝑦 ( ball β€˜ 𝐷 ) π‘Ÿ ) = ( 𝑦 ( ball β€˜ 𝐷 ) -∞ ) )
28 0xr ⊒ 0 ∈ ℝ*
29 nltmnf ⊒ ( 0 ∈ ℝ* β†’ Β¬ 0 < -∞ )
30 28 29 ax-mp ⊒ ¬ 0 < -∞
31 mnfxr ⊒ -∞ ∈ ℝ*
32 xbln0 ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ ℝ ) ∧ 𝑦 ∈ ℝ ∧ -∞ ∈ ℝ* ) β†’ ( ( 𝑦 ( ball β€˜ 𝐷 ) -∞ ) β‰  βˆ… ↔ 0 < -∞ ) )
33 2 31 32 mp3an13 ⊒ ( 𝑦 ∈ ℝ β†’ ( ( 𝑦 ( ball β€˜ 𝐷 ) -∞ ) β‰  βˆ… ↔ 0 < -∞ ) )
34 33 necon1bbid ⊒ ( 𝑦 ∈ ℝ β†’ ( Β¬ 0 < -∞ ↔ ( 𝑦 ( ball β€˜ 𝐷 ) -∞ ) = βˆ… ) )
35 30 34 mpbii ⊒ ( 𝑦 ∈ ℝ β†’ ( 𝑦 ( ball β€˜ 𝐷 ) -∞ ) = βˆ… )
36 27 35 sylan9eqr ⊒ ( ( 𝑦 ∈ ℝ ∧ π‘Ÿ = -∞ ) β†’ ( 𝑦 ( ball β€˜ 𝐷 ) π‘Ÿ ) = βˆ… )
37 iooid ⊒ ( 0 (,) 0 ) = βˆ…
38 ioorebas ⊒ ( 0 (,) 0 ) ∈ ran (,)
39 37 38 eqeltrri ⊒ βˆ… ∈ ran (,)
40 36 39 eqeltrdi ⊒ ( ( 𝑦 ∈ ℝ ∧ π‘Ÿ = -∞ ) β†’ ( 𝑦 ( ball β€˜ 𝐷 ) π‘Ÿ ) ∈ ran (,) )
41 17 26 40 3jaodan ⊒ ( ( 𝑦 ∈ ℝ ∧ ( π‘Ÿ ∈ ℝ ∨ π‘Ÿ = +∞ ∨ π‘Ÿ = -∞ ) ) β†’ ( 𝑦 ( ball β€˜ 𝐷 ) π‘Ÿ ) ∈ ran (,) )
42 5 41 sylan2b ⊒ ( ( 𝑦 ∈ ℝ ∧ π‘Ÿ ∈ ℝ* ) β†’ ( 𝑦 ( ball β€˜ 𝐷 ) π‘Ÿ ) ∈ ran (,) )
43 eleq1 ⊒ ( 𝑧 = ( 𝑦 ( ball β€˜ 𝐷 ) π‘Ÿ ) β†’ ( 𝑧 ∈ ran (,) ↔ ( 𝑦 ( ball β€˜ 𝐷 ) π‘Ÿ ) ∈ ran (,) ) )
44 42 43 syl5ibrcom ⊒ ( ( 𝑦 ∈ ℝ ∧ π‘Ÿ ∈ ℝ* ) β†’ ( 𝑧 = ( 𝑦 ( ball β€˜ 𝐷 ) π‘Ÿ ) β†’ 𝑧 ∈ ran (,) ) )
45 44 rexlimivv ⊒ ( βˆƒ 𝑦 ∈ ℝ βˆƒ π‘Ÿ ∈ ℝ* 𝑧 = ( 𝑦 ( ball β€˜ 𝐷 ) π‘Ÿ ) β†’ 𝑧 ∈ ran (,) )
46 4 45 sylbi ⊒ ( 𝑧 ∈ ran ( ball β€˜ 𝐷 ) β†’ 𝑧 ∈ ran (,) )
47 46 ssriv ⊒ ran ( ball β€˜ 𝐷 ) βŠ† ran (,)