This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem blsscls

Description: If two concentric balls have different radii, the closure of the smaller one is contained in the larger one. (Contributed by Mario Carneiro, 5-Jan-2014)

		Ref	Expression
	Hypothesis	blsscls.2	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
	Assertion	blsscls	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑆 ∈ ℝ^* ∧ 𝑅 < 𝑆 ) ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ⊆ ( 𝑃 ( ball ‘ 𝐷 ) 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		blsscls.2	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2		eqid	⊢ { 𝑥 ∈ 𝑋 ∣ ( 𝑃 𝐷 𝑥 ) ≤ 𝑅 } = { 𝑥 ∈ 𝑋 ∣ ( 𝑃 𝐷 𝑥 ) ≤ 𝑅 }
3	1 2	blcls	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ^* ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ⊆ { 𝑥 ∈ 𝑋 ∣ ( 𝑃 𝐷 𝑥 ) ≤ 𝑅 } )
4	3	3expa	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ⊆ { 𝑥 ∈ 𝑋 ∣ ( 𝑃 𝐷 𝑥 ) ≤ 𝑅 } )
5	4	3ad2antr1	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑆 ∈ ℝ^* ∧ 𝑅 < 𝑆 ) ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ⊆ { 𝑥 ∈ 𝑋 ∣ ( 𝑃 𝐷 𝑥 ) ≤ 𝑅 } )
6	1 2	blsscls2	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑆 ∈ ℝ^* ∧ 𝑅 < 𝑆 ) ) → { 𝑥 ∈ 𝑋 ∣ ( 𝑃 𝐷 𝑥 ) ≤ 𝑅 } ⊆ ( 𝑃 ( ball ‘ 𝐷 ) 𝑆 ) )
7	5 6	sstrd	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ ( 𝑅 ∈ ℝ^* ∧ 𝑆 ∈ ℝ^* ∧ 𝑅 < 𝑆 ) ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ⊆ ( 𝑃 ( ball ‘ 𝐷 ) 𝑆 ) )