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 β€˜ 𝐷 ) 𝑅 ) ) βŠ† 𝑆 )