# Metamath Proof Explorer

## Theorem xmeter

Description: The "finitely separated" relation is an equivalence relation. (Contributed by Mario Carneiro, 24-Aug-2015)

Ref Expression
Hypothesis xmeter.1
Assertion xmeter

### Proof

Step Hyp Ref Expression
1 xmeter.1
2 cnvimass ${⊢}{{D}}^{-1}\left[ℝ\right]\subseteq \mathrm{dom}{D}$
3 1 2 eqsstri
4 xmetf ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to {D}:{X}×{X}⟶{ℝ}^{*}$
5 3 4 fssdm
6 relxp ${⊢}\mathrm{Rel}\left({X}×{X}\right)$
7 relss
8 5 6 7 mpisyl
9 1 xmeterval
10 9 biimpa
11 10 simp2d
12 10 simp1d
13 simpl
14 xmetsym ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {x}\in {X}\wedge {y}\in {X}\right)\to {x}{D}{y}={y}{D}{x}$
15 13 12 11 14 syl3anc
16 10 simp3d
17 15 16 eqeltrrd
18 1 xmeterval
20 11 12 17 19 mpbir3and
22 1 xmeterval
23 22 biimpa
25 24 simp2d
26 simpl
28 24 simp3d
29 rexadd ${⊢}\left({x}{D}{y}\in ℝ\wedge {y}{D}{z}\in ℝ\right)\to \left({x}{D}{y}\right){+}_{𝑒}\left({y}{D}{z}\right)=\left({x}{D}{y}\right)+\left({y}{D}{z}\right)$
30 readdcl ${⊢}\left({x}{D}{y}\in ℝ\wedge {y}{D}{z}\in ℝ\right)\to \left({x}{D}{y}\right)+\left({y}{D}{z}\right)\in ℝ$
31 29 30 eqeltrd ${⊢}\left({x}{D}{y}\in ℝ\wedge {y}{D}{z}\in ℝ\right)\to \left({x}{D}{y}\right){+}_{𝑒}\left({y}{D}{z}\right)\in ℝ$
32 27 28 31 syl2anc
34 xmettri ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge \left({x}\in {X}\wedge {z}\in {X}\wedge {y}\in {X}\right)\right)\to {x}{D}{z}\le \left({x}{D}{y}\right){+}_{𝑒}\left({y}{D}{z}\right)$
35 26 21 25 33 34 syl13anc
36 xmetlecl ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge \left({x}\in {X}\wedge {z}\in {X}\right)\wedge \left(\left({x}{D}{y}\right){+}_{𝑒}\left({y}{D}{z}\right)\in ℝ\wedge {x}{D}{z}\le \left({x}{D}{y}\right){+}_{𝑒}\left({y}{D}{z}\right)\right)\right)\to {x}{D}{z}\in ℝ$
37 26 21 25 32 35 36 syl122anc
38 1 xmeterval
40 21 25 37 39 mpbir3and
41 xmet0 ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {x}\in {X}\right)\to {x}{D}{x}=0$
42 0re ${⊢}0\in ℝ$
43 41 42 eqeltrdi ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {x}\in {X}\right)\to {x}{D}{x}\in ℝ$
44 43 ex ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to \left({x}\in {X}\to {x}{D}{x}\in ℝ\right)$
45 44 pm4.71rd ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to \left({x}\in {X}↔\left({x}{D}{x}\in ℝ\wedge {x}\in {X}\right)\right)$
46 df-3an ${⊢}\left({x}\in {X}\wedge {x}\in {X}\wedge {x}{D}{x}\in ℝ\right)↔\left(\left({x}\in {X}\wedge {x}\in {X}\right)\wedge {x}{D}{x}\in ℝ\right)$
47 anidm ${⊢}\left({x}\in {X}\wedge {x}\in {X}\right)↔{x}\in {X}$
48 47 anbi2ci ${⊢}\left(\left({x}\in {X}\wedge {x}\in {X}\right)\wedge {x}{D}{x}\in ℝ\right)↔\left({x}{D}{x}\in ℝ\wedge {x}\in {X}\right)$
49 46 48 bitri ${⊢}\left({x}\in {X}\wedge {x}\in {X}\wedge {x}{D}{x}\in ℝ\right)↔\left({x}{D}{x}\in ℝ\wedge {x}\in {X}\right)$
50 45 49 syl6bbr ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to \left({x}\in {X}↔\left({x}\in {X}\wedge {x}\in {X}\wedge {x}{D}{x}\in ℝ\right)\right)$
51 1 xmeterval
52 50 51 bitr4d
53 8 20 40 52 iserd