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 " RR )
Assertion xmeter
|- ( D e. ( *Met ` X ) -> .~ Er X )

Proof

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