Metamath Proof Explorer

Theorem relowlssretop

Description: The lower limit topology on the reals is finer than the standard topology. (Contributed by ML, 1-Aug-2020)

Ref Expression
Hypothesis relowlssretop.1 
|- I = ( [,) " ( RR X. RR ) )
Assertion relowlssretop 
|- ( topGen ` ran (,) ) C_ ( topGen ` I )

Proof

Step Hyp Ref Expression
1 relowlssretop.1 
 |-  I = ( [,) " ( RR X. RR ) )
2 ioof 
 |-  (,) : ( RR* X. RR* ) --> ~P RR
3 ffn 
 |-  ( (,) : ( RR* X. RR* ) --> ~P RR -> (,) Fn ( RR* X. RR* ) )
4 ovelrn 
 |-  ( (,) Fn ( RR* X. RR* ) -> ( o e. ran (,) <-> E. a e. RR* E. b e. RR* o = ( a (,) b ) ) )
5 2 3 4 mp2b 
 |-  ( o e. ran (,) <-> E. a e. RR* E. b e. RR* o = ( a (,) b ) )
6 elxr 
 |-  ( b e. RR* <-> ( b e. RR \/ b = +oo \/ b = -oo ) )
7 simpr 
 |-  ( ( a e. RR* /\ b e. RR ) -> b e. RR )
8 elioore 
 |-  ( x e. ( a (,) b ) -> x e. RR )
9 7 8 anim12ci 
 |-  ( ( ( a e. RR* /\ b e. RR ) /\ x e. ( a (,) b ) ) -> ( x e. RR /\ b e. RR ) )
10 1 icoreelrn 
 |-  ( ( x e. RR /\ b e. RR ) -> { z e. RR | ( x <_ z /\ z < b ) } e. I )
11 9 10 syl 
 |-  ( ( ( a e. RR* /\ b e. RR ) /\ x e. ( a (,) b ) ) -> { z e. RR | ( x <_ z /\ z < b ) } e. I )
12 8 adantl 
 |-  ( ( ( a e. RR* /\ b e. RR ) /\ x e. ( a (,) b ) ) -> x e. RR )
13 8 leidd 
 |-  ( x e. ( a (,) b ) -> x <_ x )
14 13 adantl 
 |-  ( ( ( a e. RR* /\ b e. RR ) /\ x e. ( a (,) b ) ) -> x <_ x )
15 7 rexrd 
 |-  ( ( a e. RR* /\ b e. RR ) -> b e. RR* )
16 elioo1 
 |-  ( ( a e. RR* /\ b e. RR* ) -> ( x e. ( a (,) b ) <-> ( x e. RR* /\ a < x /\ x < b ) ) )
17 15 16 syldan 
 |-  ( ( a e. RR* /\ b e. RR ) -> ( x e. ( a (,) b ) <-> ( x e. RR* /\ a < x /\ x < b ) ) )
18 17 biimpa 
 |-  ( ( ( a e. RR* /\ b e. RR ) /\ x e. ( a (,) b ) ) -> ( x e. RR* /\ a < x /\ x < b ) )
19 18 simp3d 
 |-  ( ( ( a e. RR* /\ b e. RR ) /\ x e. ( a (,) b ) ) -> x < b )
20 rexr 
 |-  ( x e. RR -> x e. RR* )
21 20 3anim1i 
 |-  ( ( x e. RR /\ x <_ x /\ x < b ) -> ( x e. RR* /\ x <_ x /\ x < b ) )
22 rexr 
 |-  ( b e. RR -> b e. RR* )
23 elico1 
 |-  ( ( x e. RR* /\ b e. RR* ) -> ( x e. ( x [,) b ) <-> ( x e. RR* /\ x <_ x /\ x < b ) ) )
24 20 22 23 syl2an 
 |-  ( ( x e. RR /\ b e. RR ) -> ( x e. ( x [,) b ) <-> ( x e. RR* /\ x <_ x /\ x < b ) ) )
25 24 biimprd 
 |-  ( ( x e. RR /\ b e. RR ) -> ( ( x e. RR* /\ x <_ x /\ x < b ) -> x e. ( x [,) b ) ) )
26 9 21 25 syl2im 
 |-  ( ( ( a e. RR* /\ b e. RR ) /\ x e. ( a (,) b ) ) -> ( ( x e. RR /\ x <_ x /\ x < b ) -> x e. ( x [,) b ) ) )
27 icoreval 
 |-  ( ( x e. RR /\ b e. RR ) -> ( x [,) b ) = { z e. RR | ( x <_ z /\ z < b ) } )
28 9 27 syl 
 |-  ( ( ( a e. RR* /\ b e. RR ) /\ x e. ( a (,) b ) ) -> ( x [,) b ) = { z e. RR | ( x <_ z /\ z < b ) } )
29 28 eleq2d 
 |-  ( ( ( a e. RR* /\ b e. RR ) /\ x e. ( a (,) b ) ) -> ( x e. ( x [,) b ) <-> x e. { z e. RR | ( x <_ z /\ z < b ) } ) )
30 26 29 sylibd 
 |-  ( ( ( a e. RR* /\ b e. RR ) /\ x e. ( a (,) b ) ) -> ( ( x e. RR /\ x <_ x /\ x < b ) -> x e. { z e. RR | ( x <_ z /\ z < b ) } ) )
31 12 14 19 30 mp3and 
 |-  ( ( ( a e. RR* /\ b e. RR ) /\ x e. ( a (,) b ) ) -> x e. { z e. RR | ( x <_ z /\ z < b ) } )
32 nfv 
 |-  F/ z ( ( a e. RR* /\ b e. RR* ) /\ x e. ( a (,) b ) )
33 nfrab1 
 |-  F/_ z { z e. RR | ( x <_ z /\ z < b ) }
34 nfcv 
 |-  F/_ z ( a (,) b )
35 iooval 
 |-  ( ( a e. RR* /\ b e. RR* ) -> ( a (,) b ) = { x e. RR* | ( a < x /\ x < b ) } )
36 35 eleq2d 
 |-  ( ( a e. RR* /\ b e. RR* ) -> ( x e. ( a (,) b ) <-> x e. { x e. RR* | ( a < x /\ x < b ) } ) )
37 36 anbi1d 
 |-  ( ( a e. RR* /\ b e. RR* ) -> ( ( x e. ( a (,) b ) /\ z e. { z e. RR | ( x <_ z /\ z < b ) } ) <-> ( x e. { x e. RR* | ( a < x /\ x < b ) } /\ z e. { z e. RR | ( x <_ z /\ z < b ) } ) ) )
38 37 pm5.32i 
 |-  ( ( ( a e. RR* /\ b e. RR* ) /\ ( x e. ( a (,) b ) /\ z e. { z e. RR | ( x <_ z /\ z < b ) } ) ) <-> ( ( a e. RR* /\ b e. RR* ) /\ ( x e. { x e. RR* | ( a < x /\ x < b ) } /\ z e. { z e. RR | ( x <_ z /\ z < b ) } ) ) )
39 rabid 
 |-  ( x e. { x e. RR* | ( a < x /\ x < b ) } <-> ( x e. RR* /\ ( a < x /\ x < b ) ) )
40 rabid 
 |-  ( z e. { z e. RR | ( x <_ z /\ z < b ) } <-> ( z e. RR /\ ( x <_ z /\ z < b ) ) )
41 39 40 anbi12i 
 |-  ( ( x e. { x e. RR* | ( a < x /\ x < b ) } /\ z e. { z e. RR | ( x <_ z /\ z < b ) } ) <-> ( ( x e. RR* /\ ( a < x /\ x < b ) ) /\ ( z e. RR /\ ( x <_ z /\ z < b ) ) ) )
42 simpl 
 |-  ( ( z e. RR /\ ( x <_ z /\ z < b ) ) -> z e. RR )
43 42 rexrd 
 |-  ( ( z e. RR /\ ( x <_ z /\ z < b ) ) -> z e. RR* )
44 43 ad2antll 
 |-  ( ( a e. RR* /\ ( ( x e. RR* /\ ( a < x /\ x < b ) ) /\ ( z e. RR /\ ( x <_ z /\ z < b ) ) ) ) -> z e. RR* )
45 simpl 
 |-  ( ( x e. RR* /\ ( a < x /\ x < b ) ) -> x e. RR* )
46 45 43 anim12i 
 |-  ( ( ( x e. RR* /\ ( a < x /\ x < b ) ) /\ ( z e. RR /\ ( x <_ z /\ z < b ) ) ) -> ( x e. RR* /\ z e. RR* ) )
47 46 anim2i 
 |-  ( ( a e. RR* /\ ( ( x e. RR* /\ ( a < x /\ x < b ) ) /\ ( z e. RR /\ ( x <_ z /\ z < b ) ) ) ) -> ( a e. RR* /\ ( x e. RR* /\ z e. RR* ) ) )
48 3anass 
 |-  ( ( a e. RR* /\ x e. RR* /\ z e. RR* ) <-> ( a e. RR* /\ ( x e. RR* /\ z e. RR* ) ) )
49 47 48 sylibr 
 |-  ( ( a e. RR* /\ ( ( x e. RR* /\ ( a < x /\ x < b ) ) /\ ( z e. RR /\ ( x <_ z /\ z < b ) ) ) ) -> ( a e. RR* /\ x e. RR* /\ z e. RR* ) )
50 simprl 
 |-  ( ( x e. RR* /\ ( a < x /\ x < b ) ) -> a < x )
51 simprl 
 |-  ( ( z e. RR /\ ( x <_ z /\ z < b ) ) -> x <_ z )
52 50 51 anim12i 
 |-  ( ( ( x e. RR* /\ ( a < x /\ x < b ) ) /\ ( z e. RR /\ ( x <_ z /\ z < b ) ) ) -> ( a < x /\ x <_ z ) )
53 52 adantl 
 |-  ( ( a e. RR* /\ ( ( x e. RR* /\ ( a < x /\ x < b ) ) /\ ( z e. RR /\ ( x <_ z /\ z < b ) ) ) ) -> ( a < x /\ x <_ z ) )
54 xrltletr 
 |-  ( ( a e. RR* /\ x e. RR* /\ z e. RR* ) -> ( ( a < x /\ x <_ z ) -> a < z ) )
55 49 53 54 sylc 
 |-  ( ( a e. RR* /\ ( ( x e. RR* /\ ( a < x /\ x < b ) ) /\ ( z e. RR /\ ( x <_ z /\ z < b ) ) ) ) -> a < z )
56 simprr 
 |-  ( ( z e. RR /\ ( x <_ z /\ z < b ) ) -> z < b )
57 56 ad2antll 
 |-  ( ( a e. RR* /\ ( ( x e. RR* /\ ( a < x /\ x < b ) ) /\ ( z e. RR /\ ( x <_ z /\ z < b ) ) ) ) -> z < b )
58 55 57 jca 
 |-  ( ( a e. RR* /\ ( ( x e. RR* /\ ( a < x /\ x < b ) ) /\ ( z e. RR /\ ( x <_ z /\ z < b ) ) ) ) -> ( a < z /\ z < b ) )
59 rabid 
 |-  ( z e. { z e. RR* | ( a < z /\ z < b ) } <-> ( z e. RR* /\ ( a < z /\ z < b ) ) )
60 44 58 59 sylanbrc 
 |-  ( ( a e. RR* /\ ( ( x e. RR* /\ ( a < x /\ x < b ) ) /\ ( z e. RR /\ ( x <_ z /\ z < b ) ) ) ) -> z e. { z e. RR* | ( a < z /\ z < b ) } )
61 60 adantlr 
 |-  ( ( ( a e. RR* /\ b e. RR* ) /\ ( ( x e. RR* /\ ( a < x /\ x < b ) ) /\ ( z e. RR /\ ( x <_ z /\ z < b ) ) ) ) -> z e. { z e. RR* | ( a < z /\ z < b ) } )
62 iooval 
 |-  ( ( a e. RR* /\ b e. RR* ) -> ( a (,) b ) = { z e. RR* | ( a < z /\ z < b ) } )
63 62 adantr 
 |-  ( ( ( a e. RR* /\ b e. RR* ) /\ ( ( x e. RR* /\ ( a < x /\ x < b ) ) /\ ( z e. RR /\ ( x <_ z /\ z < b ) ) ) ) -> ( a (,) b ) = { z e. RR* | ( a < z /\ z < b ) } )
64 61 63 eleqtrrd 
 |-  ( ( ( a e. RR* /\ b e. RR* ) /\ ( ( x e. RR* /\ ( a < x /\ x < b ) ) /\ ( z e. RR /\ ( x <_ z /\ z < b ) ) ) ) -> z e. ( a (,) b ) )
65 41 64 sylan2b 
 |-  ( ( ( a e. RR* /\ b e. RR* ) /\ ( x e. { x e. RR* | ( a < x /\ x < b ) } /\ z e. { z e. RR | ( x <_ z /\ z < b ) } ) ) -> z e. ( a (,) b ) )
66 38 65 sylbi 
 |-  ( ( ( a e. RR* /\ b e. RR* ) /\ ( x e. ( a (,) b ) /\ z e. { z e. RR | ( x <_ z /\ z < b ) } ) ) -> z e. ( a (,) b ) )
67 66 expr 
 |-  ( ( ( a e. RR* /\ b e. RR* ) /\ x e. ( a (,) b ) ) -> ( z e. { z e. RR | ( x <_ z /\ z < b ) } -> z e. ( a (,) b ) ) )
68 32 33 34 67 ssrd 
 |-  ( ( ( a e. RR* /\ b e. RR* ) /\ x e. ( a (,) b ) ) -> { z e. RR | ( x <_ z /\ z < b ) } C_ ( a (,) b ) )
69 22 68 sylanl2 
 |-  ( ( ( a e. RR* /\ b e. RR ) /\ x e. ( a (,) b ) ) -> { z e. RR | ( x <_ z /\ z < b ) } C_ ( a (,) b ) )
70 eleq2 
 |-  ( i = { z e. RR | ( x <_ z /\ z < b ) } -> ( x e. i <-> x e. { z e. RR | ( x <_ z /\ z < b ) } ) )
71 sseq1 
 |-  ( i = { z e. RR | ( x <_ z /\ z < b ) } -> ( i C_ ( a (,) b ) <-> { z e. RR | ( x <_ z /\ z < b ) } C_ ( a (,) b ) ) )
72 70 71 anbi12d 
 |-  ( i = { z e. RR | ( x <_ z /\ z < b ) } -> ( ( x e. i /\ i C_ ( a (,) b ) ) <-> ( x e. { z e. RR | ( x <_ z /\ z < b ) } /\ { z e. RR | ( x <_ z /\ z < b ) } C_ ( a (,) b ) ) ) )
73 72 rspcev 
 |-  ( ( { z e. RR | ( x <_ z /\ z < b ) } e. I /\ ( x e. { z e. RR | ( x <_ z /\ z < b ) } /\ { z e. RR | ( x <_ z /\ z < b ) } C_ ( a (,) b ) ) ) -> E. i e. I ( x e. i /\ i C_ ( a (,) b ) ) )
74 11 31 69 73 syl12anc 
 |-  ( ( ( a e. RR* /\ b e. RR ) /\ x e. ( a (,) b ) ) -> E. i e. I ( x e. i /\ i C_ ( a (,) b ) ) )
75 74 ancom1s 
 |-  ( ( ( b e. RR /\ a e. RR* ) /\ x e. ( a (,) b ) ) -> E. i e. I ( x e. i /\ i C_ ( a (,) b ) ) )
76 75 expl 
 |-  ( b e. RR -> ( ( a e. RR* /\ x e. ( a (,) b ) ) -> E. i e. I ( x e. i /\ i C_ ( a (,) b ) ) ) )
77 8 adantl 
 |-  ( ( ( a e. RR* /\ b = +oo ) /\ x e. ( a (,) b ) ) -> x e. RR )
78 peano2re 
 |-  ( x e. RR -> ( x + 1 ) e. RR )
79 1 icoreelrn 
 |-  ( ( x e. RR /\ ( x + 1 ) e. RR ) -> { z e. RR | ( x <_ z /\ z < ( x + 1 ) ) } e. I )
80 77 78 79 syl2anc2 
 |-  ( ( ( a e. RR* /\ b = +oo ) /\ x e. ( a (,) b ) ) -> { z e. RR | ( x <_ z /\ z < ( x + 1 ) ) } e. I )
81 elioore 
 |-  ( x e. ( a (,) +oo ) -> x e. RR )
82 81 adantl 
 |-  ( ( a e. RR* /\ x e. ( a (,) +oo ) ) -> x e. RR )
83 82 leidd 
 |-  ( ( a e. RR* /\ x e. ( a (,) +oo ) ) -> x <_ x )
84 82 ltp1d 
 |-  ( ( a e. RR* /\ x e. ( a (,) +oo ) ) -> x < ( x + 1 ) )
85 82 83 84 jca32 
 |-  ( ( a e. RR* /\ x e. ( a (,) +oo ) ) -> ( x e. RR /\ ( x <_ x /\ x < ( x + 1 ) ) ) )
86 breq2 
 |-  ( z = x -> ( x <_ z <-> x <_ x ) )
87 breq1 
 |-  ( z = x -> ( z < ( x + 1 ) <-> x < ( x + 1 ) ) )
88 86 87 anbi12d 
 |-  ( z = x -> ( ( x <_ z /\ z < ( x + 1 ) ) <-> ( x <_ x /\ x < ( x + 1 ) ) ) )
89 88 elrab 
 |-  ( x e. { z e. RR | ( x <_ z /\ z < ( x + 1 ) ) } <-> ( x e. RR /\ ( x <_ x /\ x < ( x + 1 ) ) ) )
90 85 89 sylibr 
 |-  ( ( a e. RR* /\ x e. ( a (,) +oo ) ) -> x e. { z e. RR | ( x <_ z /\ z < ( x + 1 ) ) } )
91 nfv 
 |-  F/ z ( a e. RR* /\ x e. ( a (,) +oo ) )
92 nfrab1 
 |-  F/_ z { z e. RR | ( x <_ z /\ z < ( x + 1 ) ) }
93 nfcv 
 |-  F/_ z ( a (,) +oo )
94 rabid 
 |-  ( z e. { z e. RR | ( x <_ z /\ z < ( x + 1 ) ) } <-> ( z e. RR /\ ( x <_ z /\ z < ( x + 1 ) ) ) )
95 simprl 
 |-  ( ( ( a e. RR* /\ x e. ( a (,) +oo ) ) /\ ( z e. RR /\ ( x <_ z /\ z < ( x + 1 ) ) ) ) -> z e. RR )
96 simpll 
 |-  ( ( ( a e. RR* /\ x e. ( a (,) +oo ) ) /\ ( z e. RR /\ ( x <_ z /\ z < ( x + 1 ) ) ) ) -> a e. RR* )
97 82 adantr 
 |-  ( ( ( a e. RR* /\ x e. ( a (,) +oo ) ) /\ ( z e. RR /\ ( x <_ z /\ z < ( x + 1 ) ) ) ) -> x e. RR )
98 97 rexrd 
 |-  ( ( ( a e. RR* /\ x e. ( a (,) +oo ) ) /\ ( z e. RR /\ ( x <_ z /\ z < ( x + 1 ) ) ) ) -> x e. RR* )
99 95 rexrd 
 |-  ( ( ( a e. RR* /\ x e. ( a (,) +oo ) ) /\ ( z e. RR /\ ( x <_ z /\ z < ( x + 1 ) ) ) ) -> z e. RR* )
100 elioopnf 
 |-  ( a e. RR* -> ( x e. ( a (,) +oo ) <-> ( x e. RR /\ a < x ) ) )
101 100 simplbda 
 |-  ( ( a e. RR* /\ x e. ( a (,) +oo ) ) -> a < x )
102 101 adantr 
 |-  ( ( ( a e. RR* /\ x e. ( a (,) +oo ) ) /\ ( z e. RR /\ ( x <_ z /\ z < ( x + 1 ) ) ) ) -> a < x )
103 simprl 
 |-  ( ( z e. RR /\ ( x <_ z /\ z < ( x + 1 ) ) ) -> x <_ z )
104 103 adantl 
 |-  ( ( ( a e. RR* /\ x e. ( a (,) +oo ) ) /\ ( z e. RR /\ ( x <_ z /\ z < ( x + 1 ) ) ) ) -> x <_ z )
105 96 98 99 102 104 xrltletrd 
 |-  ( ( ( a e. RR* /\ x e. ( a (,) +oo ) ) /\ ( z e. RR /\ ( x <_ z /\ z < ( x + 1 ) ) ) ) -> a < z )
106 elioopnf 
 |-  ( a e. RR* -> ( z e. ( a (,) +oo ) <-> ( z e. RR /\ a < z ) ) )
107 106 biimprd 
 |-  ( a e. RR* -> ( ( z e. RR /\ a < z ) -> z e. ( a (,) +oo ) ) )
108 107 adantr 
 |-  ( ( a e. RR* /\ x e. ( a (,) +oo ) ) -> ( ( z e. RR /\ a < z ) -> z e. ( a (,) +oo ) ) )
109 108 adantr 
 |-  ( ( ( a e. RR* /\ x e. ( a (,) +oo ) ) /\ ( z e. RR /\ ( x <_ z /\ z < ( x + 1 ) ) ) ) -> ( ( z e. RR /\ a < z ) -> z e. ( a (,) +oo ) ) )
110 95 105 109 mp2and 
 |-  ( ( ( a e. RR* /\ x e. ( a (,) +oo ) ) /\ ( z e. RR /\ ( x <_ z /\ z < ( x + 1 ) ) ) ) -> z e. ( a (,) +oo ) )
111 110 ex 
 |-  ( ( a e. RR* /\ x e. ( a (,) +oo ) ) -> ( ( z e. RR /\ ( x <_ z /\ z < ( x + 1 ) ) ) -> z e. ( a (,) +oo ) ) )
112 94 111 biimtrid 
 |-  ( ( a e. RR* /\ x e. ( a (,) +oo ) ) -> ( z e. { z e. RR | ( x <_ z /\ z < ( x + 1 ) ) } -> z e. ( a (,) +oo ) ) )
113 91 92 93 112 ssrd 
 |-  ( ( a e. RR* /\ x e. ( a (,) +oo ) ) -> { z e. RR | ( x <_ z /\ z < ( x + 1 ) ) } C_ ( a (,) +oo ) )
114 90 113 jca 
 |-  ( ( a e. RR* /\ x e. ( a (,) +oo ) ) -> ( x e. { z e. RR | ( x <_ z /\ z < ( x + 1 ) ) } /\ { z e. RR | ( x <_ z /\ z < ( x + 1 ) ) } C_ ( a (,) +oo ) ) )
115 oveq2 
 |-  ( b = +oo -> ( a (,) b ) = ( a (,) +oo ) )
116 115 eleq2d 
 |-  ( b = +oo -> ( x e. ( a (,) b ) <-> x e. ( a (,) +oo ) ) )
117 116 anbi2d 
 |-  ( b = +oo -> ( ( a e. RR* /\ x e. ( a (,) b ) ) <-> ( a e. RR* /\ x e. ( a (,) +oo ) ) ) )
118 115 sseq2d 
 |-  ( b = +oo -> ( { z e. RR | ( x <_ z /\ z < ( x + 1 ) ) } C_ ( a (,) b ) <-> { z e. RR | ( x <_ z /\ z < ( x + 1 ) ) } C_ ( a (,) +oo ) ) )
119 118 anbi2d 
 |-  ( b = +oo -> ( ( x e. { z e. RR | ( x <_ z /\ z < ( x + 1 ) ) } /\ { z e. RR | ( x <_ z /\ z < ( x + 1 ) ) } C_ ( a (,) b ) ) <-> ( x e. { z e. RR | ( x <_ z /\ z < ( x + 1 ) ) } /\ { z e. RR | ( x <_ z /\ z < ( x + 1 ) ) } C_ ( a (,) +oo ) ) ) )
120 117 119 imbi12d 
 |-  ( b = +oo -> ( ( ( a e. RR* /\ x e. ( a (,) b ) ) -> ( x e. { z e. RR | ( x <_ z /\ z < ( x + 1 ) ) } /\ { z e. RR | ( x <_ z /\ z < ( x + 1 ) ) } C_ ( a (,) b ) ) ) <-> ( ( a e. RR* /\ x e. ( a (,) +oo ) ) -> ( x e. { z e. RR | ( x <_ z /\ z < ( x + 1 ) ) } /\ { z e. RR | ( x <_ z /\ z < ( x + 1 ) ) } C_ ( a (,) +oo ) ) ) ) )
121 114 120 mpbiri 
 |-  ( b = +oo -> ( ( a e. RR* /\ x e. ( a (,) b ) ) -> ( x e. { z e. RR | ( x <_ z /\ z < ( x + 1 ) ) } /\ { z e. RR | ( x <_ z /\ z < ( x + 1 ) ) } C_ ( a (,) b ) ) ) )
122 121 impl 
 |-  ( ( ( b = +oo /\ a e. RR* ) /\ x e. ( a (,) b ) ) -> ( x e. { z e. RR | ( x <_ z /\ z < ( x + 1 ) ) } /\ { z e. RR | ( x <_ z /\ z < ( x + 1 ) ) } C_ ( a (,) b ) ) )
123 122 ancom1s 
 |-  ( ( ( a e. RR* /\ b = +oo ) /\ x e. ( a (,) b ) ) -> ( x e. { z e. RR | ( x <_ z /\ z < ( x + 1 ) ) } /\ { z e. RR | ( x <_ z /\ z < ( x + 1 ) ) } C_ ( a (,) b ) ) )
124 eleq2 
 |-  ( i = { z e. RR | ( x <_ z /\ z < ( x + 1 ) ) } -> ( x e. i <-> x e. { z e. RR | ( x <_ z /\ z < ( x + 1 ) ) } ) )
125 sseq1 
 |-  ( i = { z e. RR | ( x <_ z /\ z < ( x + 1 ) ) } -> ( i C_ ( a (,) b ) <-> { z e. RR | ( x <_ z /\ z < ( x + 1 ) ) } C_ ( a (,) b ) ) )
126 124 125 anbi12d 
 |-  ( i = { z e. RR | ( x <_ z /\ z < ( x + 1 ) ) } -> ( ( x e. i /\ i C_ ( a (,) b ) ) <-> ( x e. { z e. RR | ( x <_ z /\ z < ( x + 1 ) ) } /\ { z e. RR | ( x <_ z /\ z < ( x + 1 ) ) } C_ ( a (,) b ) ) ) )
127 126 rspcev 
 |-  ( ( { z e. RR | ( x <_ z /\ z < ( x + 1 ) ) } e. I /\ ( x e. { z e. RR | ( x <_ z /\ z < ( x + 1 ) ) } /\ { z e. RR | ( x <_ z /\ z < ( x + 1 ) ) } C_ ( a (,) b ) ) ) -> E. i e. I ( x e. i /\ i C_ ( a (,) b ) ) )
128 80 123 127 syl2anc 
 |-  ( ( ( a e. RR* /\ b = +oo ) /\ x e. ( a (,) b ) ) -> E. i e. I ( x e. i /\ i C_ ( a (,) b ) ) )
129 128 ancom1s 
 |-  ( ( ( b = +oo /\ a e. RR* ) /\ x e. ( a (,) b ) ) -> E. i e. I ( x e. i /\ i C_ ( a (,) b ) ) )
130 129 expl 
 |-  ( b = +oo -> ( ( a e. RR* /\ x e. ( a (,) b ) ) -> E. i e. I ( x e. i /\ i C_ ( a (,) b ) ) ) )
131 8 adantl 
 |-  ( ( ( a e. RR* /\ b = -oo ) /\ x e. ( a (,) b ) ) -> x e. RR )
132 oveq2 
 |-  ( b = -oo -> ( a (,) b ) = ( a (,) -oo ) )
133 132 eleq2d 
 |-  ( b = -oo -> ( x e. ( a (,) b ) <-> x e. ( a (,) -oo ) ) )
134 133 adantl 
 |-  ( ( a e. RR* /\ b = -oo ) -> ( x e. ( a (,) b ) <-> x e. ( a (,) -oo ) ) )
135 134 pm5.32i 
 |-  ( ( ( a e. RR* /\ b = -oo ) /\ x e. ( a (,) b ) ) <-> ( ( a e. RR* /\ b = -oo ) /\ x e. ( a (,) -oo ) ) )
136 nltmnf 
 |-  ( x e. RR* -> -. x < -oo )
137 136 intnand 
 |-  ( x e. RR* -> -. ( a < x /\ x < -oo ) )
138 eliooord 
 |-  ( x e. ( a (,) -oo ) -> ( a < x /\ x < -oo ) )
139 137 138 nsyl 
 |-  ( x e. RR* -> -. x e. ( a (,) -oo ) )
140 139 pm2.21d 
 |-  ( x e. RR* -> ( x e. ( a (,) -oo ) -> ( ( a e. RR* /\ b = -oo ) -> E. i e. I ( x e. i /\ i C_ ( a (,) b ) ) ) ) )
141 140 impd 
 |-  ( x e. RR* -> ( ( x e. ( a (,) -oo ) /\ ( a e. RR* /\ b = -oo ) ) -> E. i e. I ( x e. i /\ i C_ ( a (,) b ) ) ) )
142 141 ancomsd 
 |-  ( x e. RR* -> ( ( ( a e. RR* /\ b = -oo ) /\ x e. ( a (,) -oo ) ) -> E. i e. I ( x e. i /\ i C_ ( a (,) b ) ) ) )
143 135 142 biimtrid 
 |-  ( x e. RR* -> ( ( ( a e. RR* /\ b = -oo ) /\ x e. ( a (,) b ) ) -> E. i e. I ( x e. i /\ i C_ ( a (,) b ) ) ) )
144 20 143 syl 
 |-  ( x e. RR -> ( ( ( a e. RR* /\ b = -oo ) /\ x e. ( a (,) b ) ) -> E. i e. I ( x e. i /\ i C_ ( a (,) b ) ) ) )
145 131 144 mpcom 
 |-  ( ( ( a e. RR* /\ b = -oo ) /\ x e. ( a (,) b ) ) -> E. i e. I ( x e. i /\ i C_ ( a (,) b ) ) )
146 145 ancom1s 
 |-  ( ( ( b = -oo /\ a e. RR* ) /\ x e. ( a (,) b ) ) -> E. i e. I ( x e. i /\ i C_ ( a (,) b ) ) )
147 146 expl 
 |-  ( b = -oo -> ( ( a e. RR* /\ x e. ( a (,) b ) ) -> E. i e. I ( x e. i /\ i C_ ( a (,) b ) ) ) )
148 76 130 147 3jaoi 
 |-  ( ( b e. RR \/ b = +oo \/ b = -oo ) -> ( ( a e. RR* /\ x e. ( a (,) b ) ) -> E. i e. I ( x e. i /\ i C_ ( a (,) b ) ) ) )
149 6 148 sylbi 
 |-  ( b e. RR* -> ( ( a e. RR* /\ x e. ( a (,) b ) ) -> E. i e. I ( x e. i /\ i C_ ( a (,) b ) ) ) )
150 149 expdimp 
 |-  ( ( b e. RR* /\ a e. RR* ) -> ( x e. ( a (,) b ) -> E. i e. I ( x e. i /\ i C_ ( a (,) b ) ) ) )
151 150 ancoms 
 |-  ( ( a e. RR* /\ b e. RR* ) -> ( x e. ( a (,) b ) -> E. i e. I ( x e. i /\ i C_ ( a (,) b ) ) ) )
152 eleq2 
 |-  ( o = ( a (,) b ) -> ( x e. o <-> x e. ( a (,) b ) ) )
153 sseq2 
 |-  ( o = ( a (,) b ) -> ( i C_ o <-> i C_ ( a (,) b ) ) )
154 153 anbi2d 
 |-  ( o = ( a (,) b ) -> ( ( x e. i /\ i C_ o ) <-> ( x e. i /\ i C_ ( a (,) b ) ) ) )
155 154 rexbidv 
 |-  ( o = ( a (,) b ) -> ( E. i e. I ( x e. i /\ i C_ o ) <-> E. i e. I ( x e. i /\ i C_ ( a (,) b ) ) ) )
156 152 155 imbi12d 
 |-  ( o = ( a (,) b ) -> ( ( x e. o -> E. i e. I ( x e. i /\ i C_ o ) ) <-> ( x e. ( a (,) b ) -> E. i e. I ( x e. i /\ i C_ ( a (,) b ) ) ) ) )
157 151 156 syl5ibrcom 
 |-  ( ( a e. RR* /\ b e. RR* ) -> ( o = ( a (,) b ) -> ( x e. o -> E. i e. I ( x e. i /\ i C_ o ) ) ) )
158 157 rexlimivv 
 |-  ( E. a e. RR* E. b e. RR* o = ( a (,) b ) -> ( x e. o -> E. i e. I ( x e. i /\ i C_ o ) ) )
159 5 158 sylbi 
 |-  ( o e. ran (,) -> ( x e. o -> E. i e. I ( x e. i /\ i C_ o ) ) )
160 159 rgen 
 |-  A. o e. ran (,) ( x e. o -> E. i e. I ( x e. i /\ i C_ o ) )
161 160 rgenw 
 |-  A. x e. RR A. o e. ran (,) ( x e. o -> E. i e. I ( x e. i /\ i C_ o ) )
162 iooex 
 |-  (,) e. _V
163 162 rnex 
 |-  ran (,) e. _V
164 unirnioo 
 |-  RR = U. ran (,)
165 1 icoreunrn 
 |-  RR = U. I
166 164 165 eqtr3i 
 |-  U. ran (,) = U. I
167 tgss2 
 |-  ( ( ran (,) e. _V /\ U. ran (,) = U. I ) -> ( ( topGen ` ran (,) ) C_ ( topGen ` I ) <-> A. x e. U. ran (,) A. o e. ran (,) ( x e. o -> E. i e. I ( x e. i /\ i C_ o ) ) ) )
168 163 166 167 mp2an 
 |-  ( ( topGen ` ran (,) ) C_ ( topGen ` I ) <-> A. x e. U. ran (,) A. o e. ran (,) ( x e. o -> E. i e. I ( x e. i /\ i C_ o ) ) )
169 164 raleqi 
 |-  ( A. x e. RR A. o e. ran (,) ( x e. o -> E. i e. I ( x e. i /\ i C_ o ) ) <-> A. x e. U. ran (,) A. o e. ran (,) ( x e. o -> E. i e. I ( x e. i /\ i C_ o ) ) )
170 168 169 bitr4i 
 |-  ( ( topGen ` ran (,) ) C_ ( topGen ` I ) <-> A. x e. RR A. o e. ran (,) ( x e. o -> E. i e. I ( x e. i /\ i C_ o ) ) )
171 161 170 mpbir 
 |-  ( topGen ` ran (,) ) C_ ( topGen ` I )