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 ⊢ J = MetOpen ⁡ D
Assertion blsscls ⊢ D ∈ ∞Met ⁡ X ∧ P ∈ X ∧ R ∈ ℝ * ∧ S ∈ ℝ * ∧ R < S → cls ⁡ J ⁡ P ball ⁡ D R ⊆ P ball ⁡ D S

Proof

Step Hyp Ref Expression
1 blsscls.2 ⊢ J = MetOpen ⁡ D
2 eqid ⊢ x ∈ X | P D x ≤ R = x ∈ X | P D x ≤ R
3 1 2 blcls ⊢ D ∈ ∞Met ⁡ X ∧ P ∈ X ∧ R ∈ ℝ * → cls ⁡ J ⁡ P ball ⁡ D R ⊆ x ∈ X | P D x ≤ R
4 3 3expa ⊢ D ∈ ∞Met ⁡ X ∧ P ∈ X ∧ R ∈ ℝ * → cls ⁡ J ⁡ P ball ⁡ D R ⊆ x ∈ X | P D x ≤ R
5 4 3ad2antr1 ⊢ D ∈ ∞Met ⁡ X ∧ P ∈ X ∧ R ∈ ℝ * ∧ S ∈ ℝ * ∧ R < S → cls ⁡ J ⁡ P ball ⁡ D R ⊆ x ∈ X | P D x ≤ R
6 1 2 blsscls2 ⊢ D ∈ ∞Met ⁡ X ∧ P ∈ X ∧ R ∈ ℝ * ∧ S ∈ ℝ * ∧ R < S → x ∈ X | P D x ≤ R ⊆ P ball ⁡ D S
7 5 6 sstrd ⊢ D ∈ ∞Met ⁡ X ∧ P ∈ X ∧ R ∈ ℝ * ∧ S ∈ ℝ * ∧ R < S → cls ⁡ J ⁡ P ball ⁡ D R ⊆ P ball ⁡ D S