Metamath Proof Explorer

Theorem unirnbl

Description: The union of the set of balls of a metric space is its base set. (Contributed by NM, 12-Sep-2006) (Revised by Mario Carneiro, 12-Nov-2013)

		Ref	Expression
	Assertion	unirnbl	$⊢ D \in ∞Met (X) \to ⋃ ran ball (D) = X$

Proof

Step	Hyp	Ref	Expression
1		blf	$⊢ D \in ∞Met (X) \to ball (D) : X \times ℝ^{*} ⟶ 𝒫 X$
2	1	frnd	$⊢ D \in ∞Met (X) \to ran ball (D) \subseteq 𝒫 X$
3		sspwuni	$⊢ ran ball (D) \subseteq 𝒫 X \leftrightarrow ⋃ ran ball (D) \subseteq X$
4	2 3	sylib	$⊢ D \in ∞Met (X) \to ⋃ ran ball (D) \subseteq X$
5		1rp	$⊢ 1 \in ℝ^{+}$
6		blcntr	$⊢ (D \in ∞Met (X) \land x \in X \land 1 \in ℝ^{+}) \to x \in (x ball (D) 1)$
7	5 6	mp3an3	$⊢ (D \in ∞Met (X) \land x \in X) \to x \in (x ball (D) 1)$
8		1xr	$⊢ 1 \in ℝ^{*}$
9		blelrn	$⊢ (D \in ∞Met (X) \land x \in X \land 1 \in ℝ^{*}) \to x ball (D) 1 \in ran ball (D)$
10	8 9	mp3an3	$⊢ (D \in ∞Met (X) \land x \in X) \to x ball (D) 1 \in ran ball (D)$
11		elunii	$⊢ (x \in (x ball (D) 1) \land x ball (D) 1 \in ran ball (D)) \to x \in ⋃ ran ball (D)$
12	7 10 11	syl2anc	$⊢ (D \in ∞Met (X) \land x \in X) \to x \in ⋃ ran ball (D)$
13	4 12	eqelssd	$⊢ D \in ∞Met (X) \to ⋃ ran ball (D) = X$