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

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 ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ∼ Er 𝑋 )

Proof

Step Hyp Ref Expression
1 xmeter.1 ⊢ ∼ = ( ◡ 𝐷 “ ℝ )
2 cnvimass ⊢ ( ◡ 𝐷 “ ℝ ) ⊆ dom 𝐷
3 1 2 eqsstri ⊢ ∼ ⊆ dom 𝐷
4 xmetf ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* )
5 3 4 fssdm ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ∼ ⊆ ( 𝑋 × 𝑋 ) )
6 relxp ⊢ Rel ( 𝑋 × 𝑋 )
7 relss ⊢ ( ∼ ⊆ ( 𝑋 × 𝑋 ) → ( Rel ( 𝑋 × 𝑋 ) → Rel ∼ ) )
8 5 6 7 mpisyl ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → Rel ∼ )
9 1 xmeterval ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑥 ∼ 𝑦 ↔ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ ( 𝑥 𝐷 𝑦 ) ∈ ℝ ) ) )
10 9 biimpa ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∼ 𝑦 ) → ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ ( 𝑥 𝐷 𝑦 ) ∈ ℝ ) )
11 10 simp2d ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∼ 𝑦 ) → 𝑦 ∈ 𝑋 )
12 10 simp1d ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∼ 𝑦 ) → 𝑥 ∈ 𝑋 )
13 simpl ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∼ 𝑦 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
14 xmetsym ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 𝐷 𝑦 ) = ( 𝑦 𝐷 𝑥 ) )
15 13 12 11 14 syl3anc ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∼ 𝑦 ) → ( 𝑥 𝐷 𝑦 ) = ( 𝑦 𝐷 𝑥 ) )
16 10 simp3d ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∼ 𝑦 ) → ( 𝑥 𝐷 𝑦 ) ∈ ℝ )
17 15 16 eqeltrrd ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∼ 𝑦 ) → ( 𝑦 𝐷 𝑥 ) ∈ ℝ )
18 1 xmeterval ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑦 ∼ 𝑥 ↔ ( 𝑦 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ ( 𝑦 𝐷 𝑥 ) ∈ ℝ ) ) )
19 18 adantr ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∼ 𝑦 ) → ( 𝑦 ∼ 𝑥 ↔ ( 𝑦 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ ( 𝑦 𝐷 𝑥 ) ∈ ℝ ) ) )
20 11 12 17 19 mpbir3and ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∼ 𝑦 ) → 𝑦 ∼ 𝑥 )
21 12 adantrr ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧 ) ) → 𝑥 ∈ 𝑋 )
22 1 xmeterval ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑦 ∼ 𝑧 ↔ ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ ( 𝑦 𝐷 𝑧 ) ∈ ℝ ) ) )
23 22 biimpa ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑦 ∼ 𝑧 ) → ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ ( 𝑦 𝐷 𝑧 ) ∈ ℝ ) )
24 23 adantrl ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧 ) ) → ( 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ ( 𝑦 𝐷 𝑧 ) ∈ ℝ ) )
25 24 simp2d ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧 ) ) → 𝑧 ∈ 𝑋 )
26 simpl ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧 ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
27 16 adantrr ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧 ) ) → ( 𝑥 𝐷 𝑦 ) ∈ ℝ )
28 24 simp3d ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧 ) ) → ( 𝑦 𝐷 𝑧 ) ∈ ℝ )
29 rexadd ⊢ ( ( ( 𝑥 𝐷 𝑦 ) ∈ ℝ ∧ ( 𝑦 𝐷 𝑧 ) ∈ ℝ ) → ( ( 𝑥 𝐷 𝑦 ) +𝑒 ( 𝑦 𝐷 𝑧 ) ) = ( ( 𝑥 𝐷 𝑦 ) + ( 𝑦 𝐷 𝑧 ) ) )
30 readdcl ⊢ ( ( ( 𝑥 𝐷 𝑦 ) ∈ ℝ ∧ ( 𝑦 𝐷 𝑧 ) ∈ ℝ ) → ( ( 𝑥 𝐷 𝑦 ) + ( 𝑦 𝐷 𝑧 ) ) ∈ ℝ )
31 29 30 eqeltrd ⊢ ( ( ( 𝑥 𝐷 𝑦 ) ∈ ℝ ∧ ( 𝑦 𝐷 𝑧 ) ∈ ℝ ) → ( ( 𝑥 𝐷 𝑦 ) +𝑒 ( 𝑦 𝐷 𝑧 ) ) ∈ ℝ )
32 27 28 31 syl2anc ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧 ) ) → ( ( 𝑥 𝐷 𝑦 ) +𝑒 ( 𝑦 𝐷 𝑧 ) ) ∈ ℝ )
33 11 adantrr ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧 ) ) → 𝑦 ∈ 𝑋 )
34 xmettri ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝐷 𝑧 ) ≤ ( ( 𝑥 𝐷 𝑦 ) +𝑒 ( 𝑦 𝐷 𝑧 ) ) )
35 26 21 25 33 34 syl13anc ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧 ) ) → ( 𝑥 𝐷 𝑧 ) ≤ ( ( 𝑥 𝐷 𝑦 ) +𝑒 ( 𝑦 𝐷 𝑧 ) ) )
36 xmetlecl ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ∧ ( ( ( 𝑥 𝐷 𝑦 ) +𝑒 ( 𝑦 𝐷 𝑧 ) ) ∈ ℝ ∧ ( 𝑥 𝐷 𝑧 ) ≤ ( ( 𝑥 𝐷 𝑦 ) +𝑒 ( 𝑦 𝐷 𝑧 ) ) ) ) → ( 𝑥 𝐷 𝑧 ) ∈ ℝ )
37 26 21 25 32 35 36 syl122anc ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧 ) ) → ( 𝑥 𝐷 𝑧 ) ∈ ℝ )
38 1 xmeterval ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑥 ∼ 𝑧 ↔ ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ ( 𝑥 𝐷 𝑧 ) ∈ ℝ ) ) )
39 38 adantr ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧 ) ) → ( 𝑥 ∼ 𝑧 ↔ ( 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ ( 𝑥 𝐷 𝑧 ) ∈ ℝ ) ) )
40 21 25 37 39 mpbir3and ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧 ) ) → 𝑥 ∼ 𝑧 )
41 xmet0 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 𝐷 𝑥 ) = 0 )
42 0re ⊢ 0 ∈ ℝ
43 41 42 eqeltrdi ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 𝐷 𝑥 ) ∈ ℝ )
44 43 ex ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑥 ∈ 𝑋 → ( 𝑥 𝐷 𝑥 ) ∈ ℝ ) )
45 44 pm4.71rd ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑥 ∈ 𝑋 ↔ ( ( 𝑥 𝐷 𝑥 ) ∈ ℝ ∧ 𝑥 ∈ 𝑋 ) ) )
46 df-3an ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ ( 𝑥 𝐷 𝑥 ) ∈ ℝ ) ↔ ( ( 𝑥 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑥 𝐷 𝑥 ) ∈ ℝ ) )
47 anidm ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ↔ 𝑥 ∈ 𝑋 )
48 47 anbi2ci ⊢ ( ( ( 𝑥 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑥 𝐷 𝑥 ) ∈ ℝ ) ↔ ( ( 𝑥 𝐷 𝑥 ) ∈ ℝ ∧ 𝑥 ∈ 𝑋 ) )
49 46 48 bitri ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ ( 𝑥 𝐷 𝑥 ) ∈ ℝ ) ↔ ( ( 𝑥 𝐷 𝑥 ) ∈ ℝ ∧ 𝑥 ∈ 𝑋 ) )
50 45 49 bitr4di ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑥 ∈ 𝑋 ↔ ( 𝑥 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ ( 𝑥 𝐷 𝑥 ) ∈ ℝ ) ) )
51 1 xmeterval ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑥 ∼ 𝑥 ↔ ( 𝑥 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ ( 𝑥 𝐷 𝑥 ) ∈ ℝ ) ) )
52 50 51 bitr4d ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑥 ∈ 𝑋 ↔ 𝑥 ∼ 𝑥 ) )
53 8 20 40 52 iserd ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ∼ Er 𝑋 )