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 ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋 ) → ( 𝐴 ∈ ( 𝑃 ( ball ‘ 𝐷 ) +∞ ) ↔ ( 𝐴𝑋 ∧ ( 𝑃 𝐷 𝐴 ) ∈ ℝ ) ) )

Proof

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