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 ‘ 𝐷 ) +∞ ) = 𝑋 )