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

Metamath Proof Explorer

Theorem xmetec

Description: The equivalence classes under the finite separation equivalence relation are infinity balls. Thus, by erdisj , infinity balls are either identical or disjoint, quite unlike the usual situation with Euclidean balls which admit many kinds of overlap. (Contributed by Mario Carneiro, 24-Aug-2015)

Ref Expression
Hypothesis xmeter.1 ⊢ ∼ = ( ◡ 𝐷 “ ℝ )
Assertion xmetec ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → [ 𝑃 ] ∼ = ( 𝑃 ( ball ‘ 𝐷 ) +∞ ) )

Proof

Step Hyp Ref Expression
1 xmeter.1 ⊢ ∼ = ( ◡ 𝐷 “ ℝ )
2 1 xmeterval ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑃 ∼ 𝑥 ↔ ( 𝑃 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) ∈ ℝ ) ) )
3 3anass ⊢ ( ( 𝑃 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) ∈ ℝ ) ↔ ( 𝑃 ∈ 𝑋 ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) ∈ ℝ ) ) )
4 3 baib ⊢ ( 𝑃 ∈ 𝑋 → ( ( 𝑃 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) ∈ ℝ ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) ∈ ℝ ) ) )
5 2 4 sylan9bb ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝑃 ∼ 𝑥 ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) ∈ ℝ ) ) )
6 vex ⊢ 𝑥 ∈ V
7 6 a1i ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑥 ∈ V )
8 elecg ⊢ ( ( 𝑥 ∈ V ∧ 𝑃 ∈ 𝑋 ) → ( 𝑥 ∈ [ 𝑃 ] ∼ ↔ 𝑃 ∼ 𝑥 ) )
9 7 8 sylan ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝑥 ∈ [ 𝑃 ] ∼ ↔ 𝑃 ∼ 𝑥 ) )
10 xblpnf ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) +∞ ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) ∈ ℝ ) ) )
11 5 9 10 3bitr4d ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝑥 ∈ [ 𝑃 ] ∼ ↔ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) +∞ ) ) )
12 11 eqrdv ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → [ 𝑃 ] ∼ = ( 𝑃 ( ball ‘ 𝐷 ) +∞ ) )