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 β€˜ 𝐷 ) +∞ ) ↔ ( 𝐴 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝐴 ) ∈ ℝ ) ) )