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 ` <_ ) |`t RR )
Assertion xrtgioo 
|- ( topGen ` ran (,) ) = J

Proof

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