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	⊢ 𝐷 = ( dist ‘ ℝ^*_𝑠 )
	Assertion	xrsblre	⊢ ( ( 𝑃 ∈ ℝ ∧ 𝑅 ∈ ℝ^* ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ⊆ ℝ )

Proof

Step	Hyp	Ref	Expression
1		xrsxmet.1	⊢ 𝐷 = ( dist ‘ ℝ^*_𝑠 )
2		rexr	⊢ ( 𝑃 ∈ ℝ → 𝑃 ∈ ℝ^* )
3	1	xrsxmet	⊢ 𝐷 ∈ ( ∞Met ‘ ℝ^* )
4		eqid	⊢ ( ^◡ 𝐷 “ ℝ ) = ( ^◡ 𝐷 “ ℝ )
5	4	blssec	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ ℝ^* ) ∧ 𝑃 ∈ ℝ^* ∧ 𝑅 ∈ ℝ^* ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ⊆ [ 𝑃 ] ( ^◡ 𝐷 “ ℝ ) )
6	3 5	mp3an1	⊢ ( ( 𝑃 ∈ ℝ^* ∧ 𝑅 ∈ ℝ^* ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ⊆ [ 𝑃 ] ( ^◡ 𝐷 “ ℝ ) )
7	2 6	sylan	⊢ ( ( 𝑃 ∈ ℝ ∧ 𝑅 ∈ ℝ^* ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ⊆ [ 𝑃 ] ( ^◡ 𝐷 “ ℝ ) )
8		vex	⊢ 𝑥 ∈ V
9		simpl	⊢ ( ( 𝑃 ∈ ℝ ∧ 𝑅 ∈ ℝ^* ) → 𝑃 ∈ ℝ )
10		elecg	⊢ ( ( 𝑥 ∈ V ∧ 𝑃 ∈ ℝ ) → ( 𝑥 ∈ [ 𝑃 ] ( ^◡ 𝐷 “ ℝ ) ↔ 𝑃 ( ^◡ 𝐷 “ ℝ ) 𝑥 ) )
11	8 9 10	sylancr	⊢ ( ( 𝑃 ∈ ℝ ∧ 𝑅 ∈ ℝ^* ) → ( 𝑥 ∈ [ 𝑃 ] ( ^◡ 𝐷 “ ℝ ) ↔ 𝑃 ( ^◡ 𝐷 “ ℝ ) 𝑥 ) )
12	4	xmeterval	⊢ ( 𝐷 ∈ ( ∞Met ‘ ℝ^* ) → ( 𝑃 ( ^◡ 𝐷 “ ℝ ) 𝑥 ↔ ( 𝑃 ∈ ℝ^* ∧ 𝑥 ∈ ℝ^* ∧ ( 𝑃 𝐷 𝑥 ) ∈ ℝ ) ) )
13	3 12	ax-mp	⊢ ( 𝑃 ( ^◡ 𝐷 “ ℝ ) 𝑥 ↔ ( 𝑃 ∈ ℝ^* ∧ 𝑥 ∈ ℝ^* ∧ ( 𝑃 𝐷 𝑥 ) ∈ ℝ ) )
14		simpr	⊢ ( ( ( ( 𝑃 ∈ ℝ ∧ 𝑅 ∈ ℝ^* ) ∧ ( 𝑃 ∈ ℝ^* ∧ 𝑥 ∈ ℝ^* ∧ ( 𝑃 𝐷 𝑥 ) ∈ ℝ ) ) ∧ 𝑃 = 𝑥 ) → 𝑃 = 𝑥 )
15		simplll	⊢ ( ( ( ( 𝑃 ∈ ℝ ∧ 𝑅 ∈ ℝ^* ) ∧ ( 𝑃 ∈ ℝ^* ∧ 𝑥 ∈ ℝ^* ∧ ( 𝑃 𝐷 𝑥 ) ∈ ℝ ) ) ∧ 𝑃 = 𝑥 ) → 𝑃 ∈ ℝ )
16	14 15	eqeltrrd	⊢ ( ( ( ( 𝑃 ∈ ℝ ∧ 𝑅 ∈ ℝ^* ) ∧ ( 𝑃 ∈ ℝ^* ∧ 𝑥 ∈ ℝ^* ∧ ( 𝑃 𝐷 𝑥 ) ∈ ℝ ) ) ∧ 𝑃 = 𝑥 ) → 𝑥 ∈ ℝ )
17		simplr3	⊢ ( ( ( ( 𝑃 ∈ ℝ ∧ 𝑅 ∈ ℝ^* ) ∧ ( 𝑃 ∈ ℝ^* ∧ 𝑥 ∈ ℝ^* ∧ ( 𝑃 𝐷 𝑥 ) ∈ ℝ ) ) ∧ 𝑃 ≠ 𝑥 ) → ( 𝑃 𝐷 𝑥 ) ∈ ℝ )
18		simplr1	⊢ ( ( ( ( 𝑃 ∈ ℝ ∧ 𝑅 ∈ ℝ^* ) ∧ ( 𝑃 ∈ ℝ^* ∧ 𝑥 ∈ ℝ^* ∧ ( 𝑃 𝐷 𝑥 ) ∈ ℝ ) ) ∧ 𝑃 ≠ 𝑥 ) → 𝑃 ∈ ℝ^* )
19		simplr2	⊢ ( ( ( ( 𝑃 ∈ ℝ ∧ 𝑅 ∈ ℝ^* ) ∧ ( 𝑃 ∈ ℝ^* ∧ 𝑥 ∈ ℝ^* ∧ ( 𝑃 𝐷 𝑥 ) ∈ ℝ ) ) ∧ 𝑃 ≠ 𝑥 ) → 𝑥 ∈ ℝ^* )
20		simpr	⊢ ( ( ( ( 𝑃 ∈ ℝ ∧ 𝑅 ∈ ℝ^* ) ∧ ( 𝑃 ∈ ℝ^* ∧ 𝑥 ∈ ℝ^* ∧ ( 𝑃 𝐷 𝑥 ) ∈ ℝ ) ) ∧ 𝑃 ≠ 𝑥 ) → 𝑃 ≠ 𝑥 )
21	1	xrsdsreclb	⊢ ( ( 𝑃 ∈ ℝ^* ∧ 𝑥 ∈ ℝ^* ∧ 𝑃 ≠ 𝑥 ) → ( ( 𝑃 𝐷 𝑥 ) ∈ ℝ ↔ ( 𝑃 ∈ ℝ ∧ 𝑥 ∈ ℝ ) ) )
22	18 19 20 21	syl3anc	⊢ ( ( ( ( 𝑃 ∈ ℝ ∧ 𝑅 ∈ ℝ^* ) ∧ ( 𝑃 ∈ ℝ^* ∧ 𝑥 ∈ ℝ^* ∧ ( 𝑃 𝐷 𝑥 ) ∈ ℝ ) ) ∧ 𝑃 ≠ 𝑥 ) → ( ( 𝑃 𝐷 𝑥 ) ∈ ℝ ↔ ( 𝑃 ∈ ℝ ∧ 𝑥 ∈ ℝ ) ) )
23	17 22	mpbid	⊢ ( ( ( ( 𝑃 ∈ ℝ ∧ 𝑅 ∈ ℝ^* ) ∧ ( 𝑃 ∈ ℝ^* ∧ 𝑥 ∈ ℝ^* ∧ ( 𝑃 𝐷 𝑥 ) ∈ ℝ ) ) ∧ 𝑃 ≠ 𝑥 ) → ( 𝑃 ∈ ℝ ∧ 𝑥 ∈ ℝ ) )
24	23	simprd	⊢ ( ( ( ( 𝑃 ∈ ℝ ∧ 𝑅 ∈ ℝ^* ) ∧ ( 𝑃 ∈ ℝ^* ∧ 𝑥 ∈ ℝ^* ∧ ( 𝑃 𝐷 𝑥 ) ∈ ℝ ) ) ∧ 𝑃 ≠ 𝑥 ) → 𝑥 ∈ ℝ )
25	16 24	pm2.61dane	⊢ ( ( ( 𝑃 ∈ ℝ ∧ 𝑅 ∈ ℝ^* ) ∧ ( 𝑃 ∈ ℝ^* ∧ 𝑥 ∈ ℝ^* ∧ ( 𝑃 𝐷 𝑥 ) ∈ ℝ ) ) → 𝑥 ∈ ℝ )
26	25	ex	⊢ ( ( 𝑃 ∈ ℝ ∧ 𝑅 ∈ ℝ^* ) → ( ( 𝑃 ∈ ℝ^* ∧ 𝑥 ∈ ℝ^* ∧ ( 𝑃 𝐷 𝑥 ) ∈ ℝ ) → 𝑥 ∈ ℝ ) )
27	13 26	biimtrid	⊢ ( ( 𝑃 ∈ ℝ ∧ 𝑅 ∈ ℝ^* ) → ( 𝑃 ( ^◡ 𝐷 “ ℝ ) 𝑥 → 𝑥 ∈ ℝ ) )
28	11 27	sylbid	⊢ ( ( 𝑃 ∈ ℝ ∧ 𝑅 ∈ ℝ^* ) → ( 𝑥 ∈ [ 𝑃 ] ( ^◡ 𝐷 “ ℝ ) → 𝑥 ∈ ℝ ) )
29	28	ssrdv	⊢ ( ( 𝑃 ∈ ℝ ∧ 𝑅 ∈ ℝ^* ) → [ 𝑃 ] ( ^◡ 𝐷 “ ℝ ) ⊆ ℝ )
30	7 29	sstrd	⊢ ( ( 𝑃 ∈ ℝ ∧ 𝑅 ∈ ℝ^* ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ⊆ ℝ )

Metamath Proof Explorer

Theorem xrsblre

Proof