# Metamath Proof Explorer

## Theorem xmeterval

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

Ref Expression
Hypothesis xmeter.1
Assertion xmeterval

### Proof

Step Hyp Ref Expression
1 xmeter.1
2 xmetf ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to {D}:{X}×{X}⟶{ℝ}^{*}$
3 ffn ${⊢}{D}:{X}×{X}⟶{ℝ}^{*}\to {D}Fn\left({X}×{X}\right)$
4 elpreima ${⊢}{D}Fn\left({X}×{X}\right)\to \left(⟨{A},{B}⟩\in {{D}}^{-1}\left[ℝ\right]↔\left(⟨{A},{B}⟩\in \left({X}×{X}\right)\wedge {D}\left(⟨{A},{B}⟩\right)\in ℝ\right)\right)$
5 2 3 4 3syl ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to \left(⟨{A},{B}⟩\in {{D}}^{-1}\left[ℝ\right]↔\left(⟨{A},{B}⟩\in \left({X}×{X}\right)\wedge {D}\left(⟨{A},{B}⟩\right)\in ℝ\right)\right)$
6 1 breqi
7 df-br ${⊢}{A}{{D}}^{-1}\left[ℝ\right]{B}↔⟨{A},{B}⟩\in {{D}}^{-1}\left[ℝ\right]$
8 6 7 bitri
9 df-3an ${⊢}\left({A}\in {X}\wedge {B}\in {X}\wedge {A}{D}{B}\in ℝ\right)↔\left(\left({A}\in {X}\wedge {B}\in {X}\right)\wedge {A}{D}{B}\in ℝ\right)$
10 opelxp ${⊢}⟨{A},{B}⟩\in \left({X}×{X}\right)↔\left({A}\in {X}\wedge {B}\in {X}\right)$
11 10 bicomi ${⊢}\left({A}\in {X}\wedge {B}\in {X}\right)↔⟨{A},{B}⟩\in \left({X}×{X}\right)$
12 df-ov ${⊢}{A}{D}{B}={D}\left(⟨{A},{B}⟩\right)$
13 12 eleq1i ${⊢}{A}{D}{B}\in ℝ↔{D}\left(⟨{A},{B}⟩\right)\in ℝ$
14 11 13 anbi12i ${⊢}\left(\left({A}\in {X}\wedge {B}\in {X}\right)\wedge {A}{D}{B}\in ℝ\right)↔\left(⟨{A},{B}⟩\in \left({X}×{X}\right)\wedge {D}\left(⟨{A},{B}⟩\right)\in ℝ\right)$
15 9 14 bitri ${⊢}\left({A}\in {X}\wedge {B}\in {X}\wedge {A}{D}{B}\in ℝ\right)↔\left(⟨{A},{B}⟩\in \left({X}×{X}\right)\wedge {D}\left(⟨{A},{B}⟩\right)\in ℝ\right)$
16 5 8 15 3bitr4g