Metamath Proof Explorer

Theorem xrsmopn

Description: The metric on the extended reals generates a topology, but this does not match the order topology on RR* ; for example { +oo } is open in the metric topology, but not the order topology. However, the metric topology is finer than the order topology, meaning that all open intervals are open in the metric topology. (Contributed by Mario Carneiro, 4-Sep-2015)

Ref Expression
Hypotheses xrsxmet.1 
|- D = ( dist ` RR*s )
xrsmopn.1 
|- J = ( MetOpen ` D )
Assertion xrsmopn 
|- ( ordTop ` <_ ) C_ J

Proof

Step Hyp Ref Expression
1 xrsxmet.1 
 |-  D = ( dist ` RR*s )
2 xrsmopn.1 
 |-  J = ( MetOpen ` D )
3 elssuni 
 |-  ( x e. ( ordTop ` <_ ) -> x C_ U. ( ordTop ` <_ ) )
4 letopuni 
 |-  RR* = U. ( ordTop ` <_ )
5 3 4 sseqtrrdi 
 |-  ( x e. ( ordTop ` <_ ) -> x C_ RR* )
6 eqid 
 |-  ( ( abs o. - ) |` ( RR X. RR ) ) = ( ( abs o. - ) |` ( RR X. RR ) )
7 6 rexmet 
 |-  ( ( abs o. - ) |` ( RR X. RR ) ) e. ( *Met ` RR )
8 letop 
 |-  ( ordTop ` <_ ) e. Top
9 reex 
 |-  RR e. _V
10 elrestr 
 |-  ( ( ( ordTop ` <_ ) e. Top /\ RR e. _V /\ x e. ( ordTop ` <_ ) ) -> ( x i^i RR ) e. ( ( ordTop ` <_ ) |`t RR ) )
11 8 9 10 mp3an12 
 |-  ( x e. ( ordTop ` <_ ) -> ( x i^i RR ) e. ( ( ordTop ` <_ ) |`t RR ) )
12 11 ad2antrr 
 |-  ( ( ( x e. ( ordTop ` <_ ) /\ y e. x ) /\ y e. RR ) -> ( x i^i RR ) e. ( ( ordTop ` <_ ) |`t RR ) )
13 elin 
 |-  ( y e. ( x i^i RR ) <-> ( y e. x /\ y e. RR ) )
14 13 biimpri 
 |-  ( ( y e. x /\ y e. RR ) -> y e. ( x i^i RR ) )
15 14 adantll 
 |-  ( ( ( x e. ( ordTop ` <_ ) /\ y e. x ) /\ y e. RR ) -> y e. ( x i^i RR ) )
16 eqid 
 |-  ( ( ordTop ` <_ ) |`t RR ) = ( ( ordTop ` <_ ) |`t RR )
17 16 xrtgioo 
 |-  ( topGen ` ran (,) ) = ( ( ordTop ` <_ ) |`t RR )
18 eqid 
 |-  ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) ) = ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) )
19 6 18 tgioo 
 |-  ( topGen ` ran (,) ) = ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) )
20 17 19 eqtr3i 
 |-  ( ( ordTop ` <_ ) |`t RR ) = ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) )
21 20 mopni2 
 |-  ( ( ( ( abs o. - ) |` ( RR X. RR ) ) e. ( *Met ` RR ) /\ ( x i^i RR ) e. ( ( ordTop ` <_ ) |`t RR ) /\ y e. ( x i^i RR ) ) -> E. r e. RR+ ( y ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ ( x i^i RR ) )
22 7 12 15 21 mp3an2i 
 |-  ( ( ( x e. ( ordTop ` <_ ) /\ y e. x ) /\ y e. RR ) -> E. r e. RR+ ( y ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ ( x i^i RR ) )
23 1 xrsxmet 
 |-  D e. ( *Met ` RR* )
24 simplr 
 |-  ( ( ( ( x e. ( ordTop ` <_ ) /\ y e. x ) /\ y e. RR ) /\ r e. RR+ ) -> y e. RR )
25 ressxr 
 |-  RR C_ RR*
26 sseqin2 
 |-  ( RR C_ RR* <-> ( RR* i^i RR ) = RR )
27 25 26 mpbi 
 |-  ( RR* i^i RR ) = RR
28 24 27 eleqtrrdi 
 |-  ( ( ( ( x e. ( ordTop ` <_ ) /\ y e. x ) /\ y e. RR ) /\ r e. RR+ ) -> y e. ( RR* i^i RR ) )
29 rpxr 
 |-  ( r e. RR+ -> r e. RR* )
30 29 adantl 
 |-  ( ( ( ( x e. ( ordTop ` <_ ) /\ y e. x ) /\ y e. RR ) /\ r e. RR+ ) -> r e. RR* )
