Metamath Proof Explorer

Theorem tgioo

Description: The topology generated by open intervals of reals is the same as the open sets of the standard metric space on the reals. (Contributed by NM, 7-May-2007) (Revised by Mario Carneiro, 13-Nov-2013)

Ref Expression
Hypotheses remet.1 ⊢D=abs∘−↾ℝ2
tgioo.2 ⊢J=MetOpen⁡D
Assertion tgioo ⊢topGen⁡ran⁡.=J

Proof

Step Hyp Ref Expression
1 remet.1 ⊢D=abs∘−↾ℝ2
2 tgioo.2 ⊢J=MetOpen⁡D
3 1 rexmet ⊢D∈∞Met⁡ℝ
4 2 mopnval ⊢D∈∞Met⁡ℝ→J=topGen⁡ran⁡ball⁡D
5 3 4 ax-mp ⊢J=topGen⁡ran⁡ball⁡D
6 1 blssioo ⊢ran⁡ball⁡D⊆ran⁡.
7 elssuni ⊢v∈ran⁡.→v⊆⋃ran⁡.
8 unirnioo ⊢ℝ=⋃ran⁡.
9 7 8 sseqtrrdi ⊢v∈ran⁡.→v⊆ℝ
10 retopbas ⊢ran⁡.∈TopBases
11 10 a1i ⊢v∈ran⁡.∧x∈v→ran⁡.∈TopBases
12 simpl ⊢v∈ran⁡.∧x∈v→v∈ran⁡.
13 9 sselda ⊢v∈ran⁡.∧x∈v→x∈ℝ
14 1re ⊢1∈ℝ
15 1 bl2ioo ⊢x∈ℝ∧1∈ℝ→xball⁡D1=x−1x+1
16 14 15 mpan2 ⊢x∈ℝ→xball⁡D1=x−1x+1
17 ioof ⊢.:ℝ*×ℝ*⟶𝒫ℝ
18 ffn ⊢.:ℝ*×ℝ*⟶𝒫ℝ→.Fnℝ*×ℝ*
19 17 18 ax-mp ⊢.Fnℝ*×ℝ*
20 peano2rem ⊢x∈ℝ→x−1∈ℝ
21 20 rexrd ⊢x∈ℝ→x−1∈ℝ*
22 peano2re ⊢x∈ℝ→x+1∈ℝ
23 22 rexrd ⊢x∈ℝ→x+1∈ℝ*
24 fnovrn ⊢.Fnℝ*×ℝ*∧x−1∈ℝ*∧x+1∈ℝ*→x−1x+1∈ran⁡.
25 19 21 23 24 mp3an2i ⊢x∈ℝ→x−1x+1∈ran⁡.
26 16 25 eqeltrd ⊢x∈ℝ→xball⁡D1∈ran⁡.
27 13 26 syl ⊢v∈ran⁡.∧x∈v→xball⁡D1∈ran⁡.
28 simpr ⊢v∈ran⁡.∧x∈v→x∈v
29 1rp ⊢1∈ℝ+
30 blcntr ⊢D∈∞Met⁡ℝ∧x∈ℝ∧1∈ℝ+→x∈xball⁡D1
31 3 29 30 mp3an13 ⊢x∈ℝ→x∈xball⁡D1
32 13 31 syl ⊢v∈ran⁡.∧x∈v→x∈xball⁡D1
33 28 32 elind ⊢v∈ran⁡.∧x∈v→x∈v∩xball⁡D1
34 basis2 ⊢ran⁡.∈TopBases∧v∈ran⁡.∧xball⁡D1∈ran⁡.∧x∈v∩xball⁡D1→∃z∈ran⁡.x∈z∧z⊆v∩xball⁡D1
35 11 12 27 33 34 syl22anc ⊢v∈ran⁡.∧x∈v→∃z∈ran⁡.x∈z∧z⊆v∩xball⁡D1
36 ovelrn ⊢.Fnℝ*×ℝ*→z∈ran⁡.↔∃a∈ℝ*∃b∈ℝ*z=ab
37 19 36 ax-mp ⊢z∈ran⁡.↔∃a∈ℝ*∃b∈ℝ*z=ab
38 eleq2 ⊢z=ab→x∈z↔x∈ab
39 sseq1 ⊢z=ab→z⊆v∩xball⁡D1↔ab⊆v∩xball⁡D1
40 38 39 anbi12d ⊢z=ab→x∈z∧z⊆v∩xball⁡D1↔x∈ab∧ab⊆v∩xball⁡D1
41 inss2 ⊢v∩xball⁡D1⊆xball⁡D1
42 sstr ⊢ab⊆v∩xball⁡D1∧v∩xball⁡D1⊆xball⁡D1→ab⊆xball⁡D1
43 41 42 mpan2 ⊢ab⊆v∩xball⁡D1→ab⊆xball⁡D1
44 43 adantl ⊢x∈ab∧ab⊆v∩xball⁡D1→ab⊆xball⁡D1
45 elioore ⊢x∈ab→x∈ℝ
46 45 adantr ⊢x∈ab∧ab⊆v∩xball⁡D1→x∈ℝ
47 46 16 syl ⊢x∈ab∧ab⊆v∩xball⁡D1→xball⁡D1=x−1x+1
48 44 47 sseqtrd ⊢x∈ab∧ab⊆v∩xball⁡D1→ab⊆x−1x+1
49 dfss ⊢ab⊆x−1x+1↔ab=ab∩x−1x+1
50 48 49 sylib ⊢x∈ab∧ab⊆v∩xball⁡D1→ab=ab∩x−1x+1
51 eliooxr ⊢x∈ab→a∈ℝ*∧b∈ℝ*
52 21 23 jca ⊢x∈ℝ→x−1∈ℝ*∧x+1∈ℝ*
53 45 52 syl ⊢x∈ab→x−1∈ℝ*∧x+1∈ℝ*
54 iooin ⊢a∈ℝ*∧b∈ℝ*∧x−1∈ℝ*∧x+1∈ℝ*→ab∩x−1x+1=ifa≤x−1x−1aifb≤x+1bx+1
55 51 53 54 syl2anc ⊢x∈ab→ab∩x−1x+1=ifa≤x−1x−1aifb≤x+1bx+1
56 55 adantr ⊢x∈ab∧ab⊆v∩xball⁡D1→ab∩x−1x+1=ifa≤x−1x−1aifb≤x+1bx+1
57 50 56 eqtrd ⊢x∈ab∧ab⊆v∩xball⁡D1→ab=ifa≤x−1x−1aifb≤x+1bx+1
58 mnfxr ⊢−∞∈ℝ*
59 58 a1i ⊢x∈ab∧ab⊆v∩xball⁡D1→−∞∈ℝ*
60 46 21 syl ⊢x∈ab∧ab⊆v∩xball⁡D1→x−1∈ℝ*
61 51 adantr ⊢x∈ab∧ab⊆v∩xball⁡D1→a∈ℝ*∧b∈ℝ*
62 61 simpld ⊢x∈ab∧ab⊆v∩xball⁡D1→a∈ℝ*
63 60 62 ifcld ⊢x∈ab∧ab⊆v∩xball⁡D1→ifa≤x−1x−1a∈ℝ*
64 61 simprd ⊢x∈ab∧ab⊆v∩xball⁡D1→b∈ℝ*
65 46 22 syl ⊢x∈ab∧ab⊆v∩xball⁡D1→x+1∈ℝ
66 65 rexrd ⊢x∈ab∧ab⊆v∩xball⁡D1→x+1∈ℝ*
67 64 66 ifcld ⊢x∈ab∧ab⊆v∩xball⁡D1→ifb≤x+1bx+1∈ℝ*
68 45 20 syl ⊢x∈ab→x−1∈ℝ
69 68 adantr ⊢x∈ab∧ab⊆v∩xball⁡D1→x−1∈ℝ
70 69 mnfltd ⊢x∈ab∧ab⊆v∩xball⁡D1→−∞<x−1
71 xrmax2 ⊢a∈ℝ*∧x−1∈ℝ*→x−1≤ifa≤x−1x−1a
72 62 60 71 syl2anc ⊢x∈ab∧ab⊆v∩xball⁡D1→x−1≤ifa≤x−1x−1a
73 59 60 63 70 72 xrltletrd ⊢x∈ab∧ab⊆v∩xball⁡D1→−∞<ifa≤x−1x−1a
74 simpl ⊢x∈ab∧ab⊆v∩xball⁡D1→x∈ab
75 74 57 eleqtrd ⊢x∈ab∧ab⊆v∩xball⁡D1→x∈ifa≤x−1x−1aifb≤x+1bx+1
76 eliooxr ⊢x∈ifa≤x−1x−1aifb≤x+1bx+1→ifa≤x−1x−1a∈ℝ*∧ifb≤x+1bx+1∈ℝ*
77 ne0i ⊢x∈ifa≤x−1x−1aifb≤x+1bx+1→ifa≤x−1x−1aifb≤x+1bx+1≠∅
78 ioon0 ⊢ifa≤x−1x−1a∈ℝ*∧ifb≤x+1bx+1∈ℝ*→ifa≤x−1x−1aifb≤x+1bx+1≠∅↔ifa≤x−1x−1a<ifb≤x+1bx+1
79 77 78 imbitrid ⊢ifa≤x−1x−1a∈ℝ*∧ifb≤x+1bx+1∈ℝ*→x∈ifa≤x−1x−1aifb≤x+1bx+1→ifa≤x−1x−1a<ifb≤x+1bx+1
80 76 79 mpcom ⊢x∈ifa≤x−1x−1aifb≤x+1bx+1→ifa≤x−1x−1a<ifb≤x+1bx+1
81 75 80 syl ⊢x∈ab∧ab⊆v∩xball⁡D1→ifa≤x−1x−1a<ifb≤x+1bx+1
82 xrre2 ⊢−∞∈ℝ*∧ifa≤x−1x−1a∈ℝ*∧ifb≤x+1bx+1∈ℝ*∧−∞<ifa≤x−1x−1a∧ifa≤x−1x−1a<ifb≤x+1bx+1→ifa≤x−1x−1a∈ℝ
83 59 63 67 73 81 82 syl32anc ⊢x∈ab∧ab⊆v∩xball⁡D1→ifa≤x−1x−1a∈ℝ
84 mnfle ⊢ifa≤x−1x−1a∈ℝ*→−∞≤ifa≤x−1x−1a
85 63 84 syl ⊢x∈ab∧ab⊆v∩xball⁡D1→−∞≤ifa≤x−1x−1a
86 59 63 67 85 81 xrlelttrd ⊢x∈ab∧ab⊆v∩xball⁡D1→−∞<ifb≤x+1bx+1
87 xrmin2 ⊢b∈ℝ*∧x+1∈ℝ*→ifb≤x+1bx+1≤x+1
88 64 66 87 syl2anc ⊢x∈ab∧ab⊆v∩xball⁡D1→ifb≤x+1bx+1≤x+1
89 xrre ⊢ifb≤x+1bx+1∈ℝ*∧x+1∈ℝ∧−∞<ifb≤x+1bx+1∧ifb≤x+1bx+1≤x+1→ifb≤x+1bx+1∈ℝ
90 67 65 86 88 89 syl22anc ⊢x∈ab∧ab⊆v∩xball⁡D1→ifb≤x+1bx+1∈ℝ
91 1 ioo2blex ⊢ifa≤x−1x−1a∈ℝ∧ifb≤x+1bx+1∈ℝ→ifa≤x−1x−1aifb≤x+1bx+1∈ran⁡ball⁡D
92 83 90 91 syl2anc ⊢x∈ab∧ab⊆v∩xball⁡D1→ifa≤x−1x−1aifb≤x+1bx+1∈ran⁡ball⁡D
93 57 92 eqeltrd ⊢x∈ab∧ab⊆v∩xball⁡D1→ab∈ran⁡ball⁡D
94 inss1 ⊢v∩xball⁡D1⊆v
95 sstr ⊢ab⊆v∩xball⁡D1∧v∩xball⁡D1⊆v→ab⊆v
96 94 95 mpan2 ⊢ab⊆v∩xball⁡D1→ab⊆v
97 96 adantl ⊢x∈ab∧ab⊆v∩xball⁡D1→ab⊆v
98 sseq1 ⊢z=ab→z⊆v↔ab⊆v
99 38 98 anbi12d ⊢z=ab→x∈z∧z⊆v↔x∈ab∧ab⊆v
100 99 rspcev ⊢ab∈ran⁡ball⁡D∧x∈ab∧ab⊆v→∃z∈ran⁡ball⁡Dx∈z∧z⊆v
101 93 74 97 100 syl12anc ⊢x∈ab∧ab⊆v∩xball⁡D1→∃z∈ran⁡ball⁡Dx∈z∧z⊆v
102 blssex ⊢D∈∞Met⁡ℝ∧x∈ℝ→∃z∈ran⁡ball⁡Dx∈z∧z⊆v↔∃y∈ℝ+xball⁡Dy⊆v
103 3 46 102 sylancr ⊢x∈ab∧ab⊆v∩xball⁡D1→∃z∈ran⁡ball⁡Dx∈z∧z⊆v↔∃y∈ℝ+xball⁡Dy⊆v
104 101 103 mpbid ⊢x∈ab∧ab⊆v∩xball⁡D1→∃y∈ℝ+xball⁡Dy⊆v
105 40 104 syl6bi ⊢z=ab→x∈z∧z⊆v∩xball⁡D1→∃y∈ℝ+xball⁡Dy⊆v
106 105 a1i ⊢a∈ℝ*∧b∈ℝ*→z=ab→x∈z∧z⊆v∩xball⁡D1→∃y∈ℝ+xball⁡Dy⊆v
107 106 rexlimivv ⊢∃a∈ℝ*∃b∈ℝ*z=ab→x∈z∧z⊆v∩xball⁡D1→∃y∈ℝ+xball⁡Dy⊆v
108 107 imp ⊢∃a∈ℝ*∃b∈ℝ*z=ab∧x∈z∧z⊆v∩xball⁡D1→∃y∈ℝ+xball⁡Dy⊆v
109 37 108 sylanb ⊢z∈ran⁡.∧x∈z∧z⊆v∩xball⁡D1→∃y∈ℝ+xball⁡Dy⊆v
110 109 rexlimiva ⊢∃z∈ran⁡.x∈z∧z⊆v∩xball⁡D1→∃y∈ℝ+xball⁡Dy⊆v
111 35 110 syl ⊢v∈ran⁡.∧x∈v→∃y∈ℝ+xball⁡Dy⊆v
112 111 ralrimiva ⊢v∈ran⁡.→∀x∈v∃y∈ℝ+xball⁡Dy⊆v
113 2 elmopn2 ⊢D∈∞Met⁡ℝ→v∈J↔v⊆ℝ∧∀x∈v∃y∈ℝ+xball⁡Dy⊆v
114 3 113 ax-mp ⊢v∈J↔v⊆ℝ∧∀x∈v∃y∈ℝ+xball⁡Dy⊆v
115 9 112 114 sylanbrc ⊢v∈ran⁡.→v∈J
116 115 ssriv ⊢ran⁡.⊆J
117 116 5 sseqtri ⊢ran⁡.⊆topGen⁡ran⁡ball⁡D
118 2basgen ⊢ran⁡ball⁡D⊆ran⁡.∧ran⁡.⊆topGen⁡ran⁡ball⁡D→topGen⁡ran⁡ball⁡D=topGen⁡ran⁡.
119 6 117 118 mp2an ⊢topGen⁡ran⁡ball⁡D=topGen⁡ran⁡.
120 5 119 eqtr2i ⊢topGen⁡ran⁡.=J