xrsblre

Description: Any ball of the metric of the extended reals centered on an element of RR is entirely contained in RR . (Contributed by Mario Carneiro, 4-Sep-2015)

		Ref	Expression
	Hypothesis	xrsxmet.1	$⊢ D = dist (ℝ_{𝑠}^{*})$
	Assertion	xrsblre	$⊢ (P \in ℝ \land R \in ℝ^{*}) \to P ball (D) R \subseteq ℝ$

Proof

Step	Hyp	Ref	Expression
1		xrsxmet.1	$⊢ D = dist (ℝ_{𝑠}^{*})$
2		rexr	$⊢ P \in ℝ \to P \in ℝ^{*}$
3	1	xrsxmet	$⊢ D \in ∞Met (ℝ^{*})$
4		eqid	$⊢ D^{-1} [ℝ] = D^{-1} [ℝ]$
5	4	blssec	$⊢ (D \in ∞Met (ℝ^{}) \land P \in ℝ^{} \land R \in ℝ^{*}) \to P ball (D) R \subseteq [P] D^{-1} [ℝ]$
6	3 5	mp3an1	$⊢ (P \in ℝ^{} \land R \in ℝ^{}) \to P ball (D) R \subseteq [P] D^{-1} [ℝ]$
7	2 6	sylan	$⊢ (P \in ℝ \land R \in ℝ^{*}) \to P ball (D) R \subseteq [P] D^{-1} [ℝ]$
8		vex	$⊢ x \in V$
9		simpl	$⊢ (P \in ℝ \land R \in ℝ^{*}) \to P \in ℝ$
10		elecg	$⊢ (x \in V \land P \in ℝ) \to (x \in [P] D^{-1} [ℝ] \leftrightarrow P D^{-1} [ℝ] x)$
11	8 9 10	sylancr	$⊢ (P \in ℝ \land R \in ℝ^{*}) \to (x \in [P] D^{-1} [ℝ] \leftrightarrow P D^{-1} [ℝ] x)$
12	4	xmeterval	$⊢ D \in ∞Met (ℝ^{}) \to (P D^{-1} [ℝ] x \leftrightarrow (P \in ℝ^{} \land x \in ℝ^{*} \land P D x \in ℝ))$
13	3 12	ax-mp	$⊢ P D^{-1} [ℝ] x \leftrightarrow (P \in ℝ^{} \land x \in ℝ^{} \land P D x \in ℝ)$
14		simpr	$⊢ (((P \in ℝ \land R \in ℝ^{}) \land (P \in ℝ^{} \land x \in ℝ^{*} \land P D x \in ℝ)) \land P = x) \to P = x$
15		simplll	$⊢ (((P \in ℝ \land R \in ℝ^{}) \land (P \in ℝ^{} \land x \in ℝ^{*} \land P D x \in ℝ)) \land P = x) \to P \in ℝ$
16	14 15	eqeltrrd	$⊢ (((P \in ℝ \land R \in ℝ^{}) \land (P \in ℝ^{} \land x \in ℝ^{*} \land P D x \in ℝ)) \land P = x) \to x \in ℝ$
17		simplr3	$⊢ (((P \in ℝ \land R \in ℝ^{}) \land (P \in ℝ^{} \land x \in ℝ^{*} \land P D x \in ℝ)) \land P \neq x) \to P D x \in ℝ$
18		simplr1	$⊢ (((P \in ℝ \land R \in ℝ^{}) \land (P \in ℝ^{} \land x \in ℝ^{} \land P D x \in ℝ)) \land P \neq x) \to P \in ℝ^{}$
19		simplr2	$⊢ (((P \in ℝ \land R \in ℝ^{}) \land (P \in ℝ^{} \land x \in ℝ^{} \land P D x \in ℝ)) \land P \neq x) \to x \in ℝ^{}$
20		simpr	$⊢ (((P \in ℝ \land R \in ℝ^{}) \land (P \in ℝ^{} \land x \in ℝ^{*} \land P D x \in ℝ)) \land P \neq x) \to P \neq x$
21	1	xrsdsreclb	$⊢ (P \in ℝ^{} \land x \in ℝ^{} \land P \neq x) \to (P D x \in ℝ \leftrightarrow (P \in ℝ \land x \in ℝ))$
22	18 19 20 21	syl3anc	$⊢ (((P \in ℝ \land R \in ℝ^{}) \land (P \in ℝ^{} \land x \in ℝ^{*} \land P D x \in ℝ)) \land P \neq x) \to (P D x \in ℝ \leftrightarrow (P \in ℝ \land x \in ℝ))$
23	17 22	mpbid	$⊢ (((P \in ℝ \land R \in ℝ^{}) \land (P \in ℝ^{} \land x \in ℝ^{*} \land P D x \in ℝ)) \land P \neq x) \to (P \in ℝ \land x \in ℝ)$
24	23	simprd	$⊢ (((P \in ℝ \land R \in ℝ^{}) \land (P \in ℝ^{} \land x \in ℝ^{*} \land P D x \in ℝ)) \land P \neq x) \to x \in ℝ$
25	16 24	pm2.61dane	$⊢ ((P \in ℝ \land R \in ℝ^{}) \land (P \in ℝ^{} \land x \in ℝ^{*} \land P D x \in ℝ)) \to x \in ℝ$
26	25	ex	$⊢ (P \in ℝ \land R \in ℝ^{}) \to ((P \in ℝ^{} \land x \in ℝ^{*} \land P D x \in ℝ) \to x \in ℝ)$
27	13 26	biimtrid	$⊢ (P \in ℝ \land R \in ℝ^{*}) \to (P D^{-1} [ℝ] x \to x \in ℝ)$
28	11 27	sylbid	$⊢ (P \in ℝ \land R \in ℝ^{*}) \to (x \in [P] D^{-1} [ℝ] \to x \in ℝ)$
29	28	ssrdv	$⊢ (P \in ℝ \land R \in ℝ^{*}) \to [P] D^{-1} [ℝ] \subseteq ℝ$
30	7 29	sstrd	$⊢ (P \in ℝ \land R \in ℝ^{*}) \to P ball (D) R \subseteq ℝ$

Metamath Proof Explorer

Theorem xrsblre

Proof