Metamath Proof Explorer

Theorem ssbl

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

Ref Expression
Assertion ssbl ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ) ∧ 𝑅 ≀ 𝑆 ) β†’ ( 𝑃 ( ball β€˜ 𝐷 ) 𝑅 ) βŠ† ( 𝑃 ( ball β€˜ 𝐷 ) 𝑆 ) )

Proof

Step Hyp Ref Expression
1 simp1l ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ) ∧ 𝑅 ≀ 𝑆 ) β†’ 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) )
2 simp1r ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ) ∧ 𝑅 ≀ 𝑆 ) β†’ 𝑃 ∈ 𝑋 )
3 simp2l ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ) ∧ 𝑅 ≀ 𝑆 ) β†’ 𝑅 ∈ ℝ* )
4 simp2r ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ) ∧ 𝑅 ≀ 𝑆 ) β†’ 𝑆 ∈ ℝ* )
5 xmet0 ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) β†’ ( 𝑃 𝐷 𝑃 ) = 0 )
6 5 3ad2ant1 ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ) ∧ 𝑅 ≀ 𝑆 ) β†’ ( 𝑃 𝐷 𝑃 ) = 0 )
7 0re ⊒ 0 ∈ ℝ
8 6 7 eqeltrdi ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ) ∧ 𝑅 ≀ 𝑆 ) β†’ ( 𝑃 𝐷 𝑃 ) ∈ ℝ )
9 simp3 ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ) ∧ 𝑅 ≀ 𝑆 ) β†’ 𝑅 ≀ 𝑆 )
10 xsubge0 ⊒ ( ( 𝑆 ∈ ℝ* ∧ 𝑅 ∈ ℝ* ) β†’ ( 0 ≀ ( 𝑆 +𝑒 -𝑒 𝑅 ) ↔ 𝑅 ≀ 𝑆 ) )
11 4 3 10 syl2anc ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ) ∧ 𝑅 ≀ 𝑆 ) β†’ ( 0 ≀ ( 𝑆 +𝑒 -𝑒 𝑅 ) ↔ 𝑅 ≀ 𝑆 ) )
12 9 11 mpbird ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ) ∧ 𝑅 ≀ 𝑆 ) β†’ 0 ≀ ( 𝑆 +𝑒 -𝑒 𝑅 ) )
13 6 12 eqbrtrd ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ) ∧ 𝑅 ≀ 𝑆 ) β†’ ( 𝑃 𝐷 𝑃 ) ≀ ( 𝑆 +𝑒 -𝑒 𝑅 ) )
14 1 2 2 3 4 8 13 xblss2 ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ) ∧ 𝑅 ≀ 𝑆 ) β†’ ( 𝑃 ( ball β€˜ 𝐷 ) 𝑅 ) βŠ† ( 𝑃 ( ball β€˜ 𝐷 ) 𝑆 ) )