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 ‘ 𝐷 ) 𝑅 ) ) ⊆ 𝑆 )

Metamath Proof Explorer

Theorem blcls

Proof