Metamath Proof Explorer

Theorem xrtgioo

Description: The topology on the extended reals coincides with the standard topology on the reals, when restricted to RR . (Contributed by Mario Carneiro, 3-Sep-2015)

Ref Expression
Hypothesis xrtgioo.1 ⊢J=ordTop⁡≤↾𝑡ℝ
Assertion xrtgioo ⊢topGen⁡ran⁡.=J

Proof

Step Hyp Ref Expression
1 xrtgioo.1 ⊢J=ordTop⁡≤↾𝑡ℝ
2 letop ⊢ordTop⁡≤∈Top
3 ioof ⊢.:ℝ*×ℝ*⟶𝒫ℝ
4 ffn ⊢.:ℝ*×ℝ*⟶𝒫ℝ→.Fnℝ*×ℝ*
5 3 4 ax-mp ⊢.Fnℝ*×ℝ*
6 iooordt ⊢xy∈ordTop⁡≤
7 6 rgen2w ⊢∀x∈ℝ*∀y∈ℝ*xy∈ordTop⁡≤
8 ffnov ⊢.:ℝ*×ℝ*⟶ordTop⁡≤↔.Fnℝ*×ℝ*∧∀x∈ℝ*∀y∈ℝ*xy∈ordTop⁡≤
9 5 7 8 mpbir2an ⊢.:ℝ*×ℝ*⟶ordTop⁡≤
10 frn ⊢.:ℝ*×ℝ*⟶ordTop⁡≤→ran⁡.⊆ordTop⁡≤
11 9 10 ax-mp ⊢ran⁡.⊆ordTop⁡≤
12 tgss ⊢ordTop⁡≤∈Top∧ran⁡.⊆ordTop⁡≤→topGen⁡ran⁡.⊆topGen⁡ordTop⁡≤
13 2 11 12 mp2an ⊢topGen⁡ran⁡.⊆topGen⁡ordTop⁡≤
14 tgtop ⊢ordTop⁡≤∈Top→topGen⁡ordTop⁡≤=ordTop⁡≤
15 2 14 ax-mp ⊢topGen⁡ordTop⁡≤=ordTop⁡≤
16 13 15 sseqtri ⊢topGen⁡ran⁡.⊆ordTop⁡≤
17 16 sseli ⊢x∈topGen⁡ran⁡.→x∈ordTop⁡≤
18 retopon ⊢topGen⁡ran⁡.∈TopOn⁡ℝ
19 toponss ⊢topGen⁡ran⁡.∈TopOn⁡ℝ∧x∈topGen⁡ran⁡.→x⊆ℝ
20 18 19 mpan ⊢x∈topGen⁡ran⁡.→x⊆ℝ
21 reordt ⊢ℝ∈ordTop⁡≤
22 restopn2 ⊢ordTop⁡≤∈Top∧ℝ∈ordTop⁡≤→x∈ordTop⁡≤↾𝑡ℝ↔x∈ordTop⁡≤∧x⊆ℝ
23 2 21 22 mp2an ⊢x∈ordTop⁡≤↾𝑡ℝ↔x∈ordTop⁡≤∧x⊆ℝ
24 17 20 23 sylanbrc ⊢x∈topGen⁡ran⁡.→x∈ordTop⁡≤↾𝑡ℝ
25 24 ssriv ⊢topGen⁡ran⁡.⊆ordTop⁡≤↾𝑡ℝ
26 eqid ⊢ran⁡x∈ℝ*⟼x+∞=ran⁡x∈ℝ*⟼x+∞
27 eqid ⊢ran⁡x∈ℝ*⟼−∞x=ran⁡x∈ℝ*⟼−∞x
28 eqid ⊢ran⁡.=ran⁡.
29 26 27 28 leordtval ⊢ordTop⁡≤=topGen⁡ran⁡x∈ℝ*⟼x+∞∪ran⁡x∈ℝ*⟼−∞x∪ran⁡.
30 29 oveq1i ⊢ordTop⁡≤↾𝑡ℝ=topGen⁡ran⁡x∈ℝ*⟼x+∞∪ran⁡x∈ℝ*⟼−∞x∪ran⁡.↾𝑡ℝ
31 29 2 eqeltrri ⊢topGen⁡ran⁡x∈ℝ*⟼x+∞∪ran⁡x∈ℝ*⟼−∞x∪ran⁡.∈Top
32 tgclb ⊢ran⁡x∈ℝ*⟼x+∞∪ran⁡x∈ℝ*⟼−∞x∪ran⁡.∈TopBases↔topGen⁡ran⁡x∈ℝ*⟼x+∞∪ran⁡x∈ℝ*⟼−∞x∪ran⁡.∈Top
33 31 32 mpbir ⊢ran⁡x∈ℝ*⟼x+∞∪ran⁡x∈ℝ*⟼−∞x∪ran⁡.∈TopBases
34 reex ⊢ℝ∈V
35 tgrest ⊢ran⁡x∈ℝ*⟼x+∞∪ran⁡x∈ℝ*⟼−∞x∪ran⁡.∈TopBases∧ℝ∈V→topGen⁡ran⁡x∈ℝ*⟼x+∞∪ran⁡x∈ℝ*⟼−∞x∪ran⁡.↾𝑡ℝ=topGen⁡ran⁡x∈ℝ*⟼x+∞∪ran⁡x∈ℝ*⟼−∞x∪ran⁡.↾𝑡ℝ
36 33 34 35 mp2an ⊢topGen⁡ran⁡x∈ℝ*⟼x+∞∪ran⁡x∈ℝ*⟼−∞x∪ran⁡.↾𝑡ℝ=topGen⁡ran⁡x∈ℝ*⟼x+∞∪ran⁡x∈ℝ*⟼−∞x∪ran⁡.↾𝑡ℝ
37 30 36 eqtr4i ⊢ordTop⁡≤↾𝑡ℝ=topGen⁡ran⁡x∈ℝ*⟼x+∞∪ran⁡x∈ℝ*⟼−∞x∪ran⁡.↾𝑡ℝ
38 retopbas ⊢ran⁡.∈TopBases
39 elrest ⊢ran⁡x∈ℝ*⟼x+∞∪ran⁡x∈ℝ*⟼−∞x∪ran⁡.∈TopBases∧ℝ∈V→u∈ran⁡x∈ℝ*⟼x+∞∪ran⁡x∈ℝ*⟼−∞x∪ran⁡.↾𝑡ℝ↔∃v∈ran⁡x∈ℝ*⟼x+∞∪ran⁡x∈ℝ*⟼−∞x∪ran⁡.u=v∩ℝ
40 33 34 39 mp2an ⊢u∈ran⁡x∈ℝ*⟼x+∞∪ran⁡x∈ℝ*⟼−∞x∪ran⁡.↾𝑡ℝ↔∃v∈ran⁡x∈ℝ*⟼x+∞∪ran⁡x∈ℝ*⟼−∞x∪ran⁡.u=v∩ℝ
41 elun ⊢v∈ran⁡x∈ℝ*⟼x+∞∪ran⁡x∈ℝ*⟼−∞x∪ran⁡.↔v∈ran⁡x∈ℝ*⟼x+∞∪ran⁡x∈ℝ*⟼−∞x∨v∈ran⁡.
42 elun ⊢v∈ran⁡x∈ℝ*⟼x+∞∪ran⁡x∈ℝ*⟼−∞x↔v∈ran⁡x∈ℝ*⟼x+∞∨v∈ran⁡x∈ℝ*⟼−∞x
43 eqid ⊢x∈ℝ*⟼x+∞=x∈ℝ*⟼x+∞
44 43 elrnmpt ⊢v∈V→v∈ran⁡x∈ℝ*⟼x+∞↔∃x∈ℝ*v=x+∞
45 44 elv ⊢v∈ran⁡x∈ℝ*⟼x+∞↔∃x∈ℝ*v=x+∞
46 simpl ⊢x∈ℝ*∧y∈ℝ→x∈ℝ*
47 pnfxr ⊢+∞∈ℝ*
48 47 a1i ⊢x∈ℝ*∧y∈ℝ→+∞∈ℝ*
49 rexr ⊢y∈ℝ→y∈ℝ*
50 49 adantl ⊢x∈ℝ*∧y∈ℝ→y∈ℝ*
51 df-ioc ⊢.=a∈ℝ*,b∈ℝ*⟼c∈ℝ*|a<c∧c≤b
52 51 elixx3g ⊢y∈x+∞↔x∈ℝ*∧+∞∈ℝ*∧y∈ℝ*∧x<y∧y≤+∞
53 52 baib ⊢x∈ℝ*∧+∞∈ℝ*∧y∈ℝ*→y∈x+∞↔x<y∧y≤+∞
54 46 48 50 53 syl3anc ⊢x∈ℝ*∧y∈ℝ→y∈x+∞↔x<y∧y≤+∞
55 pnfge ⊢y∈ℝ*→y≤+∞
56 50 55 syl ⊢x∈ℝ*∧y∈ℝ→y≤+∞
57 56 biantrud ⊢x∈ℝ*∧y∈ℝ→x<y↔x<y∧y≤+∞
58 ltpnf ⊢y∈ℝ→y<+∞
59 58 adantl ⊢x∈ℝ*∧y∈ℝ→y<+∞
60 59 biantrud ⊢x∈ℝ*∧y∈ℝ→x<y↔x<y∧y<+∞
61 54 57 60 3bitr2d ⊢x∈ℝ*∧y∈ℝ→y∈x+∞↔x<y∧y<+∞
62 61 pm5.32da ⊢x∈ℝ*→y∈ℝ∧y∈x+∞↔y∈ℝ∧x<y∧y<+∞
63 elin ⊢y∈x+∞∩ℝ↔y∈x+∞∧y∈ℝ
64 63 biancomi ⊢y∈x+∞∩ℝ↔y∈ℝ∧y∈x+∞
65 3anass ⊢y∈ℝ∧x<y∧y<+∞↔y∈ℝ∧x<y∧y<+∞
66 62 64 65 3bitr4g ⊢x∈ℝ*→y∈x+∞∩ℝ↔y∈ℝ∧x<y∧y<+∞
67 elioo2 ⊢x∈ℝ*∧+∞∈ℝ*→y∈x+∞↔y∈ℝ∧x<y∧y<+∞
68 47 67 mpan2 ⊢x∈ℝ*→y∈x+∞↔y∈ℝ∧x<y∧y<+∞
69 66 68 bitr4d ⊢x∈ℝ*→y∈x+∞∩ℝ↔y∈x+∞
70 69 eqrdv ⊢x∈ℝ*→x+∞∩ℝ=x+∞
71 ioorebas ⊢x+∞∈ran⁡.
72 70 71 eqeltrdi ⊢x∈ℝ*→x+∞∩ℝ∈ran⁡.
73 ineq1 ⊢v=x+∞→v∩ℝ=x+∞∩ℝ
74 73 eleq1d ⊢v=x+∞→v∩ℝ∈ran⁡.↔x+∞∩ℝ∈ran⁡.
75 72 74 syl5ibrcom ⊢x∈ℝ*→v=x+∞→v∩ℝ∈ran⁡.
76 75 rexlimiv ⊢∃x∈ℝ*v=x+∞→v∩ℝ∈ran⁡.
77 45 76 sylbi ⊢v∈ran⁡x∈ℝ*⟼x+∞→v∩ℝ∈ran⁡.
78 eqid ⊢x∈ℝ*⟼−∞x=x∈ℝ*⟼−∞x
79 78 elrnmpt ⊢v∈V→v∈ran⁡x∈ℝ*⟼−∞x↔∃x∈ℝ*v=−∞x
80 79 elv ⊢v∈ran⁡x∈ℝ*⟼−∞x↔∃x∈ℝ*v=−∞x
81 mnfxr ⊢−∞∈ℝ*
82 81 a1i ⊢x∈ℝ*∧y∈ℝ→−∞∈ℝ*
83 df-ico ⊢.=a∈ℝ*,b∈ℝ*⟼c∈ℝ*|a≤c∧c<b
84 83 elixx3g ⊢y∈−∞x↔−∞∈ℝ*∧x∈ℝ*∧y∈ℝ*∧−∞≤y∧y<x
85 84 baib ⊢−∞∈ℝ*∧x∈ℝ*∧y∈ℝ*→y∈−∞x↔−∞≤y∧y<x
86 82 46 50 85 syl3anc ⊢x∈ℝ*∧y∈ℝ→y∈−∞x↔−∞≤y∧y<x
87 mnfle ⊢y∈ℝ*→−∞≤y
88 50 87 syl ⊢x∈ℝ*∧y∈ℝ→−∞≤y
89 88 biantrurd ⊢x∈ℝ*∧y∈ℝ→y<x↔−∞≤y∧y<x
90 mnflt ⊢y∈ℝ→−∞<y
91 90 adantl ⊢x∈ℝ*∧y∈ℝ→−∞<y
92 91 biantrurd ⊢x∈ℝ*∧y∈ℝ→y<x↔−∞<y∧y<x
93 86 89 92 3bitr2d ⊢x∈ℝ*∧y∈ℝ→y∈−∞x↔−∞<y∧y<x
94 93 pm5.32da ⊢x∈ℝ*→y∈ℝ∧y∈−∞x↔y∈ℝ∧−∞<y∧y<x
95 elin ⊢y∈−∞x∩ℝ↔y∈−∞x∧y∈ℝ
96 95 biancomi ⊢y∈−∞x∩ℝ↔y∈ℝ∧y∈−∞x
97 3anass ⊢y∈ℝ∧−∞<y∧y<x↔y∈ℝ∧−∞<y∧y<x
98 94 96 97 3bitr4g ⊢x∈ℝ*→y∈−∞x∩ℝ↔y∈ℝ∧−∞<y∧y<x
99 elioo2 ⊢−∞∈ℝ*∧x∈ℝ*→y∈−∞x↔y∈ℝ∧−∞<y∧y<x
100 81 99 mpan ⊢x∈ℝ*→y∈−∞x↔y∈ℝ∧−∞<y∧y<x
101 98 100 bitr4d ⊢x∈ℝ*→y∈−∞x∩ℝ↔y∈−∞x
102 101 eqrdv ⊢x∈ℝ*→−∞x∩ℝ=−∞x
103 ioorebas ⊢−∞x∈ran⁡.
104 102 103 eqeltrdi ⊢x∈ℝ*→−∞x∩ℝ∈ran⁡.
105 ineq1 ⊢v=−∞x→v∩ℝ=−∞x∩ℝ
106 105 eleq1d ⊢v=−∞x→v∩ℝ∈ran⁡.↔−∞x∩ℝ∈ran⁡.
107 104 106 syl5ibrcom ⊢x∈ℝ*→v=−∞x→v∩ℝ∈ran⁡.
108 107 rexlimiv ⊢∃x∈ℝ*v=−∞x→v∩ℝ∈ran⁡.
109 80 108 sylbi ⊢v∈ran⁡x∈ℝ*⟼−∞x→v∩ℝ∈ran⁡.
110 77 109 jaoi ⊢v∈ran⁡x∈ℝ*⟼x+∞∨v∈ran⁡x∈ℝ*⟼−∞x→v∩ℝ∈ran⁡.
111 42 110 sylbi ⊢v∈ran⁡x∈ℝ*⟼x+∞∪ran⁡x∈ℝ*⟼−∞x→v∩ℝ∈ran⁡.
112 elssuni ⊢v∈ran⁡.→v⊆⋃ran⁡.
113 unirnioo ⊢ℝ=⋃ran⁡.
114 112 113 sseqtrrdi ⊢v∈ran⁡.→v⊆ℝ
115 df-ss ⊢v⊆ℝ↔v∩ℝ=v
116 114 115 sylib ⊢v∈ran⁡.→v∩ℝ=v
117 id ⊢v∈ran⁡.→v∈ran⁡.
118 116 117 eqeltrd ⊢v∈ran⁡.→v∩ℝ∈ran⁡.
119 111 118 jaoi ⊢v∈ran⁡x∈ℝ*⟼x+∞∪ran⁡x∈ℝ*⟼−∞x∨v∈ran⁡.→v∩ℝ∈ran⁡.
120 41 119 sylbi ⊢v∈ran⁡x∈ℝ*⟼x+∞∪ran⁡x∈ℝ*⟼−∞x∪ran⁡.→v∩ℝ∈ran⁡.
121 eleq1 ⊢u=v∩ℝ→u∈ran⁡.↔v∩ℝ∈ran⁡.
122 120 121 syl5ibrcom ⊢v∈ran⁡x∈ℝ*⟼x+∞∪ran⁡x∈ℝ*⟼−∞x∪ran⁡.→u=v∩ℝ→u∈ran⁡.
123 122 rexlimiv ⊢∃v∈ran⁡x∈ℝ*⟼x+∞∪ran⁡x∈ℝ*⟼−∞x∪ran⁡.u=v∩ℝ→u∈ran⁡.
124 40 123 sylbi ⊢u∈ran⁡x∈ℝ*⟼x+∞∪ran⁡x∈ℝ*⟼−∞x∪ran⁡.↾𝑡ℝ→u∈ran⁡.
125 124 ssriv ⊢ran⁡x∈ℝ*⟼x+∞∪ran⁡x∈ℝ*⟼−∞x∪ran⁡.↾𝑡ℝ⊆ran⁡.
126 tgss ⊢ran⁡.∈TopBases∧ran⁡x∈ℝ*⟼x+∞∪ran⁡x∈ℝ*⟼−∞x∪ran⁡.↾𝑡ℝ⊆ran⁡.→topGen⁡ran⁡x∈ℝ*⟼x+∞∪ran⁡x∈ℝ*⟼−∞x∪ran⁡.↾𝑡ℝ⊆topGen⁡ran⁡.
127 38 125 126 mp2an ⊢topGen⁡ran⁡x∈ℝ*⟼x+∞∪ran⁡x∈ℝ*⟼−∞x∪ran⁡.↾𝑡ℝ⊆topGen⁡ran⁡.
128 37 127 eqsstri ⊢ordTop⁡≤↾𝑡ℝ⊆topGen⁡ran⁡.
129 25 128 eqssi ⊢topGen⁡ran⁡.=ordTop⁡≤↾𝑡ℝ
130 129 1 eqtr4i ⊢topGen⁡ran⁡.=J