Metamath Proof Explorer


Theorem blcls

Description: The closure of an open ball in a metric space is contained in the corresponding closed ball. (Equality need not hold; for example, with the discrete metric, the closed ball of radius 1 is the whole space, but the open ball of radius 1 is just a point, whose closure is also a point.) (Contributed by Mario Carneiro, 31-Dec-2013)

Ref Expression
Hypotheses mopni.1 𝐽 = ( MetOpen ‘ 𝐷 )
blcld.3 𝑆 = { 𝑧𝑋 ∣ ( 𝑃 𝐷 𝑧 ) ≤ 𝑅 }
Assertion blcls ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑅 ∈ ℝ* ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ⊆ 𝑆 )

Proof

Step Hyp Ref Expression
1 mopni.1 𝐽 = ( MetOpen ‘ 𝐷 )
2 blcld.3 𝑆 = { 𝑧𝑋 ∣ ( 𝑃 𝐷 𝑧 ) ≤ 𝑅 }
3 1 2 blcld ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑅 ∈ ℝ* ) → 𝑆 ∈ ( Clsd ‘ 𝐽 ) )
4 blssm ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑅 ∈ ℝ* ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ⊆ 𝑋 )
5 elbl ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑅 ∈ ℝ* ) → ( 𝑧 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ↔ ( 𝑧𝑋 ∧ ( 𝑃 𝐷 𝑧 ) < 𝑅 ) ) )
6 xmetcl ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑧𝑋 ) → ( 𝑃 𝐷 𝑧 ) ∈ ℝ* )
7 6 3expa ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋 ) ∧ 𝑧𝑋 ) → ( 𝑃 𝐷 𝑧 ) ∈ ℝ* )
8 7 3adantl3 ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑅 ∈ ℝ* ) ∧ 𝑧𝑋 ) → ( 𝑃 𝐷 𝑧 ) ∈ ℝ* )
9 simpl3 ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑅 ∈ ℝ* ) ∧ 𝑧𝑋 ) → 𝑅 ∈ ℝ* )
10 xrltle ( ( ( 𝑃 𝐷 𝑧 ) ∈ ℝ*𝑅 ∈ ℝ* ) → ( ( 𝑃 𝐷 𝑧 ) < 𝑅 → ( 𝑃 𝐷 𝑧 ) ≤ 𝑅 ) )
11 8 9 10 syl2anc ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑅 ∈ ℝ* ) ∧ 𝑧𝑋 ) → ( ( 𝑃 𝐷 𝑧 ) < 𝑅 → ( 𝑃 𝐷 𝑧 ) ≤ 𝑅 ) )
12 11 expimpd ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑅 ∈ ℝ* ) → ( ( 𝑧𝑋 ∧ ( 𝑃 𝐷 𝑧 ) < 𝑅 ) → ( 𝑃 𝐷 𝑧 ) ≤ 𝑅 ) )
13 5 12 sylbid ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑅 ∈ ℝ* ) → ( 𝑧 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) → ( 𝑃 𝐷 𝑧 ) ≤ 𝑅 ) )
14 13 ralrimiv ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑅 ∈ ℝ* ) → ∀ 𝑧 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ( 𝑃 𝐷 𝑧 ) ≤ 𝑅 )
15 ssrab ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ⊆ { 𝑧𝑋 ∣ ( 𝑃 𝐷 𝑧 ) ≤ 𝑅 } ↔ ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ⊆ 𝑋 ∧ ∀ 𝑧 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ( 𝑃 𝐷 𝑧 ) ≤ 𝑅 ) )
16 4 14 15 sylanbrc ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑅 ∈ ℝ* ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ⊆ { 𝑧𝑋 ∣ ( 𝑃 𝐷 𝑧 ) ≤ 𝑅 } )
17 16 2 sseqtrrdi ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑅 ∈ ℝ* ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ⊆ 𝑆 )
18 eqid 𝐽 = 𝐽
19 18 clsss2 ( ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ⊆ 𝑆 ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ⊆ 𝑆 )
20 3 17 19 syl2anc ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑅 ∈ ℝ* ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ) ⊆ 𝑆 )