Theorem ssblps

Description: The size of a ball increases monotonically with its radius. (Contributed by NM, 20-Sep-2007) (Revised by Mario Carneiro, 24-Aug-2015) (Revised by Thierry Arnoux, 11-Mar-2018)

	Ref	Expression
Assertion	ssblps	⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ) ∧ 𝑅 ≤ 𝑆 ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ⊆ ( 𝑃 ( ball ‘ 𝐷 ) 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		simp1l	⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ) ∧ 𝑅 ≤ 𝑆 ) → 𝐷 ∈ ( PsMet ‘ 𝑋 ) )
2		simp1r	⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ) ∧ 𝑅 ≤ 𝑆 ) → 𝑃 ∈ 𝑋 )
3		simp2l	⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ) ∧ 𝑅 ≤ 𝑆 ) → 𝑅 ∈ ℝ* )
4		simp2r	⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ) ∧ 𝑅 ≤ 𝑆 ) → 𝑆 ∈ ℝ* )
5		psmet0	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝑃 𝐷 𝑃 ) = 0 )
6	5	3ad2ant1	⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ) ∧ 𝑅 ≤ 𝑆 ) → ( 𝑃 𝐷 𝑃 ) = 0 )
7		0re	⊢ 0 ∈ ℝ
8	6 7	eqeltrdi	⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ) ∧ 𝑅 ≤ 𝑆 ) → ( 𝑃 𝐷 𝑃 ) ∈ ℝ )
9		simp3	⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ) ∧ 𝑅 ≤ 𝑆 ) → 𝑅 ≤ 𝑆 )
10		xsubge0	⊢ ( ( 𝑆 ∈ ℝ* ∧ 𝑅 ∈ ℝ* ) → ( 0 ≤ ( 𝑆 +𝑒 -𝑒 𝑅 ) ↔ 𝑅 ≤ 𝑆 ) )
11	4 3 10	syl2anc	⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ) ∧ 𝑅 ≤ 𝑆 ) → ( 0 ≤ ( 𝑆 +𝑒 -𝑒 𝑅 ) ↔ 𝑅 ≤ 𝑆 ) )
12	9 11	mpbird	⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ) ∧ 𝑅 ≤ 𝑆 ) → 0 ≤ ( 𝑆 +𝑒 -𝑒 𝑅 ) )
13	6 12	eqbrtrd	⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ) ∧ 𝑅 ≤ 𝑆 ) → ( 𝑃 𝐷 𝑃 ) ≤ ( 𝑆 +𝑒 -𝑒 𝑅 ) )
14	1 2 2 3 4 8 13	xblss2ps	⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ) ∧ 𝑅 ≤ 𝑆 ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ⊆ ( 𝑃 ( ball ‘ 𝐷 ) 𝑆 ) )