Metamath Proof Explorer

Theorem relowlpssretop

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

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

Proof

Step Hyp Ref Expression
1 relowlpssretop.1 
 |-  I = ( [,) " ( RR X. RR ) )
2 1 relowlssretop 
 |-  ( topGen ` ran (,) ) C_ ( topGen ` I )
3 2re 
 |-  2 e. RR
4 1lt2 
 |-  1 < 2
5 ovex 
 |-  ( 1 [,) c ) e. _V
6 sbcan 
 |-  ( [. 1 / x ]. ( c e. RR /\ x < c ) <-> ( [. 1 / x ]. c e. RR /\ [. 1 / x ]. x < c ) )
7 1re 
 |-  1 e. RR
8 sbcg 
 |-  ( 1 e. RR -> ( [. 1 / x ]. c e. RR <-> c e. RR ) )
9 7 8 ax-mp 
 |-  ( [. 1 / x ]. c e. RR <-> c e. RR )
10 sbcbr123 
 |-  ( [. 1 / x ]. x < c <-> [_ 1 / x ]_ x [_ 1 / x ]_ < [_ 1 / x ]_ c )
11 csbvarg 
 |-  ( 1 e. RR -> [_ 1 / x ]_ x = 1 )
12 7 11 ax-mp 
 |-  [_ 1 / x ]_ x = 1
13 csbconstg 
 |-  ( 1 e. RR -> [_ 1 / x ]_ c = c )
14 7 13 ax-mp 
 |-  [_ 1 / x ]_ c = c
15 12 14 breq12i 
 |-  ( [_ 1 / x ]_ x [_ 1 / x ]_ < [_ 1 / x ]_ c <-> 1 [_ 1 / x ]_ < c )
16 csbconstg 
 |-  ( 1 e. RR -> [_ 1 / x ]_ < = < )
17 7 16 ax-mp 
 |-  [_ 1 / x ]_ < = <
18 17 breqi 
 |-  ( 1 [_ 1 / x ]_ < c <-> 1 < c )
19 10 15 18 3bitri 
 |-  ( [. 1 / x ]. x < c <-> 1 < c )
20 9 19 anbi12i 
 |-  ( ( [. 1 / x ]. c e. RR /\ [. 1 / x ]. x < c ) <-> ( c e. RR /\ 1 < c ) )
21 6 20 bitri 
 |-  ( [. 1 / x ]. ( c e. RR /\ x < c ) <-> ( c e. RR /\ 1 < c ) )
22 sbceqg 
 |-  ( 1 e. RR -> ( [. 1 / x ]. i = ( x [,) c ) <-> [_ 1 / x ]_ i = [_ 1 / x ]_ ( x [,) c ) ) )
23 7 22 ax-mp 
 |-  ( [. 1 / x ]. i = ( x [,) c ) <-> [_ 1 / x ]_ i = [_ 1 / x ]_ ( x [,) c ) )
24 csbconstg 
 |-  ( 1 e. RR -> [_ 1 / x ]_ i = i )
25 7 24 ax-mp 
 |-  [_ 1 / x ]_ i = i
26 csbov123 
 |-  [_ 1 / x ]_ ( x [,) c ) = ( [_ 1 / x ]_ x [_ 1 / x ]_ [,) [_ 1 / x ]_ c )
27 csbconstg 
 |-  ( 1 e. RR -> [_ 1 / x ]_ [,) = [,) )
28 7 27 ax-mp 
 |-  [_ 1 / x ]_ [,) = [,)
29 12 14 28 oveq123i 
 |-  ( [_ 1 / x ]_ x [_ 1 / x ]_ [,) [_ 1 / x ]_ c ) = ( 1 [,) c )
30 26 29 eqtri 
 |-  [_ 1 / x ]_ ( x [,) c ) = ( 1 [,) c )
31 25 30 eqeq12i 
 |-  ( [_ 1 / x ]_ i = [_ 1 / x ]_ ( x [,) c ) <-> i = ( 1 [,) c ) )
32 23 31 bitri 
 |-  ( [. 1 / x ]. i = ( x [,) c ) <-> i = ( 1 [,) c ) )
33 sbcan 
 |-  ( [. 1 / x ]. ( ( c e. RR /\ x < c ) /\ i = ( x [,) c ) ) <-> ( [. 1 / x ]. ( c e. RR /\ x < c ) /\ [. 1 / x ]. i = ( x [,) c ) ) )
34 simpr 
 |-  ( ( ( ( c e. RR /\ x < c ) /\ i = ( x [,) c ) ) /\ x e. RR ) -> x e. RR )
35 simpl 
 |-  ( ( x e. RR /\ c e. RR ) -> x e. RR )
36 leid 
 |-  ( x e. RR -> x <_ x )
37 35 36 jccir 
 |-  ( ( x e. RR /\ c e. RR ) -> ( x e. RR /\ x <_ x ) )
38 rexr 
 |-  ( c e. RR -> c e. RR* )
39 elico2 
 |-  ( ( x e. RR /\ c e. RR* ) -> ( x e. ( x [,) c ) <-> ( x e. RR /\ x <_ x /\ x < c ) ) )
40 38 39 sylan2 
 |-  ( ( x e. RR /\ c e. RR ) -> ( x e. ( x [,) c ) <-> ( x e. RR /\ x <_ x /\ x < c ) ) )
41 df-3an 
 |-  ( ( x e. RR /\ x <_ x /\ x < c ) <-> ( ( x e. RR /\ x <_ x ) /\ x < c ) )
42 40 41 bitrdi 
 |-  ( ( x e. RR /\ c e. RR ) -> ( x e. ( x [,) c ) <-> ( ( x e. RR /\ x <_ x ) /\ x < c ) ) )
43 42 baibd 
 |-  ( ( ( x e. RR /\ c e. RR ) /\ ( x e. RR /\ x <_ x ) ) -> ( x e. ( x [,) c ) <-> x < c ) )
44 37 43 mpdan 
 |-  ( ( x e. RR /\ c e. RR ) -> ( x e. ( x [,) c ) <-> x < c ) )
45 44 biimpar 
 |-  ( ( ( x e. RR /\ c e. RR ) /\ x < c ) -> x e. ( x [,) c ) )
46 45 adantr 
 |-  ( ( ( ( x e. RR /\ c e. RR ) /\ x < c ) /\ i = ( x [,) c ) ) -> x e. ( x [,) c ) )
47 eleq2 
 |-  ( i = ( x [,) c ) -> ( x e. i <-> x e. ( x [,) c ) ) )
48 47 adantl 
 |-  ( ( ( ( x e. RR /\ c e. RR ) /\ x < c ) /\ i = ( x [,) c ) ) -> ( x e. i <-> x e. ( x [,) c ) ) )
49 46 48 mpbird 
 |-  ( ( ( ( x e. RR /\ c e. RR ) /\ x < c ) /\ i = ( x [,) c ) ) -> x e. i )
50 rexpssxrxp 
 |-  ( RR X. RR ) C_ ( RR* X. RR* )
51 opelxpi 
 |-  ( ( x e. RR /\ c e. RR ) -> <. x , c >. e. ( RR X. RR ) )
52 50 51 sseldi 
 |-  ( ( x e. RR /\ c e. RR ) -> <. x , c >. e. ( RR* X. RR* ) )
53 df-ico 
 |-  [,) = ( x e. RR* , c e. RR* |-> { z e. RR* | ( x <_ z /\ z < c ) } )
54 53 ixxf 
 |-  [,) : ( RR* X. RR* ) --> ~P RR*
55 54 fdmi 
 |-  dom [,) = ( RR* X. RR* )
56 55 eleq2i 
 |-  ( <. x , c >. e. dom [,) <-> <. x , c >. e. ( RR* X. RR* ) )
57 53 mpofun 
 |-  Fun [,)
58 funfvima 
 |-  ( ( Fun [,) /\ <. x , c >. e. dom [,) ) -> ( <. x , c >. e. ( RR X. RR ) -> ( [,) ` <. x , c >. ) e. ( [,) " ( RR X. RR ) ) ) )
59 57 58 mpan 
 |-  ( <. x , c >. e. dom [,) -> ( <. x , c >. e. ( RR X. RR ) -> ( [,) ` <. x , c >. ) e. ( [,) " ( RR X. RR ) ) ) )
60 56 59 sylbir 
 |-  ( <. x , c >. e. ( RR* X. RR* ) -> ( <. x , c >. e. ( RR X. RR ) -> ( [,) ` <. x , c >. ) e. ( [,) " ( RR X. RR ) ) ) )
61 52 51 60 sylc 
 |-  ( ( x e. RR /\ c e. RR ) -> ( [,) ` <. x , c >. ) e. ( [,) " ( RR X. RR ) ) )
62 df-ov 
 |-  ( x [,) c ) = ( [,) ` <. x , c >. )
63 61 62 1 3eltr4g 
 |-  ( ( x e. RR /\ c e. RR ) -> ( x [,) c ) e. I )
64 eleq1 
 |-  ( i = ( x [,) c ) -> ( i e. I <-> ( x [,) c ) e. I ) )
65 63 64 syl5ibrcom 
 |-  ( ( x e. RR /\ c e. RR ) -> ( i = ( x [,) c ) -> i e. I ) )
66 65 imp 
 |-  ( ( ( x e. RR /\ c e. RR ) /\ i = ( x [,) c ) ) -> i e. I )
67 ioof 
 |-  (,) : ( RR* X. RR* ) --> ~P RR
68 ffn 
 |-  ( (,) : ( RR* X. RR* ) --> ~P RR -> (,) Fn ( RR* X. RR* ) )
69 67 68 ax-mp 
 |-  (,) Fn ( RR* X. RR* )
70 ovelrn 
 |-  ( (,) Fn ( RR* X. RR* ) -> ( o e. ran (,) <-> E. a e. RR* E. b e. RR* o = ( a (,) b ) ) )
71 69 70 ax-mp 
 |-  ( o e. ran (,) <-> E. a e. RR* E. b e. RR* o = ( a (,) b ) )
72 iooelexlt 
 |-  ( x e. ( a (,) b ) -> E. y e. ( a (,) b ) y < x )
73 df-rex 
 |-  ( E. y e. ( a (,) b ) y < x <-> E. y ( y e. ( a (,) b ) /\ y < x ) )
74 72 73 sylib 
 |-  ( x e. ( a (,) b ) -> E. y ( y e. ( a (,) b ) /\ y < x ) )
75 simpl 
 |-  ( ( y e. ( a (,) b ) /\ y < x ) -> y e. ( a (,) b ) )
76 75 a1i 
 |-  ( x e. ( a (,) b ) -> ( ( y e. ( a (,) b ) /\ y < x ) -> y e. ( a (,) b ) ) )
77 53 elmpocl2 
 |-  ( y e. ( x [,) c ) -> c e. RR* )
78 elioore 
 |-  ( x e. ( a (,) b ) -> x e. RR )
79 elico2 
 |-  ( ( x e. RR /\ c e. RR* ) -> ( y e. ( x [,) c ) <-> ( y e. RR /\ x <_ y /\ y < c ) ) )
80 78 79 sylan 
 |-  ( ( x e. ( a (,) b ) /\ c e. RR* ) -> ( y e. ( x [,) c ) <-> ( y e. RR /\ x <_ y /\ y < c ) ) )
81 simp2 
 |-  ( ( y e. RR /\ x <_ y /\ y < c ) -> x <_ y )
82 80 81 syl6bi 
 |-  ( ( x e. ( a (,) b ) /\ c e. RR* ) -> ( y e. ( x [,) c ) -> x <_ y ) )
83 82 ex 
 |-  ( x e. ( a (,) b ) -> ( c e. RR* -> ( y e. ( x [,) c ) -> x <_ y ) ) )
84 83 com23 
 |-  ( x e. ( a (,) b ) -> ( y e. ( x [,) c ) -> ( c e. RR* -> x <_ y ) ) )
85 77 84 mpdi 
 |-  ( x e. ( a (,) b ) -> ( y e. ( x [,) c ) -> x <_ y ) )
86 85 imp 
 |-  ( ( x e. ( a (,) b ) /\ y e. ( x [,) c ) ) -> x <_ y )
87 78 rexrd 
 |-  ( x e. ( a (,) b ) -> x e. RR* )
88 87 adantr 
 |-  ( ( x e. ( a (,) b ) /\ y e. ( x [,) c ) ) -> x e. RR* )
89 elicore 
 |-  ( ( x e. RR /\ y e. ( x [,) c ) ) -> y e. RR )
90 78 89 sylan 
 |-  ( ( x e. ( a (,) b ) /\ y e. ( x [,) c ) ) -> y e. RR )
91 90 rexrd 
 |-  ( ( x e. ( a (,) b ) /\ y e. ( x [,) c ) ) -> y e. RR* )
92 xrlenlt 
 |-  ( ( x e. RR* /\ y e. RR* ) -> ( x <_ y <-> -. y < x ) )
93 92 biimpd 
 |-  ( ( x e. RR* /\ y e. RR* ) -> ( x <_ y -> -. y < x ) )
94 93 con2d 
 |-  ( ( x e. RR* /\ y e. RR* ) -> ( y < x -> -. x <_ y ) )
95 88 91 94 syl2anc 
 |-  ( ( x e. ( a (,) b ) /\ y e. ( x [,) c ) ) -> ( y < x -> -. x <_ y ) )
96 86 95 mt2d 
 |-  ( ( x e. ( a (,) b ) /\ y e. ( x [,) c ) ) -> -. y < x )
97 96 intnand 
 |-  ( ( x e. ( a (,) b ) /\ y e. ( x [,) c ) ) -> -. ( y e. ( a (,) b ) /\ y < x ) )
98 97 ex 
 |-  ( x e. ( a (,) b ) -> ( y e. ( x [,) c ) -> -. ( y e. ( a (,) b ) /\ y < x ) ) )
99 98 con2d 
 |-  ( x e. ( a (,) b ) -> ( ( y e. ( a (,) b ) /\ y < x ) -> -. y e. ( x [,) c ) ) )
100 76 99 jcad 
 |-  ( x e. ( a (,) b ) -> ( ( y e. ( a (,) b ) /\ y < x ) -> ( y e. ( a (,) b ) /\ -. y e. ( x [,) c ) ) ) )
101 annim 
 |-  ( ( y e. ( a (,) b ) /\ -. y e. ( x [,) c ) ) <-> -. ( y e. ( a (,) b ) -> y e. ( x [,) c ) ) )
102 100 101 syl6ib 
 |-  ( x e. ( a (,) b ) -> ( ( y e. ( a (,) b ) /\ y < x ) -> -. ( y e. ( a (,) b ) -> y e. ( x [,) c ) ) ) )
103 102 eximdv 
 |-  ( x e. ( a (,) b ) -> ( E. y ( y e. ( a (,) b ) /\ y < x ) -> E. y -. ( y e. ( a (,) b ) -> y e. ( x [,) c ) ) ) )
104 74 103 mpd 
 |-  ( x e. ( a (,) b ) -> E. y -. ( y e. ( a (,) b ) -> y e. ( x [,) c ) ) )
105 exnal 
 |-  ( E. y -. ( y e. ( a (,) b ) -> y e. ( x [,) c ) ) <-> -. A. y ( y e. ( a (,) b ) -> y e. ( x [,) c ) ) )
106 104 105 sylib 
 |-  ( x e. ( a (,) b ) -> -. A. y ( y e. ( a (,) b ) -> y e. ( x [,) c ) ) )
107 dfss2 
 |-  ( ( a (,) b ) C_ ( x [,) c ) <-> A. y ( y e. ( a (,) b ) -> y e. ( x [,) c ) ) )
108 106 107 sylnibr 
 |-  ( x e. ( a (,) b ) -> -. ( a (,) b ) C_ ( x [,) c ) )
109 imnan 
 |-  ( ( x e. ( a (,) b ) -> -. ( a (,) b ) C_ ( x [,) c ) ) <-> -. ( x e. ( a (,) b ) /\ ( a (,) b ) C_ ( x [,) c ) ) )
110 108 109 mpbi 
 |-  -. ( x e. ( a (,) b ) /\ ( a (,) b ) C_ ( x [,) c ) )
111 eleq2 
 |-  ( o = ( a (,) b ) -> ( x e. o <-> x e. ( a (,) b ) ) )
112 sseq1 
 |-  ( o = ( a (,) b ) -> ( o C_ ( x [,) c ) <-> ( a (,) b ) C_ ( x [,) c ) ) )
113 111 112 anbi12d 
 |-  ( o = ( a (,) b ) -> ( ( x e. o /\ o C_ ( x [,) c ) ) <-> ( x e. ( a (,) b ) /\ ( a (,) b ) C_ ( x [,) c ) ) ) )
114 110 113 mtbiri 
 |-  ( o = ( a (,) b ) -> -. ( x e. o /\ o C_ ( x [,) c ) ) )
115 sseq2 
 |-  ( i = ( x [,) c ) -> ( o C_ i <-> o C_ ( x [,) c ) ) )
116 115 anbi2d 
 |-  ( i = ( x [,) c ) -> ( ( x e. o /\ o C_ i ) <-> ( x e. o /\ o C_ ( x [,) c ) ) ) )
117 116 notbid 
 |-  ( i = ( x [,) c ) -> ( -. ( x e. o /\ o C_ i ) <-> -. ( x e. o /\ o C_ ( x [,) c ) ) ) )
118 114 117 syl5ibrcom 
 |-  ( o = ( a (,) b ) -> ( i = ( x [,) c ) -> -. ( x e. o /\ o C_ i ) ) )
119 118 a1i 
 |-  ( ( a e. RR* /\ b e. RR* ) -> ( o = ( a (,) b ) -> ( i = ( x [,) c ) -> -. ( x e. o /\ o C_ i ) ) ) )
120 119 rexlimivv 
 |-  ( E. a e. RR* E. b e. RR* o = ( a (,) b ) -> ( i = ( x [,) c ) -> -. ( x e. o /\ o C_ i ) ) )
121 71 120 sylbi 
 |-  ( o e. ran (,) -> ( i = ( x [,) c ) -> -. ( x e. o /\ o C_ i ) ) )
122 121 com12 
 |-  ( i = ( x [,) c ) -> ( o e. ran (,) -> -. ( x e. o /\ o C_ i ) ) )
123 122 ralrimiv 
 |-  ( i = ( x [,) c ) -> A. o e. ran (,) -. ( x e. o /\ o C_ i ) )
124 ralnex 
 |-  ( A. o e. ran (,) -. ( x e. o /\ o C_ i ) <-> -. E. o e. ran (,) ( x e. o /\ o C_ i ) )
125 123 124 sylib 
 |-  ( i = ( x [,) c ) -> -. E. o e. ran (,) ( x e. o /\ o C_ i ) )
126 125 adantl 
 |-  ( ( ( x e. RR /\ c e. RR ) /\ i = ( x [,) c ) ) -> -. E. o e. ran (,) ( x e. o /\ o C_ i ) )
127 66 126 jca 
 |-  ( ( ( x e. RR /\ c e. RR ) /\ i = ( x [,) c ) ) -> ( i e. I /\ -. E. o e. ran (,) ( x e. o /\ o C_ i ) ) )
128 127 adantlr 
 |-  ( ( ( ( x e. RR /\ c e. RR ) /\ x < c ) /\ i = ( x [,) c ) ) -> ( i e. I /\ -. E. o e. ran (,) ( x e. o /\ o C_ i ) ) )
129 49 128 jca 
 |-  ( ( ( ( x e. RR /\ c e. RR ) /\ x < c ) /\ i = ( x [,) c ) ) -> ( x e. i /\ ( i e. I /\ -. E. o e. ran (,) ( x e. o /\ o C_ i ) ) ) )
130 an12 
 |-  ( ( x e. i /\ ( i e. I /\ -. E. o e. ran (,) ( x e. o /\ o C_ i ) ) ) <-> ( i e. I /\ ( x e. i /\ -. E. o e. ran (,) ( x e. o /\ o C_ i ) ) ) )
131 annim 
 |-  ( ( x e. i /\ -. E. o e. ran (,) ( x e. o /\ o C_ i ) ) <-> -. ( x e. i -> E. o e. ran (,) ( x e. o /\ o C_ i ) ) )
132 131 anbi2i 
 |-  ( ( i e. I /\ ( x e. i /\ -. E. o e. ran (,) ( x e. o /\ o C_ i ) ) ) <-> ( i e. I /\ -. ( x e. i -> E. o e. ran (,) ( x e. o /\ o C_ i ) ) ) )
133 130 132 bitri 
 |-  ( ( x e. i /\ ( i e. I /\ -. E. o e. ran (,) ( x e. o /\ o C_ i ) ) ) <-> ( i e. I /\ -. ( x e. i -> E. o e. ran (,) ( x e. o /\ o C_ i ) ) ) )
134 129 133 sylib 
 |-  ( ( ( ( x e. RR /\ c e. RR ) /\ x < c ) /\ i = ( x [,) c ) ) -> ( i e. I /\ -. ( x e. i -> E. o e. ran (,) ( x e. o /\ o C_ i ) ) ) )
135 rspe 
 |-  ( ( i e. I /\ -. ( x e. i -> E. o e. ran (,) ( x e. o /\ o C_ i ) ) ) -> E. i e. I -. ( x e. i -> E. o e. ran (,) ( x e. o /\ o C_ i ) ) )
136 134 135 syl 
 |-  ( ( ( ( x e. RR /\ c e. RR ) /\ x < c ) /\ i = ( x [,) c ) ) -> E. i e. I -. ( x e. i -> E. o e. ran (,) ( x e. o /\ o C_ i ) ) )
137 rexnal 
 |-  ( E. i e. I -. ( x e. i -> E. o e. ran (,) ( x e. o /\ o C_ i ) ) <-> -. A. i e. I ( x e. i -> E. o e. ran (,) ( x e. o /\ o C_ i ) ) )
138 136 137 sylib 
 |-  ( ( ( ( x e. RR /\ c e. RR ) /\ x < c ) /\ i = ( x [,) c ) ) -> -. A. i e. I ( x e. i -> E. o e. ran (,) ( x e. o /\ o C_ i ) ) )
139 138 exp41 
 |-  ( x e. RR -> ( c e. RR -> ( x < c -> ( i = ( x [,) c ) -> -. A. i e. I ( x e. i -> E. o e. ran (,) ( x e. o /\ o C_ i ) ) ) ) ) )
140 139 com4l 
 |-  ( c e. RR -> ( x < c -> ( i = ( x [,) c ) -> ( x e. RR -> -. A. i e. I ( x e. i -> E. o e. ran (,) ( x e. o /\ o C_ i ) ) ) ) ) )
141 140 imp41 
 |-  ( ( ( ( c e. RR /\ x < c ) /\ i = ( x [,) c ) ) /\ x e. RR ) -> -. A. i e. I ( x e. i -> E. o e. ran (,) ( x e. o /\ o C_ i ) ) )
142 rspe 
 |-  ( ( x e. RR /\ -. A. i e. I ( x e. i -> E. o e. ran (,) ( x e. o /\ o C_ i ) ) ) -> E. x e. RR -. A. i e. I ( x e. i -> E. o e. ran (,) ( x e. o /\ o C_ i ) ) )
143 34 141 142 syl2anc 
 |-  ( ( ( ( c e. RR /\ x < c ) /\ i = ( x [,) c ) ) /\ x e. RR ) -> E. x e. RR -. A. i e. I ( x e. i -> E. o e. ran (,) ( x e. o /\ o C_ i ) ) )
144 rexnal 
 |-  ( E. x e. RR -. A. i e. I ( x e. i -> E. o e. ran (,) ( x e. o /\ o C_ i ) ) <-> -. A. x e. RR A. i e. I ( x e. i -> E. o e. ran (,) ( x e. o /\ o C_ i ) ) )
145 143 144 sylib 
 |-  ( ( ( ( c e. RR /\ x < c ) /\ i = ( x [,) c ) ) /\ x e. RR ) -> -. A. x e. RR A. i e. I ( x e. i -> E. o e. ran (,) ( x e. o /\ o C_ i ) ) )
146 df-ico 
 |-  [,) = ( m e. RR* , n e. RR* |-> { z e. RR* | ( m <_ z /\ z < n ) } )
147 146 ixxex 
 |-  [,) e. _V
148 imaexg 
 |-  ( [,) e. _V -> ( [,) " ( RR X. RR ) ) e. _V )
149 147 148 ax-mp 
 |-  ( [,) " ( RR X. RR ) ) e. _V
150 1 149 eqeltri 
 |-  I e. _V
151 1 icoreunrn 
 |-  RR = U. I
152 unirnioo 
 |-  RR = U. ran (,)
153 151 152 eqtr3i 
 |-  U. I = U. ran (,)
154 tgss2 
 |-  ( ( I e. _V /\ U. I = U. ran (,) ) -> ( ( topGen ` I ) C_ ( topGen ` ran (,) ) <-> A. x e. U. I A. i e. I ( x e. i -> E. o e. ran (,) ( x e. o /\ o C_ i ) ) ) )
155 150 153 154 mp2an 
 |-  ( ( topGen ` I ) C_ ( topGen ` ran (,) ) <-> A. x e. U. I A. i e. I ( x e. i -> E. o e. ran (,) ( x e. o /\ o C_ i ) ) )
156 151 raleqi 
 |-  ( A. x e. RR A. i e. I ( x e. i -> E. o e. ran (,) ( x e. o /\ o C_ i ) ) <-> A. x e. U. I A. i e. I ( x e. i -> E. o e. ran (,) ( x e. o /\ o C_ i ) ) )
157 155 156 bitr4i 
 |-  ( ( topGen ` I ) C_ ( topGen ` ran (,) ) <-> A. x e. RR A. i e. I ( x e. i -> E. o e. ran (,) ( x e. o /\ o C_ i ) ) )
158 145 157 sylnibr 
 |-  ( ( ( ( c e. RR /\ x < c ) /\ i = ( x [,) c ) ) /\ x e. RR ) -> -. ( topGen ` I ) C_ ( topGen ` ran (,) ) )
159 158 sbcth 
 |-  ( 1 e. RR -> [. 1 / x ]. ( ( ( ( c e. RR /\ x < c ) /\ i = ( x [,) c ) ) /\ x e. RR ) -> -. ( topGen ` I ) C_ ( topGen ` ran (,) ) ) )
160 7 159 ax-mp 
 |-  [. 1 / x ]. ( ( ( ( c e. RR /\ x < c ) /\ i = ( x [,) c ) ) /\ x e. RR ) -> -. ( topGen ` I ) C_ ( topGen ` ran (,) ) )
161 sbcimg 
 |-  ( 1 e. RR -> ( [. 1 / x ]. ( ( ( ( c e. RR /\ x < c ) /\ i = ( x [,) c ) ) /\ x e. RR ) -> -. ( topGen ` I ) C_ ( topGen ` ran (,) ) ) <-> ( [. 1 / x ]. ( ( ( c e. RR /\ x < c ) /\ i = ( x [,) c ) ) /\ x e. RR ) -> [. 1 / x ]. -. ( topGen ` I ) C_ ( topGen ` ran (,) ) ) ) )
162 7 161 ax-mp 
 |-  ( [. 1 / x ]. ( ( ( ( c e. RR /\ x < c ) /\ i = ( x [,) c ) ) /\ x e. RR ) -> -. ( topGen ` I ) C_ ( topGen ` ran (,) ) ) <-> ( [. 1 / x ]. ( ( ( c e. RR /\ x < c ) /\ i = ( x [,) c ) ) /\ x e. RR ) -> [. 1 / x ]. -. ( topGen ` I ) C_ ( topGen ` ran (,) ) ) )
163 160 162 mpbi 
 |-  ( [. 1 / x ]. ( ( ( c e. RR /\ x < c ) /\ i = ( x [,) c ) ) /\ x e. RR ) -> [. 1 / x ]. -. ( topGen ` I ) C_ ( topGen ` ran (,) ) )
164 sbcel1v 
 |-  ( [. 1 / x ]. x e. RR <-> 1 e. RR )
165 7 164 mpbir 
 |-  [. 1 / x ]. x e. RR
166 sbcan 
 |-  ( [. 1 / x ]. ( ( ( c e. RR /\ x < c ) /\ i = ( x [,) c ) ) /\ x e. RR ) <-> ( [. 1 / x ]. ( ( c e. RR /\ x < c ) /\ i = ( x [,) c ) ) /\ [. 1 / x ]. x e. RR ) )
167 165 166 mpbiran2 
 |-  ( [. 1 / x ]. ( ( ( c e. RR /\ x < c ) /\ i = ( x [,) c ) ) /\ x e. RR ) <-> [. 1 / x ]. ( ( c e. RR /\ x < c ) /\ i = ( x [,) c ) ) )
168 sbcg 
 |-  ( 1 e. RR -> ( [. 1 / x ]. -. ( topGen ` I ) C_ ( topGen ` ran (,) ) <-> -. ( topGen ` I ) C_ ( topGen ` ran (,) ) ) )
169 7 168 ax-mp 
 |-  ( [. 1 / x ]. -. ( topGen ` I ) C_ ( topGen ` ran (,) ) <-> -. ( topGen ` I ) C_ ( topGen ` ran (,) ) )
170 163 167 169 3imtr3i 
 |-  ( [. 1 / x ]. ( ( c e. RR /\ x < c ) /\ i = ( x [,) c ) ) -> -. ( topGen ` I ) C_ ( topGen ` ran (,) ) )
171 33 170 sylbir 
 |-  ( ( [. 1 / x ]. ( c e. RR /\ x < c ) /\ [. 1 / x ]. i = ( x [,) c ) ) -> -. ( topGen ` I ) C_ ( topGen ` ran (,) ) )
172 21 32 171 syl2anbr 
 |-  ( ( ( c e. RR /\ 1 < c ) /\ i = ( 1 [,) c ) ) -> -. ( topGen ` I ) C_ ( topGen ` ran (,) ) )
173 172 sbcth 
 |-  ( ( 1 [,) c ) e. _V -> [. ( 1 [,) c ) / i ]. ( ( ( c e. RR /\ 1 < c ) /\ i = ( 1 [,) c ) ) -> -. ( topGen ` I ) C_ ( topGen ` ran (,) ) ) )
174 5 173 ax-mp 
 |-  [. ( 1 [,) c ) / i ]. ( ( ( c e. RR /\ 1 < c ) /\ i = ( 1 [,) c ) ) -> -. ( topGen ` I ) C_ ( topGen ` ran (,) ) )
175 sbcimg 
 |-  ( ( 1 [,) c ) e. _V -> ( [. ( 1 [,) c ) / i ]. ( ( ( c e. RR /\ 1 < c ) /\ i = ( 1 [,) c ) ) -> -. ( topGen ` I ) C_ ( topGen ` ran (,) ) ) <-> ( [. ( 1 [,) c ) / i ]. ( ( c e. RR /\ 1 < c ) /\ i = ( 1 [,) c ) ) -> [. ( 1 [,) c ) / i ]. -. ( topGen ` I ) C_ ( topGen ` ran (,) ) ) ) )
176 5 175 ax-mp 
 |-  ( [. ( 1 [,) c ) / i ]. ( ( ( c e. RR /\ 1 < c ) /\ i = ( 1 [,) c ) ) -> -. ( topGen ` I ) C_ ( topGen ` ran (,) ) ) <-> ( [. ( 1 [,) c ) / i ]. ( ( c e. RR /\ 1 < c ) /\ i = ( 1 [,) c ) ) -> [. ( 1 [,) c ) / i ]. -. ( topGen ` I ) C_ ( topGen ` ran (,) ) ) )
177 174 176 mpbi 
 |-  ( [. ( 1 [,) c ) / i ]. ( ( c e. RR /\ 1 < c ) /\ i = ( 1 [,) c ) ) -> [. ( 1 [,) c ) / i ]. -. ( topGen ` I ) C_ ( topGen ` ran (,) ) )
178 sbcan 
 |-  ( [. ( 1 [,) c ) / i ]. ( ( c e. RR /\ 1 < c ) /\ i = ( 1 [,) c ) ) <-> ( [. ( 1 [,) c ) / i ]. ( c e. RR /\ 1 < c ) /\ [. ( 1 [,) c ) / i ]. i = ( 1 [,) c ) ) )
179 eqid 
 |-  ( 1 [,) c ) = ( 1 [,) c )
180 eqsbc3 
 |-  ( ( 1 [,) c ) e. _V -> ( [. ( 1 [,) c ) / i ]. i = ( 1 [,) c ) <-> ( 1 [,) c ) = ( 1 [,) c ) ) )
181 5 180 ax-mp 
 |-  ( [. ( 1 [,) c ) / i ]. i = ( 1 [,) c ) <-> ( 1 [,) c ) = ( 1 [,) c ) )
182 179 181 mpbir 
 |-  [. ( 1 [,) c ) / i ]. i = ( 1 [,) c )
183 sbcg 
 |-  ( ( 1 [,) c ) e. _V -> ( [. ( 1 [,) c ) / i ]. ( c e. RR /\ 1 < c ) <-> ( c e. RR /\ 1 < c ) ) )
184 5 183 ax-mp 
 |-  ( [. ( 1 [,) c ) / i ]. ( c e. RR /\ 1 < c ) <-> ( c e. RR /\ 1 < c ) )
185 184 anbi1i 
 |-  ( ( [. ( 1 [,) c ) / i ]. ( c e. RR /\ 1 < c ) /\ [. ( 1 [,) c ) / i ]. i = ( 1 [,) c ) ) <-> ( ( c e. RR /\ 1 < c ) /\ [. ( 1 [,) c ) / i ]. i = ( 1 [,) c ) ) )
186 182 185 mpbiran2 
 |-  ( ( [. ( 1 [,) c ) / i ]. ( c e. RR /\ 1 < c ) /\ [. ( 1 [,) c ) / i ]. i = ( 1 [,) c ) ) <-> ( c e. RR /\ 1 < c ) )
187 178 186 bitri 
 |-  ( [. ( 1 [,) c ) / i ]. ( ( c e. RR /\ 1 < c ) /\ i = ( 1 [,) c ) ) <-> ( c e. RR /\ 1 < c ) )
188 sbcg 
 |-  ( ( 1 [,) c ) e. _V -> ( [. ( 1 [,) c ) / i ]. -. ( topGen ` I ) C_ ( topGen ` ran (,) ) <-> -. ( topGen ` I ) C_ ( topGen ` ran (,) ) ) )
189 5 188 ax-mp 
 |-  ( [. ( 1 [,) c ) / i ]. -. ( topGen ` I ) C_ ( topGen ` ran (,) ) <-> -. ( topGen ` I ) C_ ( topGen ` ran (,) ) )
190 177 187 189 3imtr3i 
 |-  ( ( c e. RR /\ 1 < c ) -> -. ( topGen ` I ) C_ ( topGen ` ran (,) ) )
191 190 sbcth 
 |-  ( 2 e. RR -> [. 2 / c ]. ( ( c e. RR /\ 1 < c ) -> -. ( topGen ` I ) C_ ( topGen ` ran (,) ) ) )
192 3 191 ax-mp 
 |-  [. 2 / c ]. ( ( c e. RR /\ 1 < c ) -> -. ( topGen ` I ) C_ ( topGen ` ran (,) ) )
193 sbcimg 
 |-  ( 2 e. RR -> ( [. 2 / c ]. ( ( c e. RR /\ 1 < c ) -> -. ( topGen ` I ) C_ ( topGen ` ran (,) ) ) <-> ( [. 2 / c ]. ( c e. RR /\ 1 < c ) -> [. 2 / c ]. -. ( topGen ` I ) C_ ( topGen ` ran (,) ) ) ) )
194 3 193 ax-mp 
 |-  ( [. 2 / c ]. ( ( c e. RR /\ 1 < c ) -> -. ( topGen ` I ) C_ ( topGen ` ran (,) ) ) <-> ( [. 2 / c ]. ( c e. RR /\ 1 < c ) -> [. 2 / c ]. -. ( topGen ` I ) C_ ( topGen ` ran (,) ) ) )
195 192 194 mpbi 
 |-  ( [. 2 / c ]. ( c e. RR /\ 1 < c ) -> [. 2 / c ]. -. ( topGen ` I ) C_ ( topGen ` ran (,) ) )
196 sbcan 
 |-  ( [. 2 / c ]. ( c e. RR /\ 1 < c ) <-> ( [. 2 / c ]. c e. RR /\ [. 2 / c ]. 1 < c ) )
197 sbcel1v 
 |-  ( [. 2 / c ]. c e. RR <-> 2 e. RR )
198 sbcbr123 
 |-  ( [. 2 / c ]. 1 < c <-> [_ 2 / c ]_ 1 [_ 2 / c ]_ < [_ 2 / c ]_ c )
199 csbconstg 
 |-  ( 2 e. RR -> [_ 2 / c ]_ 1 = 1 )
200 3 199 ax-mp 
 |-  [_ 2 / c ]_ 1 = 1
201 csbvarg 
 |-  ( 2 e. RR -> [_ 2 / c ]_ c = 2 )
202 3 201 ax-mp 
 |-  [_ 2 / c ]_ c = 2
203 200 202 breq12i 
 |-  ( [_ 2 / c ]_ 1 [_ 2 / c ]_ < [_ 2 / c ]_ c <-> 1 [_ 2 / c ]_ < 2 )
204 csbconstg 
 |-  ( 2 e. RR -> [_ 2 / c ]_ < = < )
205 3 204 ax-mp 
 |-  [_ 2 / c ]_ < = <
206 205 breqi 
 |-  ( 1 [_ 2 / c ]_ < 2 <-> 1 < 2 )
207 198 203 206 3bitri 
 |-  ( [. 2 / c ]. 1 < c <-> 1 < 2 )
208 197 207 anbi12i 
 |-  ( ( [. 2 / c ]. c e. RR /\ [. 2 / c ]. 1 < c ) <-> ( 2 e. RR /\ 1 < 2 ) )
209 196 208 bitri 
 |-  ( [. 2 / c ]. ( c e. RR /\ 1 < c ) <-> ( 2 e. RR /\ 1 < 2 ) )
210 sbcg 
 |-  ( 2 e. RR -> ( [. 2 / c ]. -. ( topGen ` I ) C_ ( topGen ` ran (,) ) <-> -. ( topGen ` I ) C_ ( topGen ` ran (,) ) ) )
211 3 210 ax-mp 
 |-  ( [. 2 / c ]. -. ( topGen ` I ) C_ ( topGen ` ran (,) ) <-> -. ( topGen ` I ) C_ ( topGen ` ran (,) ) )
212 195 209 211 3imtr3i 
 |-  ( ( 2 e. RR /\ 1 < 2 ) -> -. ( topGen ` I ) C_ ( topGen ` ran (,) ) )
213 3 4 212 mp2an 
 |-  -. ( topGen ` I ) C_ ( topGen ` ran (,) )
214 eqimss 
 |-  ( ( topGen ` I ) = ( topGen ` ran (,) ) -> ( topGen ` I ) C_ ( topGen ` ran (,) ) )
215 213 214 mto 
 |-  -. ( topGen ` I ) = ( topGen ` ran (,) )
216 215 nesymir 
 |-  ( topGen ` ran (,) ) =/= ( topGen ` I )
217 df-pss 
 |-  ( ( topGen ` ran (,) ) C. ( topGen ` I ) <-> ( ( topGen ` ran (,) ) C_ ( topGen ` I ) /\ ( topGen ` ran (,) ) =/= ( topGen ` I ) ) )
218 2 216 217 mpbir2an 
 |-  ( topGen ` ran (,) ) C. ( topGen ` I )