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 𝑋 )