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 ˙ = D -1
Assertion xmeter D ∞Met X ˙ Er X

Proof

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