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	$⊢ D = {(abs \circ -) ↾}_{ℝ^{2}}$
	Assertion	blssioo	$⊢ ran ball (D) \subseteq ran (.)$

Proof

Step	Hyp	Ref	Expression
1		remet.1	$⊢ D = {(abs \circ -) ↾}_{ℝ^{2}}$
2	1	rexmet	$⊢ D \in ∞Met (ℝ)$
3		blrn	$⊢ D \in ∞Met (ℝ) \to (z \in ran ball (D) \leftrightarrow \exists y \in ℝ \exists r \in ℝ^{*} z = y ball (D) r)$
4	2 3	ax-mp	$⊢ z \in ran ball (D) \leftrightarrow \exists y \in ℝ \exists r \in ℝ^{*} z = y ball (D) r$
5		elxr	$⊢ r \in ℝ^{*} \leftrightarrow (r \in ℝ \lor r = +∞ \lor r = −∞)$
6	1	bl2ioo	$⊢ (y \in ℝ \land r \in ℝ) \to y ball (D) r = (y - r, y + r)$
7		resubcl	$⊢ (y \in ℝ \land r \in ℝ) \to y - r \in ℝ$
8		readdcl	$⊢ (y \in ℝ \land r \in ℝ) \to y + r \in ℝ$
9		ioof	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ$
10		ffn	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ \to (.) Fn (ℝ^{} \times ℝ^{})$
11	9 10	ax-mp	$⊢ (.) Fn (ℝ^{} \times ℝ^{})$
12		rexr	$⊢ y - r \in ℝ \to y - r \in ℝ^{*}$
13		rexr	$⊢ y + r \in ℝ \to y + r \in ℝ^{*}$
14		fnovrn	$⊢ ((.) Fn (ℝ^{} \times ℝ^{}) \land y - r \in ℝ^{} \land y + r \in ℝ^{}) \to (y - r, y + r) \in ran (.)$
15	11 12 13 14	mp3an3an	$⊢ (y - r \in ℝ \land y + r \in ℝ) \to (y - r, y + r) \in ran (.)$
16	7 8 15	syl2anc	$⊢ (y \in ℝ \land r \in ℝ) \to (y - r, y + r) \in ran (.)$
17	6 16	eqeltrd	$⊢ (y \in ℝ \land r \in ℝ) \to y ball (D) r \in ran (.)$
18		oveq2	$⊢ r = +∞ \to y ball (D) r = y ball (D) +∞$
19	1	remet	$⊢ D \in Met (ℝ)$
20		blpnf	$⊢ (D \in Met (ℝ) \land y \in ℝ) \to y ball (D) +∞ = ℝ$
21	19 20	mpan	$⊢ y \in ℝ \to y ball (D) +∞ = ℝ$
22	18 21	sylan9eqr	$⊢ (y \in ℝ \land r = +∞) \to y ball (D) r = ℝ$
23		ioomax	$⊢ (−∞, +∞) = ℝ$
24		ioorebas	$⊢ (−∞, +∞) \in ran (.)$
25	23 24	eqeltrri	$⊢ ℝ \in ran (.)$
26	22 25	eqeltrdi	$⊢ (y \in ℝ \land r = +∞) \to y ball (D) r \in ran (.)$
27		oveq2	$⊢ r = −∞ \to y ball (D) r = y ball (D) −∞$
28		0xr	$⊢ 0 \in ℝ^{*}$
29		nltmnf	$⊢ 0 \in ℝ^{*} \to \neg 0 < −∞$
30	28 29	ax-mp	$⊢ \neg 0 < −∞$
31		mnfxr	$⊢ −∞ \in ℝ^{*}$
32		xbln0	$⊢ (D \in ∞Met (ℝ) \land y \in ℝ \land −∞ \in ℝ^{*}) \to (y ball (D) −∞ \neq \emptyset \leftrightarrow 0 < −∞)$
33	2 31 32	mp3an13	$⊢ y \in ℝ \to (y ball (D) −∞ \neq \emptyset \leftrightarrow 0 < −∞)$
34	33	necon1bbid	$⊢ y \in ℝ \to (\neg 0 < −∞ \leftrightarrow y ball (D) −∞ = \emptyset)$
35	30 34	mpbii	$⊢ y \in ℝ \to y ball (D) −∞ = \emptyset$
36	27 35	sylan9eqr	$⊢ (y \in ℝ \land r = −∞) \to y ball (D) r = \emptyset$
37		iooid	$⊢ (0, 0) = \emptyset$
38		ioorebas	$⊢ (0, 0) \in ran (.)$
39	37 38	eqeltrri	$⊢ \emptyset \in ran (.)$
40	36 39	eqeltrdi	$⊢ (y \in ℝ \land r = −∞) \to y ball (D) r \in ran (.)$
41	17 26 40	3jaodan	$⊢ (y \in ℝ \land (r \in ℝ \lor r = +∞ \lor r = −∞)) \to y ball (D) r \in ran (.)$
42	5 41	sylan2b	$⊢ (y \in ℝ \land r \in ℝ^{*}) \to y ball (D) r \in ran (.)$
43		eleq1	$⊢ z = y ball (D) r \to (z \in ran (.) \leftrightarrow y ball (D) r \in ran (.))$
44	42 43	syl5ibrcom	$⊢ (y \in ℝ \land r \in ℝ^{*}) \to (z = y ball (D) r \to z \in ran (.))$
45	44	rexlimivv	$⊢ \exists y \in ℝ \exists r \in ℝ^{*} z = y ball (D) r \to z \in ran (.)$
46	4 45	sylbi	$⊢ z \in ran ball (D) \to z \in ran (.)$
47	46	ssriv	$⊢ ran ball (D) \subseteq ran (.)$

Metamath Proof Explorer

Theorem blssioo

Proof