Metamath Proof Explorer

Theorem xblpnf

Description: The infinity ball in an extended metric is the set of all points that are a finite distance from the center. (Contributed by Mario Carneiro, 23-Aug-2015)

		Ref	Expression
	Assertion	xblpnf	$⊢ (D \in ∞Met (X) \land P \in X) \to (A \in (P ball (D) +∞) \leftrightarrow (A \in X \land P D A \in ℝ))$

Proof

Step	Hyp	Ref	Expression
1		pnfxr	$⊢ +∞ \in ℝ^{*}$
2		elbl	$⊢ (D \in ∞Met (X) \land P \in X \land +∞ \in ℝ^{*}) \to (A \in (P ball (D) +∞) \leftrightarrow (A \in X \land P D A < +∞))$
3	1 2	mp3an3	$⊢ (D \in ∞Met (X) \land P \in X) \to (A \in (P ball (D) +∞) \leftrightarrow (A \in X \land P D A < +∞))$
4		xmetcl	$⊢ (D \in ∞Met (X) \land P \in X \land A \in X) \to P D A \in ℝ^{*}$
5		xmetge0	$⊢ (D \in ∞Met (X) \land P \in X \land A \in X) \to 0 \leq P D A$
6		ge0nemnf	$⊢ (P D A \in ℝ^{*} \land 0 \leq P D A) \to P D A \neq −∞$
7	4 5 6	syl2anc	$⊢ (D \in ∞Met (X) \land P \in X \land A \in X) \to P D A \neq −∞$
8		ngtmnft	$⊢ P D A \in ℝ^{*} \to (P D A = −∞ \leftrightarrow \neg −∞ < P D A)$
9	4 8	syl	$⊢ (D \in ∞Met (X) \land P \in X \land A \in X) \to (P D A = −∞ \leftrightarrow \neg −∞ < P D A)$
10	9	necon2abid	$⊢ (D \in ∞Met (X) \land P \in X \land A \in X) \to (−∞ < P D A \leftrightarrow P D A \neq −∞)$
11	7 10	mpbird	$⊢ (D \in ∞Met (X) \land P \in X \land A \in X) \to −∞ < P D A$
12	11	biantrurd	$⊢ (D \in ∞Met (X) \land P \in X \land A \in X) \to (P D A < +∞ \leftrightarrow (−∞ < P D A \land P D A < +∞))$
13		xrrebnd	$⊢ P D A \in ℝ^{*} \to (P D A \in ℝ \leftrightarrow (−∞ < P D A \land P D A < +∞))$
14	4 13	syl	$⊢ (D \in ∞Met (X) \land P \in X \land A \in X) \to (P D A \in ℝ \leftrightarrow (−∞ < P D A \land P D A < +∞))$
15	12 14	bitr4d	$⊢ (D \in ∞Met (X) \land P \in X \land A \in X) \to (P D A < +∞ \leftrightarrow P D A \in ℝ)$
16	15	3expa	$⊢ ((D \in ∞Met (X) \land P \in X) \land A \in X) \to (P D A < +∞ \leftrightarrow P D A \in ℝ)$
17	16	pm5.32da	$⊢ (D \in ∞Met (X) \land P \in X) \to ((A \in X \land P D A < +∞) \leftrightarrow (A \in X \land P D A \in ℝ))$
18	3 17	bitrd	$⊢ (D \in ∞Met (X) \land P \in X) \to (A \in (P ball (D) +∞) \leftrightarrow (A \in X \land P D A \in ℝ))$