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 )