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 𝑠 *
xrsmopn.1 J = MetOpen D
Assertion xrsmopn ordTop J

Proof

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