31 1 xrsdsre 
 |-  ( D |` ( RR X. RR ) ) = ( ( abs o. - ) |` ( RR X. RR ) )
32 31 eqcomi 
 |-  ( ( abs o. - ) |` ( RR X. RR ) ) = ( D |` ( RR X. RR ) )
33 32 blres 
 |-  ( ( D e. ( *Met ` RR* ) /\ y e. ( RR* i^i RR ) /\ r e. RR* ) -> ( y ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) = ( ( y ( ball ` D ) r ) i^i RR ) )
34 23 28 30 33 mp3an2i 
 |-  ( ( ( ( x e. ( ordTop ` <_ ) /\ y e. x ) /\ y e. RR ) /\ r e. RR+ ) -> ( y ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) = ( ( y ( ball ` D ) r ) i^i RR ) )
35 1 xrsblre 
 |-  ( ( y e. RR /\ r e. RR* ) -> ( y ( ball ` D ) r ) C_ RR )
36 29 35 sylan2 
 |-  ( ( y e. RR /\ r e. RR+ ) -> ( y ( ball ` D ) r ) C_ RR )
37 36 adantll 
 |-  ( ( ( ( x e. ( ordTop ` <_ ) /\ y e. x ) /\ y e. RR ) /\ r e. RR+ ) -> ( y ( ball ` D ) r ) C_ RR )
38 df-ss 
 |-  ( ( y ( ball ` D ) r ) C_ RR <-> ( ( y ( ball ` D ) r ) i^i RR ) = ( y ( ball ` D ) r ) )
39 37 38 sylib 
 |-  ( ( ( ( x e. ( ordTop ` <_ ) /\ y e. x ) /\ y e. RR ) /\ r e. RR+ ) -> ( ( y ( ball ` D ) r ) i^i RR ) = ( y ( ball ` D ) r ) )
40 34 39 eqtrd 
 |-  ( ( ( ( x e. ( ordTop ` <_ ) /\ y e. x ) /\ y e. RR ) /\ r e. RR+ ) -> ( y ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) = ( y ( ball ` D ) r ) )
41 40 sseq1d 
 |-  ( ( ( ( x e. ( ordTop ` <_ ) /\ y e. x ) /\ y e. RR ) /\ r e. RR+ ) -> ( ( y ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ ( x i^i RR ) <-> ( y ( ball ` D ) r ) C_ ( x i^i RR ) ) )
42 inss1 
 |-  ( x i^i RR ) C_ x
43 sstr 
 |-  ( ( ( y ( ball ` D ) r ) C_ ( x i^i RR ) /\ ( x i^i RR ) C_ x ) -> ( y ( ball ` D ) r ) C_ x )
44 42 43 mpan2 
 |-  ( ( y ( ball ` D ) r ) C_ ( x i^i RR ) -> ( y ( ball ` D ) r ) C_ x )
45 41 44 syl6bi 
 |-  ( ( ( ( x e. ( ordTop ` <_ ) /\ y e. x ) /\ y e. RR ) /\ r e. RR+ ) -> ( ( y ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ ( x i^i RR ) -> ( y ( ball ` D ) r ) C_ x ) )
46 45 reximdva 
 |-  ( ( ( x e. ( ordTop ` <_ ) /\ y e. x ) /\ y e. RR ) -> ( E. r e. RR+ ( y ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ ( x i^i RR ) -> E. r e. RR+ ( y ( ball ` D ) r ) C_ x ) )
47 22 46 mpd 
 |-  ( ( ( x e. ( ordTop ` <_ ) /\ y e. x ) /\ y e. RR ) -> E. r e. RR+ ( y ( ball ` D ) r ) C_ x )
48 1rp 
 |-  1 e. RR+
49 5 sselda 
 |-  ( ( x e. ( ordTop ` <_ ) /\ y e. x ) -> y e. RR* )
50 49 adantr 
 |-  ( ( ( x e. ( ordTop ` <_ ) /\ y e. x ) /\ -. y e. RR ) -> y e. RR* )
51 rpxr 
 |-  ( 1 e. RR+ -> 1 e. RR* )
52 48 51 mp1i 
 |-  ( ( ( x e. ( ordTop ` <_ ) /\ y e. x ) /\ -. y e. RR ) -> 1 e. RR* )
53 elbl 
 |-  ( ( D e. ( *Met ` RR* ) /\ y e. RR* /\ 1 e. RR* ) -> ( z e. ( y ( ball ` D ) 1 ) <-> ( z e. RR* /\ ( y D z ) < 1 ) ) )
54 23 50 52 53 mp3an2i 
 |-  ( ( ( x e. ( ordTop ` <_ ) /\ y e. x ) /\ -. y e. RR ) -> ( z e. ( y ( ball ` D ) 1 ) <-> ( z e. RR* /\ ( y D z ) < 1 ) ) )
55 simp2 
 |-  ( ( ( x e. ( ordTop ` <_ ) /\ y e. x ) /\ -. y e. RR /\ ( z e. RR* /\ ( y D z ) < 1 ) ) -> -. y e. RR )
56 49 3ad2ant1 
 |-  ( ( ( x e. ( ordTop ` <_ ) /\ y e. x ) /\ -. y e. RR /\ ( z e. RR* /\ ( y D z ) < 1 ) ) -> y e. RR* )
57 56 adantr 
 |-  ( ( ( ( x e. ( ordTop ` <_ ) /\ y e. x ) /\ -. y e. RR /\ ( z e. RR* /\ ( y D z ) < 1 ) ) /\ y =/= z ) -> y e. RR* )
58 simpl3l 
 |-  ( ( ( ( x e. ( ordTop ` <_ ) /\ y e. x ) /\ -. y e. RR /\ ( z e. RR* /\ ( y D z ) < 1 ) ) /\ y =/= z ) -> z e. RR* )
59 xmetcl 
 |-  ( ( D e. ( *Met ` RR* ) /\ y e. RR* /\ z e. RR* ) -> ( y D z ) e. RR* )
60 23 57 58 59 mp3an2i 
 |-  ( ( ( ( x e. ( ordTop ` <_ ) /\ y e. x ) /\ -. y e. RR /\ ( z e. RR* /\ ( y D z ) < 1 ) ) /\ y =/= z ) -> ( y D z ) e. RR* )
61 1red 
 |-  ( ( ( ( x e. ( ordTop ` <_ ) /\ y e. x ) /\ -. y e. RR /\ ( z e. RR* /\ ( y D z ) < 1 ) ) /\ y =/= z ) -> 1 e. RR )
62 xmetge0 
 |-  ( ( D e. ( *Met ` RR* ) /\ y e. RR* /\ z e. RR* ) -> 0 <_ ( y D z ) )
63 23 57 58 62 mp3an2i 
 |-  ( ( ( ( x e. ( ordTop ` <_ ) /\ y e. x ) /\ -. y e. RR /\ ( z e. RR* /\ ( y D z ) < 1 ) ) /\ y =/= z ) -> 0 <_ ( y D z ) )
64 simpl3r 
 |-  ( ( ( ( x e. ( ordTop ` <_ ) /\ y e. x ) /\ -. y e. RR /\ ( z e. RR* /\ ( y D z ) < 1 ) ) /\ y =/= z ) -> ( y D z ) < 1 )
65 1xr 
 |-  1 e. RR*
66 xrltle 
 |-  ( ( ( y D z ) e. RR* /\ 1 e. RR* ) -> ( ( y D z ) < 1 -> ( y D z ) <_ 1 ) )
67 60 65 66 sylancl 
 |-  ( ( ( ( x e. ( ordTop ` <_ ) /\ y e. x ) /\ -. y e. RR /\ ( z e. RR* /\ ( y D z ) < 1 ) ) /\ y =/= z ) -> ( ( y D z ) < 1 -> ( y D z ) <_ 1 ) )
68 64 67 mpd 
 |-  ( ( ( ( x e. ( ordTop ` <_ ) /\ y e. x ) /\ -. y e. RR /\ ( z e. RR* /\ ( y D z ) < 1 ) ) /\ y =/= z ) -> ( y D z ) <_ 1 )
69 xrrege0 
 |-  ( ( ( ( y D z ) e. RR* /\ 1 e. RR ) /\ ( 0 <_ ( y D z ) /\ ( y D z ) <_ 1 ) ) -> ( y D z ) e. RR )
70 60 61 63 68 69 syl22anc 
 |-  ( ( ( ( x e. ( ordTop ` <_ ) /\ y e. x ) /\ -. y e. RR /\ ( z e. RR* /\ ( y D z ) < 1 ) ) /\ y =/= z ) -> ( y D z ) e. RR )
71 simpr 
 |-  ( ( ( ( x e. ( ordTop ` <_ ) /\ y e. x ) /\ -. y e. RR /\ ( z e. RR* /\ ( y D z ) < 1 ) ) /\ y =/= z ) -> y =/= z )
72 1 xrsdsreclb 
 |-  ( ( y e. RR* /\ z e. RR* /\ y =/= z ) -> ( ( y D z ) e. RR <-> ( y e. RR /\ z e. RR ) ) )
73 57 58 71 72 syl3anc 
 |-  ( ( ( ( x e. ( ordTop ` <_ ) /\ y e. x ) /\ -. y e. RR /\ ( z e. RR* /\ ( y D z ) < 1 ) ) /\ y =/= z ) -> ( ( y D z ) e. RR <-> ( y e. RR /\ z e. RR ) ) )
74 70 73 mpbid 
 |-  ( ( ( ( x e. ( ordTop ` <_ ) /\ y e. x ) /\ -. y e. RR /\ ( z e. RR* /\ ( y D z ) < 1 ) ) /\ y =/= z ) -> ( y e. RR /\ z e. RR ) )
75 74 simpld 
 |-  ( ( ( ( x e. ( ordTop ` <_ ) /\ y e. x ) /\ -. y e. RR /\ ( z e. RR* /\ ( y D z ) < 1 ) ) /\ y =/= z ) -> y e. RR )
76 75 ex 
 |-  ( ( ( x e. ( ordTop ` <_ ) /\ y e. x ) /\ -. y e. RR /\ ( z e. RR* /\ ( y D z ) < 1 ) ) -> ( y =/= z -> y e. RR ) )
77 76 necon1bd 
 |-  ( ( ( x e. ( ordTop ` <_ ) /\ y e. x ) /\ -. y e. RR /\ ( z e. RR* /\ ( y D z ) < 1 ) ) -> ( -. y e. RR -> y = z ) )
78 simp1r 
 |-  ( ( ( x e. ( ordTop ` <_ ) /\ y e. x ) /\ -. y e. RR /\ ( z e. RR* /\ ( y D z ) < 1 ) ) -> y e. x )
79 elequ1 
 |-  ( y = z -> ( y e. x <-> z e. x ) )
80 78 79 syl5ibcom 
 |-  ( ( ( x e. ( ordTop ` <_ ) /\ y e. x ) /\ -. y e. RR /\ ( z e. RR* /\ ( y D z ) < 1 ) ) -> ( y = z -> z e. x ) )
81 77 80 syld 
 |-  ( ( ( x e. ( ordTop ` <_ ) /\ y e. x ) /\ -. y e. RR /\ ( z e. RR* /\ ( y D z ) < 1 ) ) -> ( -. y e. RR -> z e. x ) )
82 55 81 mpd 
 |-  ( ( ( x e. ( ordTop ` <_ ) /\ y e. x ) /\ -. y e. RR /\ ( z e. RR* /\ ( y D z ) < 1 ) ) -> z e. x )
83 82 3expia 
 |-  ( ( ( x e. ( ordTop ` <_ ) /\ y e. x ) /\ -. y e. RR ) -> ( ( z e. RR* /\ ( y D z ) < 1 ) -> z e. x ) )
84 54 83 sylbid 
 |-  ( ( ( x e. ( ordTop ` <_ ) /\ y e. x ) /\ -. y e. RR ) -> ( z e. ( y ( ball ` D ) 1 ) -> z e. x ) )
85 84 ssrdv 
 |-  ( ( ( x e. ( ordTop ` <_ ) /\ y e. x ) /\ -. y e. RR ) -> ( y ( ball ` D ) 1 ) C_ x )
86 oveq2 
 |-  ( r = 1 -> ( y ( ball ` D ) r ) = ( y ( ball ` D ) 1 ) )
87 86 sseq1d 
 |-  ( r = 1 -> ( ( y ( ball ` D ) r ) C_ x <-> ( y ( ball ` D ) 1 ) C_ x ) )
88 87 rspcev 
 |-  ( ( 1 e. RR+ /\ ( y ( ball ` D ) 1 ) C_ x ) -> E. r e. RR+ ( y ( ball ` D ) r ) C_ x )
89 48 85 88 sylancr 
 |-  ( ( ( x e. ( ordTop ` <_ ) /\ y e. x ) /\ -. y e. RR ) -> E. r e. RR+ ( y ( ball ` D ) r ) C_ x )
90 47 89 pm2.61dan 
 |-  ( ( x e. ( ordTop ` <_ ) /\ y e. x ) -> E. r e. RR+ ( y ( ball ` D ) r ) C_ x )
91 90 ralrimiva 
 |-  ( x e. ( ordTop ` <_ ) -> A. y e. x E. r e. RR+ ( y ( ball ` D ) r ) C_ x )
92 2 elmopn2 
 |-  ( D e. ( *Met ` RR* ) -> ( x e. J <-> ( x C_ RR* /\ A. y e. x E. r e. RR+ ( y ( ball ` D ) r ) C_ x ) ) )
93 23 92 ax-mp 
 |-  ( x e. J <-> ( x C_ RR* /\ A. y e. x E. r e. RR+ ( y ( ball ` D ) r ) C_ x ) )
94 5 91 93 sylanbrc 
 |-  ( x e. ( ordTop ` <_ ) -> x e. J )
95 94 ssriv 
 |-  ( ordTop ` <_ ) C_ J