Theorem xblpnfps

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) (Revised by Thierry Arnoux, 11-Mar-2018)

	Ref	Expression
Assertion	xblpnfps	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝐴 ∈ ( 𝑃 ( ball ‘ 𝐷 ) +∞ ) ↔ ( 𝐴 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝐴 ) ∈ ℝ ) ) )

Proof

Step	Hyp	Ref	Expression
1		pnfxr	⊢ +∞ ∈ ℝ*
2		elblps	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ +∞ ∈ ℝ* ) → ( 𝐴 ∈ ( 𝑃 ( ball ‘ 𝐷 ) +∞ ) ↔ ( 𝐴 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝐴 ) < +∞ ) ) )
3	1 2	mp3an3	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝐴 ∈ ( 𝑃 ( ball ‘ 𝐷 ) +∞ ) ↔ ( 𝐴 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝐴 ) < +∞ ) ) )
4		psmetcl	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝑃 𝐷 𝐴 ) ∈ ℝ* )
5		psmetge0	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → 0 ≤ ( 𝑃 𝐷 𝐴 ) )
6		ge0nemnf	⊢ ( ( ( 𝑃 𝐷 𝐴 ) ∈ ℝ* ∧ 0 ≤ ( 𝑃 𝐷 𝐴 ) ) → ( 𝑃 𝐷 𝐴 ) ≠ -∞ )
7	4 5 6	syl2anc	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝑃 𝐷 𝐴 ) ≠ -∞ )
8		ngtmnft	⊢ ( ( 𝑃 𝐷 𝐴 ) ∈ ℝ* → ( ( 𝑃 𝐷 𝐴 ) = -∞ ↔ ¬ -∞ < ( 𝑃 𝐷 𝐴 ) ) )
9	4 8	syl	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑃 𝐷 𝐴 ) = -∞ ↔ ¬ -∞ < ( 𝑃 𝐷 𝐴 ) ) )
10	9	necon2abid	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( -∞ < ( 𝑃 𝐷 𝐴 ) ↔ ( 𝑃 𝐷 𝐴 ) ≠ -∞ ) )
11	7 10	mpbird	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → -∞ < ( 𝑃 𝐷 𝐴 ) )
12	11	biantrurd	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑃 𝐷 𝐴 ) < +∞ ↔ ( -∞ < ( 𝑃 𝐷 𝐴 ) ∧ ( 𝑃 𝐷 𝐴 ) < +∞ ) ) )
13		xrrebnd	⊢ ( ( 𝑃 𝐷 𝐴 ) ∈ ℝ* → ( ( 𝑃 𝐷 𝐴 ) ∈ ℝ ↔ ( -∞ < ( 𝑃 𝐷 𝐴 ) ∧ ( 𝑃 𝐷 𝐴 ) < +∞ ) ) )
14	4 13	syl	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑃 𝐷 𝐴 ) ∈ ℝ ↔ ( -∞ < ( 𝑃 𝐷 𝐴 ) ∧ ( 𝑃 𝐷 𝐴 ) < +∞ ) ) )
15	12 14	bitr4d	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑃 𝐷 𝐴 ) < +∞ ↔ ( 𝑃 𝐷 𝐴 ) ∈ ℝ ) )
16	15	3expa	⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑃 𝐷 𝐴 ) < +∞ ↔ ( 𝑃 𝐷 𝐴 ) ∈ ℝ ) )
17	16	pm5.32da	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → ( ( 𝐴 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝐴 ) < +∞ ) ↔ ( 𝐴 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝐴 ) ∈ ℝ ) ) )
18	3 17	bitrd	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝐴 ∈ ( 𝑃 ( ball ‘ 𝐷 ) +∞ ) ↔ ( 𝐴 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝐴 ) ∈ ℝ ) ) )