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 (,)