blpnf

Description: The infinity ball in a standard metric is just the whole space. (Contributed by Mario Carneiro, 23-Aug-2015)

		Ref	Expression
	Assertion	blpnf	$⊢ (D \in Met (X) \land P \in X) \to P ball (D) +∞ = X$

Step	Hyp	Ref	Expression
1		metxmet	$⊢ D \in Met (X) \to D \in ∞Met (X)$
2		xblpnf	$⊢ (D \in ∞Met (X) \land P \in X) \to (x \in (P ball (D) +∞) \leftrightarrow (x \in X \land P D x \in ℝ))$
3	1 2	sylan	$⊢ (D \in Met (X) \land P \in X) \to (x \in (P ball (D) +∞) \leftrightarrow (x \in X \land P D x \in ℝ))$
4		metcl	$⊢ (D \in Met (X) \land P \in X \land x \in X) \to P D x \in ℝ$
5	4	3expia	$⊢ (D \in Met (X) \land P \in X) \to (x \in X \to P D x \in ℝ)$
6	5	pm4.71d	$⊢ (D \in Met (X) \land P \in X) \to (x \in X \leftrightarrow (x \in X \land P D x \in ℝ))$
7	3 6	bitr4d	$⊢ (D \in Met (X) \land P \in X) \to (x \in (P ball (D) +∞) \leftrightarrow x \in X)$
8	7	eqrdv	$⊢ (D \in Met (X) \land P \in X) \to P ball (D) +∞ = X$

Metamath Proof Explorer