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