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

Metamath Proof Explorer

Theorem xmeterval

Description: Value of the "finitely separated" relation. (Contributed by Mario Carneiro, 24-Aug-2015)

Ref Expression
Hypothesis xmeter.1 ⊢ ∼ ˙ = D -1 ℝ
Assertion xmeterval ⊢ D ∈ ∞Met ⁡ X → A ∼ ˙ B ↔ A ∈ X ∧ B ∈ X ∧ A D B ∈ ℝ

Proof

Step Hyp Ref Expression
1 xmeter.1 ⊢ ∼ ˙ = D -1 ℝ
2 xmetf ⊢ D ∈ ∞Met ⁡ X → D : X × X ⟶ ℝ *
3 ffn ⊢ D : X × X ⟶ ℝ * → D Fn X × X
4 elpreima ⊢ D Fn X × X → A B ∈ D -1 ℝ ↔ A B ∈ X × X ∧ D ⁡ A B ∈ ℝ
5 2 3 4 3syl ⊢ D ∈ ∞Met ⁡ X → A B ∈ D -1 ℝ ↔ A B ∈ X × X ∧ D ⁡ A B ∈ ℝ
6 1 breqi ⊢ A ∼ ˙ B ↔ A D -1 ℝ B
7 df-br ⊢ A D -1 ℝ B ↔ A B ∈ D -1 ℝ
8 6 7 bitri ⊢ A ∼ ˙ B ↔ A B ∈ D -1 ℝ
9 df-3an ⊢ A ∈ X ∧ B ∈ X ∧ A D B ∈ ℝ ↔ A ∈ X ∧ B ∈ X ∧ A D B ∈ ℝ
10 opelxp ⊢ A B ∈ X × X ↔ A ∈ X ∧ B ∈ X
11 10 bicomi ⊢ A ∈ X ∧ B ∈ X ↔ A B ∈ X × X
12 df-ov ⊢ A D B = D ⁡ A B
13 12 eleq1i ⊢ A D B ∈ ℝ ↔ D ⁡ A B ∈ ℝ
14 11 13 anbi12i ⊢ A ∈ X ∧ B ∈ X ∧ A D B ∈ ℝ ↔ A B ∈ X × X ∧ D ⁡ A B ∈ ℝ
15 9 14 bitri ⊢ A ∈ X ∧ B ∈ X ∧ A D B ∈ ℝ ↔ A B ∈ X × X ∧ D ⁡ A B ∈ ℝ
16 5 8 15 3bitr4g ⊢ D ∈ ∞Met ⁡ X → A ∼ ˙ B ↔ A ∈ X ∧ B ∈ X ∧ A D B ∈ ℝ