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 ⊢ ∼ ˙ = D -1 ℝ
Assertion xmetec ⊢ D ∈ ∞Met ⁡ X ∧ P ∈ X → P ∼ ˙ = P ball ⁡ D +∞

Proof

Step Hyp Ref Expression
1 xmeter.1 ⊢ ∼ ˙ = D -1 ℝ
2 1 xmeterval ⊢ D ∈ ∞Met ⁡ X → P ∼ ˙ x ↔ P ∈ X ∧ x ∈ X ∧ P D x ∈ ℝ
3 3anass ⊢ P ∈ X ∧ x ∈ X ∧ P D x ∈ ℝ ↔ P ∈ X ∧ x ∈ X ∧ P D x ∈ ℝ
4 3 baib ⊢ P ∈ X → P ∈ X ∧ x ∈ X ∧ P D x ∈ ℝ ↔ x ∈ X ∧ P D x ∈ ℝ
5 2 4 sylan9bb ⊢ D ∈ ∞Met ⁡ X ∧ P ∈ X → P ∼ ˙ x ↔ x ∈ X ∧ P D x ∈ ℝ
6 vex ⊢ x ∈ V
7 6 a1i ⊢ D ∈ ∞Met ⁡ X → x ∈ V
8 elecg ⊢ x ∈ V ∧ P ∈ X → x ∈ P ∼ ˙ ↔ P ∼ ˙ x
9 7 8 sylan ⊢ D ∈ ∞Met ⁡ X ∧ P ∈ X → x ∈ P ∼ ˙ ↔ P ∼ ˙ x
10 xblpnf ⊢ D ∈ ∞Met ⁡ X ∧ P ∈ X → x ∈ P ball ⁡ D +∞ ↔ x ∈ X ∧ P D x ∈ ℝ
11 5 9 10 3bitr4d ⊢ D ∈ ∞Met ⁡ X ∧ P ∈ X → x ∈ P ∼ ˙ ↔ x ∈ P ball ⁡ D +∞
12 11 eqrdv ⊢ D ∈ ∞Met ⁡ X ∧ P ∈ X → P ∼ ˙ = P ball ⁡ D +∞