Metamath Proof Explorer

Theorem metustto

Description: Any two elements of the filter base generated by the metric D can be compared, like for RR+ (i.e. it's totally ordered). (Contributed by Thierry Arnoux, 22-Nov-2017) (Revised by Thierry Arnoux, 11-Feb-2018)

Ref Expression
Hypothesis metust.1 
|- F = ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )
Assertion metustto 
|- ( ( D e. ( PsMet ` X ) /\ A e. F /\ B e. F ) -> ( A C_ B \/ B C_ A ) )

Proof

Step Hyp Ref Expression
1 metust.1 
 |-  F = ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )
2 simpll 
 |-  ( ( ( a e. RR+ /\ b e. RR+ ) /\ ( A = ( `' D " ( 0 [,) a ) ) /\ B = ( `' D " ( 0 [,) b ) ) ) ) -> a e. RR+ )
3 2 rpred 
 |-  ( ( ( a e. RR+ /\ b e. RR+ ) /\ ( A = ( `' D " ( 0 [,) a ) ) /\ B = ( `' D " ( 0 [,) b ) ) ) ) -> a e. RR )
4 simplr 
 |-  ( ( ( a e. RR+ /\ b e. RR+ ) /\ ( A = ( `' D " ( 0 [,) a ) ) /\ B = ( `' D " ( 0 [,) b ) ) ) ) -> b e. RR+ )
5 4 rpred 
 |-  ( ( ( a e. RR+ /\ b e. RR+ ) /\ ( A = ( `' D " ( 0 [,) a ) ) /\ B = ( `' D " ( 0 [,) b ) ) ) ) -> b e. RR )
6 simpllr 
 |-  ( ( ( ( a e. RR+ /\ b e. RR+ ) /\ ( A = ( `' D " ( 0 [,) a ) ) /\ B = ( `' D " ( 0 [,) b ) ) ) ) /\ a <_ b ) -> b e. RR+ )
7 6 rpred 
 |-  ( ( ( ( a e. RR+ /\ b e. RR+ ) /\ ( A = ( `' D " ( 0 [,) a ) ) /\ B = ( `' D " ( 0 [,) b ) ) ) ) /\ a <_ b ) -> b e. RR )
8 0xr 
 |-  0 e. RR*
9 8 a1i 
 |-  ( ( b e. RR /\ a <_ b ) -> 0 e. RR* )
10 simpl 
 |-  ( ( b e. RR /\ a <_ b ) -> b e. RR )
11 10 rexrd 
 |-  ( ( b e. RR /\ a <_ b ) -> b e. RR* )
12 0le0 
 |-  0 <_ 0
13 12 a1i 
 |-  ( ( b e. RR /\ a <_ b ) -> 0 <_ 0 )
14 simpr 
 |-  ( ( b e. RR /\ a <_ b ) -> a <_ b )
15 icossico 
 |-  ( ( ( 0 e. RR* /\ b e. RR* ) /\ ( 0 <_ 0 /\ a <_ b ) ) -> ( 0 [,) a ) C_ ( 0 [,) b ) )
16 9 11 13 14 15 syl22anc 
 |-  ( ( b e. RR /\ a <_ b ) -> ( 0 [,) a ) C_ ( 0 [,) b ) )
17 imass2 
 |-  ( ( 0 [,) a ) C_ ( 0 [,) b ) -> ( `' D " ( 0 [,) a ) ) C_ ( `' D " ( 0 [,) b ) ) )
18 16 17 syl 
 |-  ( ( b e. RR /\ a <_ b ) -> ( `' D " ( 0 [,) a ) ) C_ ( `' D " ( 0 [,) b ) ) )
19 7 18 sylancom 
 |-  ( ( ( ( a e. RR+ /\ b e. RR+ ) /\ ( A = ( `' D " ( 0 [,) a ) ) /\ B = ( `' D " ( 0 [,) b ) ) ) ) /\ a <_ b ) -> ( `' D " ( 0 [,) a ) ) C_ ( `' D " ( 0 [,) b ) ) )
20 simplrl 
 |-  ( ( ( ( a e. RR+ /\ b e. RR+ ) /\ ( A = ( `' D " ( 0 [,) a ) ) /\ B = ( `' D " ( 0 [,) b ) ) ) ) /\ a <_ b ) -> A = ( `' D " ( 0 [,) a ) ) )
21 simplrr 
 |-  ( ( ( ( a e. RR+ /\ b e. RR+ ) /\ ( A = ( `' D " ( 0 [,) a ) ) /\ B = ( `' D " ( 0 [,) b ) ) ) ) /\ a <_ b ) -> B = ( `' D " ( 0 [,) b ) ) )
22 19 20 21 3sstr4d 
 |-  ( ( ( ( a e. RR+ /\ b e. RR+ ) /\ ( A = ( `' D " ( 0 [,) a ) ) /\ B = ( `' D " ( 0 [,) b ) ) ) ) /\ a <_ b ) -> A C_ B )
23 22 orcd 
 |-  ( ( ( ( a e. RR+ /\ b e. RR+ ) /\ ( A = ( `' D " ( 0 [,) a ) ) /\ B = ( `' D " ( 0 [,) b ) ) ) ) /\ a <_ b ) -> ( A C_ B \/ B C_ A ) )
24 simplll 
 |-  ( ( ( ( a e. RR+ /\ b e. RR+ ) /\ ( A = ( `' D " ( 0 [,) a ) ) /\ B = ( `' D " ( 0 [,) b ) ) ) ) /\ b <_ a ) -> a e. RR+ )
25 24 rpred 
 |-  ( ( ( ( a e. RR+ /\ b e. RR+ ) /\ ( A = ( `' D " ( 0 [,) a ) ) /\ B = ( `' D " ( 0 [,) b ) ) ) ) /\ b <_ a ) -> a e. RR )
26 8 a1i 
 |-  ( ( a e. RR /\ b <_ a ) -> 0 e. RR* )
27 simpl 
 |-  ( ( a e. RR /\ b <_ a ) -> a e. RR )
28 27 rexrd 
 |-  ( ( a e. RR /\ b <_ a ) -> a e. RR* )
29 12 a1i 
 |-  ( ( a e. RR /\ b <_ a ) -> 0 <_ 0 )
30 simpr 
 |-  ( ( a e. RR /\ b <_ a ) -> b <_ a )
31 icossico 
 |-  ( ( ( 0 e. RR* /\ a e. RR* ) /\ ( 0 <_ 0 /\ b <_ a ) ) -> ( 0 [,) b ) C_ ( 0 [,) a ) )
32 26 28 29 30 31 syl22anc 
 |-  ( ( a e. RR /\ b <_ a ) -> ( 0 [,) b ) C_ ( 0 [,) a ) )
33 imass2 
 |-  ( ( 0 [,) b ) C_ ( 0 [,) a ) -> ( `' D " ( 0 [,) b ) ) C_ ( `' D " ( 0 [,) a ) ) )
34 32 33 syl 
 |-  ( ( a e. RR /\ b <_ a ) -> ( `' D " ( 0 [,) b ) ) C_ ( `' D " ( 0 [,) a ) ) )
35 25 34 sylancom 
 |-  ( ( ( ( a e. RR+ /\ b e. RR+ ) /\ ( A = ( `' D " ( 0 [,) a ) ) /\ B = ( `' D " ( 0 [,) b ) ) ) ) /\ b <_ a ) -> ( `' D " ( 0 [,) b ) ) C_ ( `' D " ( 0 [,) a ) ) )
36 simplrr 
 |-  ( ( ( ( a e. RR+ /\ b e. RR+ ) /\ ( A = ( `' D " ( 0 [,) a ) ) /\ B = ( `' D " ( 0 [,) b ) ) ) ) /\ b <_ a ) -> B = ( `' D " ( 0 [,) b ) ) )
37 simplrl 
 |-  ( ( ( ( a e. RR+ /\ b e. RR+ ) /\ ( A = ( `' D " ( 0 [,) a ) ) /\ B = ( `' D " ( 0 [,) b ) ) ) ) /\ b <_ a ) -> A = ( `' D " ( 0 [,) a ) ) )
38 35 36 37 3sstr4d 
 |-  ( ( ( ( a e. RR+ /\ b e. RR+ ) /\ ( A = ( `' D " ( 0 [,) a ) ) /\ B = ( `' D " ( 0 [,) b ) ) ) ) /\ b <_ a ) -> B C_ A )
39 38 olcd 
 |-  ( ( ( ( a e. RR+ /\ b e. RR+ ) /\ ( A = ( `' D " ( 0 [,) a ) ) /\ B = ( `' D " ( 0 [,) b ) ) ) ) /\ b <_ a ) -> ( A C_ B \/ B C_ A ) )
40 3 5 23 39 lecasei 
 |-  ( ( ( a e. RR+ /\ b e. RR+ ) /\ ( A = ( `' D " ( 0 [,) a ) ) /\ B = ( `' D " ( 0 [,) b ) ) ) ) -> ( A C_ B \/ B C_ A ) )
41 40 adantlll 
 |-  ( ( ( ( ( D e. ( PsMet ` X ) /\ A e. F /\ B e. F ) /\ a e. RR+ ) /\ b e. RR+ ) /\ ( A = ( `' D " ( 0 [,) a ) ) /\ B = ( `' D " ( 0 [,) b ) ) ) ) -> ( A C_ B \/ B C_ A ) )
42 1 metustel 
 |-  ( D e. ( PsMet ` X ) -> ( A e. F <-> E. a e. RR+ A = ( `' D " ( 0 [,) a ) ) ) )
43 42 biimpa 
 |-  ( ( D e. ( PsMet ` X ) /\ A e. F ) -> E. a e. RR+ A = ( `' D " ( 0 [,) a ) ) )
44 43 3adant3 
 |-  ( ( D e. ( PsMet ` X ) /\ A e. F /\ B e. F ) -> E. a e. RR+ A = ( `' D " ( 0 [,) a ) ) )
45 oveq2 
 |-  ( a = b -> ( 0 [,) a ) = ( 0 [,) b ) )
46 45 imaeq2d 
 |-  ( a = b -> ( `' D " ( 0 [,) a ) ) = ( `' D " ( 0 [,) b ) ) )
47 46 cbvmptv 
 |-  ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) = ( b e. RR+ |-> ( `' D " ( 0 [,) b ) ) )
48 47 rneqi 
 |-  ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) = ran ( b e. RR+ |-> ( `' D " ( 0 [,) b ) ) )
49 1 48 eqtri 
 |-  F = ran ( b e. RR+ |-> ( `' D " ( 0 [,) b ) ) )
50 49 metustel 
 |-  ( D e. ( PsMet ` X ) -> ( B e. F <-> E. b e. RR+ B = ( `' D " ( 0 [,) b ) ) ) )
51 50 biimpa 
 |-  ( ( D e. ( PsMet ` X ) /\ B e. F ) -> E. b e. RR+ B = ( `' D " ( 0 [,) b ) ) )
52 51 3adant2 
 |-  ( ( D e. ( PsMet ` X ) /\ A e. F /\ B e. F ) -> E. b e. RR+ B = ( `' D " ( 0 [,) b ) ) )
53 reeanv 
 |-  ( E. a e. RR+ E. b e. RR+ ( A = ( `' D " ( 0 [,) a ) ) /\ B = ( `' D " ( 0 [,) b ) ) ) <-> ( E. a e. RR+ A = ( `' D " ( 0 [,) a ) ) /\ E. b e. RR+ B = ( `' D " ( 0 [,) b ) ) ) )
54 44 52 53 sylanbrc 
 |-  ( ( D e. ( PsMet ` X ) /\ A e. F /\ B e. F ) -> E. a e. RR+ E. b e. RR+ ( A = ( `' D " ( 0 [,) a ) ) /\ B = ( `' D " ( 0 [,) b ) ) ) )
55 41 54 r19.29vva 
 |-  ( ( D e. ( PsMet ` X ) /\ A e. F /\ B e. F ) -> ( A C_ B \/ B C_ A ) )