This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 metxmet ⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
2 xblpnf ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) +∞ ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) ∈ ℝ ) ) )
3 1 2 sylan ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) +∞ ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) ∈ ℝ ) ) )
4 metcl ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑃 𝐷 𝑥 ) ∈ ℝ )
5 4 3expia ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝑥 ∈ 𝑋 → ( 𝑃 𝐷 𝑥 ) ∈ ℝ ) )
6 5 pm4.71d ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝑥 ∈ 𝑋 ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) ∈ ℝ ) ) )
7 3 6 bitr4d ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) +∞ ) ↔ 𝑥 ∈ 𝑋 ) )
8 7 eqrdv ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝑃 ( ball ‘ 𝐷 ) +∞ ) = 𝑋 )