Users' Mathboxes Mathbox for ML < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  relowlpssretop Structured version   Visualization version   Unicode version

Theorem relowlpssretop 31813
Description: The lower limit topology on the reals is strictly finer than the standard topology. (Contributed by ML, 2-Aug-2020.)
Hypothesis
Ref Expression
relowlpssretop.1  |-  I  =  ( [,) " ( RR  X.  RR ) )
Assertion
Ref Expression
relowlpssretop  |-  ( topGen ` 
ran  (,) )  C.  ( topGen `
 I )

Proof of Theorem relowlpssretop
Dummy variables  a 
b  c  i  o  x  m  n  z  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 relowlpssretop.1 . . 3  |-  I  =  ( [,) " ( RR  X.  RR ) )
21relowlssretop 31812 . 2  |-  ( topGen ` 
ran  (,) )  C_  ( topGen `
 I )
3 2re 10712 . . . . 5  |-  2  e.  RR
4 1lt2 10810 . . . . 5  |-  1  <  2
5 ovex 6348 . . . . . . . . . . . 12  |-  ( 1 [,) c )  e. 
_V
6 sbcan 3322 . . . . . . . . . . . . . . 15  |-  ( [.
1  /  x ]. ( c  e.  RR  /\  x  <  c )  <-> 
( [. 1  /  x ]. c  e.  RR  /\ 
[. 1  /  x ]. x  <  c ) )
7 1re 9673 . . . . . . . . . . . . . . . . 17  |-  1  e.  RR
8 sbcg 3345 . . . . . . . . . . . . . . . . 17  |-  ( 1  e.  RR  ->  ( [. 1  /  x ]. c  e.  RR  <->  c  e.  RR ) )
97, 8ax-mp 5 . . . . . . . . . . . . . . . 16  |-  ( [.
1  /  x ]. c  e.  RR  <->  c  e.  RR )
10 sbcbr123 4470 . . . . . . . . . . . . . . . . 17  |-  ( [.
1  /  x ]. x  <  c  <->  [_ 1  /  x ]_ x [_
1  /  x ]_  <  [_ 1  /  x ]_ c )
11 csbvarg 3804 . . . . . . . . . . . . . . . . . . 19  |-  ( 1  e.  RR  ->  [_ 1  /  x ]_ x  =  1 )
127, 11ax-mp 5 . . . . . . . . . . . . . . . . . 18  |-  [_ 1  /  x ]_ x  =  1
13 csbconstg 3388 . . . . . . . . . . . . . . . . . . 19  |-  ( 1  e.  RR  ->  [_ 1  /  x ]_ c  =  c )
147, 13ax-mp 5 . . . . . . . . . . . . . . . . . 18  |-  [_ 1  /  x ]_ c  =  c
1512, 14breq12i 4427 . . . . . . . . . . . . . . . . 17  |-  ( [_
1  /  x ]_ x [_ 1  /  x ]_  <  [_ 1  /  x ]_ c  <->  1 [_ 1  /  x ]_  <  c
)
16 csbconstg 3388 . . . . . . . . . . . . . . . . . . 19  |-  ( 1  e.  RR  ->  [_ 1  /  x ]_  <  =  <  )
177, 16ax-mp 5 . . . . . . . . . . . . . . . . . 18  |-  [_ 1  /  x ]_  <  =  <
1817breqi 4424 . . . . . . . . . . . . . . . . 17  |-  ( 1
[_ 1  /  x ]_  <  c  <->  1  <  c )
1910, 15, 183bitri 279 . . . . . . . . . . . . . . . 16  |-  ( [.
1  /  x ]. x  <  c  <->  1  <  c )
209, 19anbi12i 708 . . . . . . . . . . . . . . 15  |-  ( (
[. 1  /  x ]. c  e.  RR  /\ 
[. 1  /  x ]. x  <  c )  <-> 
( c  e.  RR  /\  1  <  c ) )
216, 20bitri 257 . . . . . . . . . . . . . 14  |-  ( [.
1  /  x ]. ( c  e.  RR  /\  x  <  c )  <-> 
( c  e.  RR  /\  1  <  c ) )
22 sbceqg 3785 . . . . . . . . . . . . . . . 16  |-  ( 1  e.  RR  ->  ( [. 1  /  x ]. i  =  (
x [,) c )  <->  [_ 1  /  x ]_ i  =  [_ 1  /  x ]_ ( x [,) c ) ) )
237, 22ax-mp 5 . . . . . . . . . . . . . . 15  |-  ( [.
1  /  x ]. i  =  ( x [,) c )  <->  [_ 1  /  x ]_ i  = 
[_ 1  /  x ]_ ( x [,) c
) )
24 csbconstg 3388 . . . . . . . . . . . . . . . . 17  |-  ( 1  e.  RR  ->  [_ 1  /  x ]_ i  =  i )
257, 24ax-mp 5 . . . . . . . . . . . . . . . 16  |-  [_ 1  /  x ]_ i  =  i
26 csbov123 6354 . . . . . . . . . . . . . . . . 17  |-  [_ 1  /  x ]_ ( x [,) c )  =  ( [_ 1  /  x ]_ x [_ 1  /  x ]_ [,) [_ 1  /  x ]_ c )
27 csbconstg 3388 . . . . . . . . . . . . . . . . . . 19  |-  ( 1  e.  RR  ->  [_ 1  /  x ]_ [,)  =  [,) )
287, 27ax-mp 5 . . . . . . . . . . . . . . . . . 18  |-  [_ 1  /  x ]_ [,)  =  [,)
2912, 14, 28oveq123i 6334 . . . . . . . . . . . . . . . . 17  |-  ( [_
1  /  x ]_ x [_ 1  /  x ]_ [,) [_ 1  /  x ]_ c )  =  ( 1 [,) c
)
3026, 29eqtri 2484 . . . . . . . . . . . . . . . 16  |-  [_ 1  /  x ]_ ( x [,) c )  =  ( 1 [,) c
)
3125, 30eqeq12i 2476 . . . . . . . . . . . . . . 15  |-  ( [_
1  /  x ]_ i  =  [_ 1  /  x ]_ ( x [,) c )  <->  i  =  ( 1 [,) c
) )
3223, 31bitri 257 . . . . . . . . . . . . . 14  |-  ( [.
1  /  x ]. i  =  ( x [,) c )  <->  i  =  ( 1 [,) c
) )
33 sbcan 3322 . . . . . . . . . . . . . . 15  |-  ( [.
1  /  x ]. ( ( c  e.  RR  /\  x  < 
c )  /\  i  =  ( x [,) c ) )  <->  ( [.
1  /  x ]. ( c  e.  RR  /\  x  <  c )  /\  [. 1  /  x ]. i  =  ( x [,) c ) ) )
34 simpr 467 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( c  e.  RR  /\  x  < 
c )  /\  i  =  ( x [,) c ) )  /\  x  e.  RR )  ->  x  e.  RR )
35 simpl 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( x  e.  RR  /\  c  e.  RR )  ->  x  e.  RR )
36 leid 9760 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( x  e.  RR  ->  x  <_  x )
3735, 36jccir 546 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( x  e.  RR  /\  c  e.  RR )  ->  ( x  e.  RR  /\  x  <_  x )
)
38 rexr 9717 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( c  e.  RR  ->  c  e.  RR* )
39 elico2 11732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( x  e.  RR  /\  c  e.  RR* )  -> 
( x  e.  ( x [,) c )  <-> 
( x  e.  RR  /\  x  <_  x  /\  x  <  c ) ) )
4038, 39sylan2 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( x  e.  RR  /\  c  e.  RR )  ->  ( x  e.  ( x [,) c )  <-> 
( x  e.  RR  /\  x  <_  x  /\  x  <  c ) ) )
41 df-3an 993 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( x  e.  RR  /\  x  <_  x  /\  x  <  c )  <->  ( (
x  e.  RR  /\  x  <_  x )  /\  x  <  c ) )
4240, 41syl6bb 269 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( x  e.  RR  /\  c  e.  RR )  ->  ( x  e.  ( x [,) c )  <-> 
( ( x  e.  RR  /\  x  <_  x )  /\  x  <  c ) ) )
4342baibd 925 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( x  e.  RR  /\  c  e.  RR )  /\  ( x  e.  RR  /\  x  <_  x ) )  -> 
( x  e.  ( x [,) c )  <-> 
x  <  c )
)
4437, 43mpdan 679 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( x  e.  RR  /\  c  e.  RR )  ->  ( x  e.  ( x [,) c )  <-> 
x  <  c )
)
4544biimpar 492 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( x  e.  RR  /\  c  e.  RR )  /\  x  <  c
)  ->  x  e.  ( x [,) c
) )
4645adantr 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( x  e.  RR  /\  c  e.  RR )  /\  x  <  c )  /\  i  =  ( x [,) c ) )  ->  x  e.  ( x [,) c ) )
47 eleq2 2529 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( i  =  ( x [,) c )  ->  (
x  e.  i  <->  x  e.  ( x [,) c
) ) )
4847adantl 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( x  e.  RR  /\  c  e.  RR )  /\  x  <  c )  /\  i  =  ( x [,) c ) )  -> 
( x  e.  i  <-> 
x  e.  ( x [,) c ) ) )
4946, 48mpbird 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( x  e.  RR  /\  c  e.  RR )  /\  x  <  c )  /\  i  =  ( x [,) c ) )  ->  x  e.  i )
50 rexpssxrxp 9716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( RR 
X.  RR )  C_  ( RR*  X.  RR* )
51 opelxpi 4888 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( x  e.  RR  /\  c  e.  RR )  -> 
<. x ,  c >.  e.  ( RR  X.  RR ) )
5250, 51sseldi 3442 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( x  e.  RR  /\  c  e.  RR )  -> 
<. x ,  c >.  e.  ( RR*  X.  RR* )
)
53 df-ico 11675 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  [,)  =  ( x  e.  RR* ,  c  e.  RR*  |->  { z  e.  RR*  |  (
x  <_  z  /\  z  <  c ) } )
5453ixxf 11679 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  [,) :
( RR*  X.  RR* ) --> ~P RR*
5554fdmi 5761 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  dom  [,)  =  ( RR*  X.  RR* )
5655eleq2i 2532 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( <.
x ,  c >.  e.  dom  [,)  <->  <. x ,  c
>.  e.  ( RR*  X.  RR* ) )
5753mpt2fun 6430 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  Fun  [,)
58 funfvima 6170 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( Fun  [,)  /\  <. x ,  c >.  e.  dom  [,) )  ->  ( <. x ,  c >.  e.  ( RR  X.  RR )  ->  ( [,) `  <. x ,  c >. )  e.  ( [,) " ( RR  X.  RR ) ) ) )
5957, 58mpan 681 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( <.
x ,  c >.  e.  dom  [,)  ->  ( <.
x ,  c >.  e.  ( RR  X.  RR )  ->  ( [,) `  <. x ,  c >. )  e.  ( [,) " ( RR  X.  RR ) ) ) )
6056, 59sylbir 218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( <.
x ,  c >.  e.  ( RR*  X.  RR* )  ->  ( <. x ,  c
>.  e.  ( RR  X.  RR )  ->  ( [,) `  <. x ,  c
>. )  e.  ( [,) " ( RR  X.  RR ) ) ) )
6152, 51, 60sylc 62 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( x  e.  RR  /\  c  e.  RR )  ->  ( [,) `  <. x ,  c >. )  e.  ( [,) " ( RR  X.  RR ) ) )
62 df-ov 6323 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( x [,) c )  =  ( [,) `  <. x ,  c >. )
6361, 62, 13eltr4g 2557 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( x  e.  RR  /\  c  e.  RR )  ->  ( x [,) c
)  e.  I )
64 eleq1 2528 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( i  =  ( x [,) c )  ->  (
i  e.  I  <->  ( x [,) c )  e.  I
) )
6563, 64syl5ibrcom 230 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( x  e.  RR  /\  c  e.  RR )  ->  ( i  =  ( x [,) c )  ->  i  e.  I
) )
6665imp 435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( x  e.  RR  /\  c  e.  RR )  /\  i  =  ( x [,) c ) )  ->  i  e.  I )
67 ioof 11766 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  (,) :
( RR*  X.  RR* ) --> ~P RR
68 ffn 5755 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( (,)
: ( RR*  X.  RR* )
--> ~P RR  ->  (,)  Fn  ( RR*  X.  RR* )
)
6967, 68ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  (,)  Fn  ( RR*  X.  RR* )
70 ovelrn 6477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( (,) 
Fn  ( RR*  X.  RR* )  ->  ( o  e. 
ran  (,)  <->  E. a  e.  RR*  E. b  e.  RR*  o  =  ( a (,) b ) ) )
7169, 70ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( o  e.  ran  (,)  <->  E. a  e.  RR*  E. b  e. 
RR*  o  =  ( a (,) b ) )
72 iooelexlt 31811 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( x  e.  ( a (,) b )  ->  E. y  e.  ( a (,) b
) y  <  x
)
73 df-rex 2755 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( E. y  e.  ( a (,) b ) y  <  x  <->  E. y
( y  e.  ( a (,) b )  /\  y  <  x
) )
7472, 73sylib 201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( x  e.  ( a (,) b )  ->  E. y
( y  e.  ( a (,) b )  /\  y  <  x
) )
75 simpl 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( ( y  e.  ( a (,) b )  /\  y  <  x )  -> 
y  e.  ( a (,) b ) )
7675a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( x  e.  ( a (,) b )  ->  (
( y  e.  ( a (,) b )  /\  y  <  x
)  ->  y  e.  ( a (,) b
) ) )
7753elmpt2cl2 6545 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( y  e.  ( x [,) c )  ->  c  e.  RR* )
78 elioore 11700 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57  |-  ( x  e.  ( a (,) b )  ->  x  e.  RR )
79 elico2 11732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57  |-  ( ( x  e.  RR  /\  c  e.  RR* )  -> 
( y  e.  ( x [,) c )  <-> 
( y  e.  RR  /\  x  <_  y  /\  y  <  c ) ) )
8078, 79sylan 478 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56  |-  ( ( x  e.  ( a (,) b )  /\  c  e.  RR* )  -> 
( y  e.  ( x [,) c )  <-> 
( y  e.  RR  /\  x  <_  y  /\  y  <  c ) ) )
81 simp2 1015 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56  |-  ( ( y  e.  RR  /\  x  <_  y  /\  y  <  c )  ->  x  <_  y )
8280, 81syl6bi 236 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55  |-  ( ( x  e.  ( a (,) b )  /\  c  e.  RR* )  -> 
( y  e.  ( x [,) c )  ->  x  <_  y
) )
8382ex 440 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54  |-  ( x  e.  ( a (,) b )  ->  (
c  e.  RR*  ->  ( y  e.  ( x [,) c )  ->  x  <_  y ) ) )
8483com23 81 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( x  e.  ( a (,) b )  ->  (
y  e.  ( x [,) c )  -> 
( c  e.  RR*  ->  x  <_  y )
) )
8577, 84mpdi 43 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( x  e.  ( a (,) b )  ->  (
y  e.  ( x [,) c )  ->  x  <_  y ) )
8685imp 435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( ( x  e.  ( a (,) b )  /\  y  e.  ( x [,) c ) )  ->  x  <_  y )
8778rexrd 9721 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( x  e.  ( a (,) b )  ->  x  e.  RR* )
8887adantr 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( ( x  e.  ( a (,) b )  /\  y  e.  ( x [,) c ) )  ->  x  e.  RR* )
89 elicore 11721 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54  |-  ( ( x  e.  RR  /\  y  e.  ( x [,) c ) )  -> 
y  e.  RR )
9078, 89sylan 478 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( ( x  e.  ( a (,) b )  /\  y  e.  ( x [,) c ) )  -> 
y  e.  RR )
9190rexrd 9721 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( ( x  e.  ( a (,) b )  /\  y  e.  ( x [,) c ) )  -> 
y  e.  RR* )
92 xrlenlt 9730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54  |-  ( ( x  e.  RR*  /\  y  e.  RR* )  ->  (
x  <_  y  <->  -.  y  <  x ) )
9392biimpd 212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( ( x  e.  RR*  /\  y  e.  RR* )  ->  (
x  <_  y  ->  -.  y  <  x ) )
9493con2d 120 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( ( x  e.  RR*  /\  y  e.  RR* )  ->  (
y  <  x  ->  -.  x  <_  y )
)
9588, 91, 94syl2anc 671 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( ( x  e.  ( a (,) b )  /\  y  e.  ( x [,) c ) )  -> 
( y  <  x  ->  -.  x  <_  y
) )
9686, 95mt2d 122 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( ( x  e.  ( a (,) b )  /\  y  e.  ( x [,) c ) )  ->  -.  y  <  x )
9796intnand 932 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( ( x  e.  ( a (,) b )  /\  y  e.  ( x [,) c ) )  ->  -.  ( y  e.  ( a (,) b )  /\  y  <  x
) )
9897ex 440 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( x  e.  ( a (,) b )  ->  (
y  e.  ( x [,) c )  ->  -.  ( y  e.  ( a (,) b )  /\  y  <  x
) ) )
9998con2d 120 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( x  e.  ( a (,) b )  ->  (
( y  e.  ( a (,) b )  /\  y  <  x
)  ->  -.  y  e.  ( x [,) c
) ) )
10076, 99jcad 540 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( x  e.  ( a (,) b )  ->  (
( y  e.  ( a (,) b )  /\  y  <  x
)  ->  ( y  e.  ( a (,) b
)  /\  -.  y  e.  ( x [,) c
) ) ) )
101 annim 431 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( ( y  e.  ( a (,) b )  /\  -.  y  e.  (
x [,) c ) )  <->  -.  ( y  e.  ( a (,) b
)  ->  y  e.  ( x [,) c
) ) )
102100, 101syl6ib 234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( x  e.  ( a (,) b )  ->  (
( y  e.  ( a (,) b )  /\  y  <  x
)  ->  -.  (
y  e.  ( a (,) b )  -> 
y  e.  ( x [,) c ) ) ) )
103102eximdv 1775 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( x  e.  ( a (,) b )  ->  ( E. y ( y  e.  ( a (,) b
)  /\  y  <  x )  ->  E. y  -.  ( y  e.  ( a (,) b )  ->  y  e.  ( x [,) c ) ) ) )
10474, 103mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( x  e.  ( a (,) b )  ->  E. y  -.  ( y  e.  ( a (,) b )  ->  y  e.  ( x [,) c ) ) )
105 exnal 1710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( E. y  -.  ( y  e.  ( a (,) b )  ->  y  e.  ( x [,) c
) )  <->  -.  A. y
( y  e.  ( a (,) b )  ->  y  e.  ( x [,) c ) ) )
106104, 105sylib 201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( x  e.  ( a (,) b )  ->  -.  A. y ( y  e.  ( a (,) b
)  ->  y  e.  ( x [,) c
) ) )
107 dfss2 3433 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( a (,) b ) 
C_  ( x [,) c )  <->  A. y
( y  e.  ( a (,) b )  ->  y  e.  ( x [,) c ) ) )
108106, 107sylnibr 311 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( x  e.  ( a (,) b )  ->  -.  ( a (,) b
)  C_  ( x [,) c ) )
109 imnan 428 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( x  e.  ( a (,) b )  ->  -.  ( a (,) b
)  C_  ( x [,) c ) )  <->  -.  (
x  e.  ( a (,) b )  /\  ( a (,) b
)  C_  ( x [,) c ) ) )
110108, 109mpbi 213 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  -.  (
x  e.  ( a (,) b )  /\  ( a (,) b
)  C_  ( x [,) c ) )
111 eleq2 2529 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( o  =  ( a (,) b )  ->  (
x  e.  o  <->  x  e.  ( a (,) b
) ) )
112 sseq1 3465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( o  =  ( a (,) b )  ->  (
o  C_  ( x [,) c )  <->  ( a (,) b )  C_  (
x [,) c ) ) )
113111, 112anbi12d 722 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( o  =  ( a (,) b )  ->  (
( x  e.  o  /\  o  C_  (
x [,) c ) )  <->  ( x  e.  ( a (,) b
)  /\  ( a (,) b )  C_  (
x [,) c ) ) ) )
114110, 113mtbiri 309 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( o  =  ( a (,) b )  ->  -.  ( x  e.  o  /\  o  C_  ( x [,) c ) ) )
115 sseq2 3466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( i  =  ( x [,) c )  ->  (
o  C_  i  <->  o  C_  ( x [,) c
) ) )
116115anbi2d 715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( i  =  ( x [,) c )  ->  (
( x  e.  o  /\  o  C_  i
)  <->  ( x  e.  o  /\  o  C_  ( x [,) c
) ) ) )
117116notbid 300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( i  =  ( x [,) c )  ->  ( -.  ( x  e.  o  /\  o  C_  i
)  <->  -.  ( x  e.  o  /\  o  C_  ( x [,) c
) ) ) )
118114, 117syl5ibrcom 230 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( o  =  ( a (,) b )  ->  (
i  =  ( x [,) c )  ->  -.  ( x  e.  o  /\  o  C_  i
) ) )
119118a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( a  e.  RR*  /\  b  e.  RR* )  ->  (
o  =  ( a (,) b )  -> 
( i  =  ( x [,) c )  ->  -.  ( x  e.  o  /\  o  C_  i ) ) ) )
120119rexlimivv 2896 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( E. a  e.  RR*  E. b  e.  RR*  o  =  ( a (,) b )  ->  ( i  =  ( x [,) c
)  ->  -.  (
x  e.  o  /\  o  C_  i ) ) )
12171, 120sylbi 200 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( o  e.  ran  (,)  ->  ( i  =  ( x [,) c )  ->  -.  ( x  e.  o  /\  o  C_  i
) ) )
122121com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( i  =  ( x [,) c )  ->  (
o  e.  ran  (,)  ->  -.  ( x  e.  o  /\  o  C_  i ) ) )
123122ralrimiv 2812 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( i  =  ( x [,) c )  ->  A. o  e.  ran  (,)  -.  (
x  e.  o  /\  o  C_  i ) )
124 ralnex 2846 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( A. o  e.  ran  (,)  -.  ( x  e.  o  /\  o  C_  i )  <->  -.  E. o  e.  ran  (,) ( x  e.  o  /\  o  C_  i
) )
125123, 124sylib 201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( i  =  ( x [,) c )  ->  -.  E. o  e.  ran  (,) ( x  e.  o  /\  o  C_  i ) )
126125adantl 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( x  e.  RR  /\  c  e.  RR )  /\  i  =  ( x [,) c ) )  ->  -.  E. o  e.  ran  (,) ( x  e.  o  /\  o  C_  i ) )
12766, 126jca 539 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( x  e.  RR  /\  c  e.  RR )  /\  i  =  ( x [,) c ) )  ->  ( i  e.  I  /\  -.  E. o  e.  ran  (,) (
x  e.  o  /\  o  C_  i ) ) )
128127adantlr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( x  e.  RR  /\  c  e.  RR )  /\  x  <  c )  /\  i  =  ( x [,) c ) )  -> 
( i  e.  I  /\  -.  E. o  e. 
ran  (,) ( x  e.  o  /\  o  C_  i ) ) )
12949, 128jca 539 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( 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 811 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( 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 431 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( 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
) ) )
132131anbi2i 705 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( 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 ) ) ) )
133130, 132bitri 257 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( 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 ) ) ) )
134129, 133sylib 201 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( 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 2857 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( 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
) ) )
136134, 135syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( 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 2848 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( 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 ) ) )
138136, 137sylib 201 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( 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
) ) )
139138exp41 619 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 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 ) ) ) ) ) )
140139com4l 87 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 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 ) ) ) ) ) )
141140imp41 602 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( 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 2857 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( 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
) ) )
14334, 141, 142syl2anc 671 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( 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 2848 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 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 ) ) )
145143, 144sylib 201 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( 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 11675 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  [,)  =  ( m  e.  RR* ,  n  e.  RR*  |->  { z  e. 
RR*  |  ( m  <_  z  /\  z  < 
n ) } )
147146ixxex 11680 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  [,)  e.  _V
148 imaexg 6762 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( [,) 
e.  _V  ->  ( [,) " ( RR  X.  RR ) )  e.  _V )
149147, 148ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( [,) " ( RR  X.  RR ) )  e.  _V
1501, 149eqeltri 2536 . . . . . . . . . . . . . . . . . . . . . 22  |-  I  e. 
_V
1511icoreunrn 31808 . . . . . . . . . . . . . . . . . . . . . . 23  |-  RR  =  U. I
152 unirnioo 11768 . . . . . . . . . . . . . . . . . . . . . . 23  |-  RR  =  U. ran  (,)
153151, 152eqtr3i 2486 . . . . . . . . . . . . . . . . . . . . . 22  |-  U. I  =  U. ran  (,)
154 tgss2 20058 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( 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
) ) ) )
155150, 153, 154mp2an 683 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
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
) ) )
156151raleqi 3003 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 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 ) ) )
157155, 156bitr4i 260 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
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
) ) )
158145, 157sylnibr 311 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( c  e.  RR  /\  x  < 
c )  /\  i  =  ( x [,) c ) )  /\  x  e.  RR )  ->  -.  ( topGen `  I
)  C_  ( topGen ` 
ran  (,) ) )
159158sbcth 3294 . . . . . . . . . . . . . . . . . 18  |-  ( 1  e.  RR  ->  [. 1  /  x ]. ( ( ( ( c  e.  RR  /\  x  < 
c )  /\  i  =  ( x [,) c ) )  /\  x  e.  RR )  ->  -.  ( topGen `  I
)  C_  ( topGen ` 
ran  (,) ) ) )
1607, 159ax-mp 5 . . . . . . . . . . . . . . . . 17  |-  [. 1  /  x ]. ( ( ( ( c  e.  RR  /\  x  < 
c )  /\  i  =  ( x [,) c ) )  /\  x  e.  RR )  ->  -.  ( topGen `  I
)  C_  ( topGen ` 
ran  (,) ) )
161 sbcimg 3321 . . . . . . . . . . . . . . . . . 18  |-  ( 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  (,) ) ) ) )
1627, 161ax-mp 5 . . . . . . . . . . . . . . . . 17  |-  ( [.
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  (,) ) ) )
163160, 162mpbi 213 . . . . . . . . . . . . . . . 16  |-  ( [.
1  /  x ]. ( ( ( c  e.  RR  /\  x  <  c )  /\  i  =  ( x [,) c ) )  /\  x  e.  RR )  ->  [. 1  /  x ].  -.  ( topGen `  I
)  C_  ( topGen ` 
ran  (,) ) )
164 sbcel1v 3338 . . . . . . . . . . . . . . . . . 18  |-  ( [.
1  /  x ]. x  e.  RR  <->  1  e.  RR )
1657, 164mpbir 214 . . . . . . . . . . . . . . . . 17  |-  [. 1  /  x ]. x  e.  RR
166 sbcan 3322 . . . . . . . . . . . . . . . . 17  |-  ( [.
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 )
)
167165, 166mpbiran2 935 . . . . . . . . . . . . . . . 16  |-  ( [.
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 3345 . . . . . . . . . . . . . . . . 17  |-  ( 1  e.  RR  ->  ( [. 1  /  x ].  -.  ( topGen `  I
)  C_  ( topGen ` 
ran  (,) )  <->  -.  ( topGen `
 I )  C_  ( topGen `  ran  (,) )
) )
1697, 168ax-mp 5 . . . . . . . . . . . . . . . 16  |-  ( [.
1  /  x ].  -.  ( topGen `  I )  C_  ( topGen `  ran  (,) )  <->  -.  ( topGen `  I )  C_  ( topGen `  ran  (,) )
)
170163, 167, 1693imtr3i 273 . . . . . . . . . . . . . . 15  |-  ( [.
1  /  x ]. ( ( c  e.  RR  /\  x  < 
c )  /\  i  =  ( x [,) c ) )  ->  -.  ( topGen `  I )  C_  ( topGen `  ran  (,) )
)
17133, 170sylbir 218 . . . . . . . . . . . . . 14  |-  ( (
[. 1  /  x ]. ( c  e.  RR  /\  x  <  c )  /\  [. 1  /  x ]. i  =  ( x [,) c ) )  ->  -.  ( topGen `
 I )  C_  ( topGen `  ran  (,) )
)
17221, 32, 171syl2anbr 487 . . . . . . . . . . . . 13  |-  ( ( ( c  e.  RR  /\  1  <  c )  /\  i  =  ( 1 [,) c ) )  ->  -.  ( topGen `
 I )  C_  ( topGen `  ran  (,) )
)
173172sbcth 3294 . . . . . . . . . . . 12  |-  ( ( 1 [,) c )  e.  _V  ->  [. (
1 [,) c )  /  i ]. (
( ( c  e.  RR  /\  1  < 
c )  /\  i  =  ( 1 [,) c ) )  ->  -.  ( topGen `  I )  C_  ( topGen `  ran  (,) )
) )
1745, 173ax-mp 5 . . . . . . . . . . 11  |-  [. (
1 [,) c )  /  i ]. (
( ( c  e.  RR  /\  1  < 
c )  /\  i  =  ( 1 [,) c ) )  ->  -.  ( topGen `  I )  C_  ( topGen `  ran  (,) )
)
175 sbcimg 3321 . . . . . . . . . . . 12  |-  ( ( 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  (,) )
) ) )
1765, 175ax-mp 5 . . . . . . . . . . 11  |-  ( [. ( 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  (,) )
) )
177174, 176mpbi 213 . . . . . . . . . 10  |-  ( [. ( 1 [,) c
)  /  i ]. ( ( c  e.  RR  /\  1  < 
c )  /\  i  =  ( 1 [,) c ) )  ->  [. ( 1 [,) c
)  /  i ].  -.  ( topGen `  I )  C_  ( topGen `  ran  (,) )
)
178 sbcan 3322 . . . . . . . . . . 11  |-  ( [. ( 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 2462 . . . . . . . . . . . . 13  |-  ( 1 [,) c )  =  ( 1 [,) c
)
180 eqsbc3 3319 . . . . . . . . . . . . . 14  |-  ( ( 1 [,) c )  e.  _V  ->  ( [. ( 1 [,) c
)  /  i ]. i  =  ( 1 [,) c )  <->  ( 1 [,) c )  =  ( 1 [,) c
) ) )
1815, 180ax-mp 5 . . . . . . . . . . . . 13  |-  ( [. ( 1 [,) c
)  /  i ]. i  =  ( 1 [,) c )  <->  ( 1 [,) c )  =  ( 1 [,) c
) )
182179, 181mpbir 214 . . . . . . . . . . . 12  |-  [. (
1 [,) c )  /  i ]. i  =  ( 1 [,) c )
183 sbcg 3345 . . . . . . . . . . . . . 14  |-  ( ( 1 [,) c )  e.  _V  ->  ( [. ( 1 [,) c
)  /  i ]. ( c  e.  RR  /\  1  <  c )  <-> 
( c  e.  RR  /\  1  <  c ) ) )
1845, 183ax-mp 5 . . . . . . . . . . . . 13  |-  ( [. ( 1 [,) c
)  /  i ]. ( c  e.  RR  /\  1  <  c )  <-> 
( c  e.  RR  /\  1  <  c ) )
185184anbi1i 706 . . . . . . . . . . . 12  |-  ( (
[. ( 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 ) ) )
186182, 185mpbiran2 935 . . . . . . . . . . 11  |-  ( (
[. ( 1 [,) c )  /  i ]. ( c  e.  RR  /\  1  <  c )  /\  [. ( 1 [,) c )  / 
i ]. i  =  ( 1 [,) c ) )  <->  ( c  e.  RR  /\  1  < 
c ) )
187178, 186bitri 257 . . . . . . . . . 10  |-  ( [. ( 1 [,) c
)  /  i ]. ( ( c  e.  RR  /\  1  < 
c )  /\  i  =  ( 1 [,) c ) )  <->  ( c  e.  RR  /\  1  < 
c ) )
188 sbcg 3345 . . . . . . . . . . 11  |-  ( ( 1 [,) c )  e.  _V  ->  ( [. ( 1 [,) c
)  /  i ].  -.  ( topGen `  I )  C_  ( topGen `  ran  (,) )  <->  -.  ( topGen `  I )  C_  ( topGen `  ran  (,) )
) )
1895, 188ax-mp 5 . . . . . . . . . 10  |-  ( [. ( 1 [,) c
)  /  i ].  -.  ( topGen `  I )  C_  ( topGen `  ran  (,) )  <->  -.  ( topGen `  I )  C_  ( topGen `  ran  (,) )
)
190177, 187, 1893imtr3i 273 . . . . . . . . 9  |-  ( ( c  e.  RR  /\  1  <  c )  ->  -.  ( topGen `  I )  C_  ( topGen `  ran  (,) )
)
191190sbcth 3294 . . . . . . . 8  |-  ( 2  e.  RR  ->  [. 2  /  c ]. (
( c  e.  RR  /\  1  <  c )  ->  -.  ( topGen `  I )  C_  ( topGen `
 ran  (,) )
) )
1923, 191ax-mp 5 . . . . . . 7  |-  [. 2  /  c ]. (
( c  e.  RR  /\  1  <  c )  ->  -.  ( topGen `  I )  C_  ( topGen `
 ran  (,) )
)
193 sbcimg 3321 . . . . . . . 8  |-  ( 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  (,) ) ) ) )
1943, 193ax-mp 5 . . . . . . 7  |-  ( [.
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  (,) ) ) )
195192, 194mpbi 213 . . . . . 6  |-  ( [.
2  /  c ]. ( c  e.  RR  /\  1  <  c )  ->  [. 2  /  c ].  -.  ( topGen `  I
)  C_  ( topGen ` 
ran  (,) ) )
196 sbcan 3322 . . . . . . 7  |-  ( [.
2  /  c ]. ( c  e.  RR  /\  1  <  c )  <-> 
( [. 2  /  c ]. c  e.  RR  /\ 
[. 2  /  c ]. 1  <  c ) )
197 sbcel1v 3338 . . . . . . . 8  |-  ( [.
2  /  c ]. c  e.  RR  <->  2  e.  RR )
198 sbcbr123 4470 . . . . . . . . 9  |-  ( [.
2  /  c ].
1  <  c  <->  [_ 2  /  c ]_ 1 [_ 2  /  c ]_  <  [_ 2  /  c ]_ c )
199 csbconstg 3388 . . . . . . . . . . 11  |-  ( 2  e.  RR  ->  [_ 2  /  c ]_ 1  =  1 )
2003, 199ax-mp 5 . . . . . . . . . 10  |-  [_ 2  /  c ]_ 1  =  1
201 csbvarg 3804 . . . . . . . . . . 11  |-  ( 2  e.  RR  ->  [_ 2  /  c ]_ c  =  2 )
2023, 201ax-mp 5 . . . . . . . . . 10  |-  [_ 2  /  c ]_ c  =  2
203200, 202breq12i 4427 . . . . . . . . 9  |-  ( [_
2  /  c ]_
1 [_ 2  /  c ]_  <  [_ 2  /  c ]_ c  <->  1 [_ 2  /  c ]_  <  2 )
204 csbconstg 3388 . . . . . . . . . . 11  |-  ( 2  e.  RR  ->  [_ 2  /  c ]_  <  =  <  )
2053, 204ax-mp 5 . . . . . . . . . 10  |-  [_ 2  /  c ]_  <  =  <
206205breqi 4424 . . . . . . . . 9  |-  ( 1
[_ 2  /  c ]_  <  2  <->  1  <  2 )
207198, 203, 2063bitri 279 . . . . . . . 8  |-  ( [.
2  /  c ].
1  <  c  <->  1  <  2 )
208197, 207anbi12i 708 . . . . . . 7  |-  ( (
[. 2  /  c ]. c  e.  RR  /\ 
[. 2  /  c ]. 1  <  c )  <-> 
( 2  e.  RR  /\  1  <  2 ) )
209196, 208bitri 257 . . . . . 6  |-  ( [.
2  /  c ]. ( c  e.  RR  /\  1  <  c )  <-> 
( 2  e.  RR  /\  1  <  2 ) )
210 sbcg 3345 . . . . . . 7  |-  ( 2  e.  RR  ->  ( [. 2  /  c ].  -.  ( topGen `  I
)  C_  ( topGen ` 
ran  (,) )  <->  -.  ( topGen `
 I )  C_  ( topGen `  ran  (,) )
) )
2113, 210ax-mp 5 . . . . . 6  |-  ( [.
2  /  c ].  -.  ( topGen `  I )  C_  ( topGen `  ran  (,) )  <->  -.  ( topGen `  I )  C_  ( topGen `  ran  (,) )
)
212195, 209, 2113imtr3i 273 . . . . 5  |-  ( ( 2  e.  RR  /\  1  <  2 )  ->  -.  ( topGen `  I )  C_  ( topGen `  ran  (,) )
)
2133, 4, 212mp2an 683 . . . 4  |-  -.  ( topGen `
 I )  C_  ( topGen `  ran  (,) )
214 eqimss 3496 . . . 4  |-  ( (
topGen `  I )  =  ( topGen `  ran  (,) )  ->  ( topGen `  I )  C_  ( topGen `  ran  (,) )
)
215213, 214mto 181 . . 3  |-  -.  ( topGen `
 I )  =  ( topGen `  ran  (,) )
216215nesymir 2694 . 2  |-  ( topGen ` 
ran  (,) )  =/=  ( topGen `
 I )
217 df-pss 3432 . 2  |-  ( (
topGen `  ran  (,) )  C.  ( topGen `  I )  <->  ( ( topGen `  ran  (,) )  C_  ( topGen `  I )  /\  ( topGen `  ran  (,) )  =/=  ( topGen `  I )
) )
2182, 216, 217mpbir2an 936 1  |-  ( topGen ` 
ran  (,) )  C.  ( topGen `
 I )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 189    /\ wa 375    /\ w3a 991   A.wal 1453    = wceq 1455   E.wex 1674    e. wcel 1898    =/= wne 2633   A.wral 2749   E.wrex 2750   {crab 2753   _Vcvv 3057   [.wsbc 3279   [_csb 3375    C_ wss 3416    C. wpss 3417   ~Pcpw 3963   <.cop 3986   U.cuni 4212   class class class wbr 4418    X. cxp 4854   dom cdm 4856   ran crn 4857   "cima 4859   Fun wfun 5599    Fn wfn 5600   -->wf 5601   ` cfv 5605  (class class class)co 6320   RRcr 9569   1c1 9571   RR*cxr 9705    < clt 9706    <_ cle 9707   2c2 10692   (,)cioo 11669   [,)cico 11671   topGenctg 15391
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4541  ax-nul 4550  ax-pow 4598  ax-pr 4656  ax-un 6615  ax-cnex 9626  ax-resscn 9627  ax-1cn 9628  ax-icn 9629  ax-addcl 9630  ax-addrcl 9631  ax-mulcl 9632  ax-mulrcl 9633  ax-mulcom 9634  ax-addass 9635  ax-mulass 9636  ax-distr 9637  ax-i2m1 9638  ax-1ne0 9639  ax-1rid 9640  ax-rnegex 9641  ax-rrecex 9642  ax-cnre 9643  ax-pre-lttri 9644  ax-pre-lttrn 9645  ax-pre-ltadd 9646  ax-pre-mulgt0 9647
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-fal 1461  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-reu 2756  df-rmo 2757  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-iun 4294  df-br 4419  df-opab 4478  df-mpt 4479  df-id 4771  df-po 4777  df-so 4778  df-xp 4862  df-rel 4863  df-cnv 4864  df-co 4865  df-dm 4866  df-rn 4867  df-res 4868  df-ima 4869  df-iota 5569  df-fun 5607  df-fn 5608  df-f 5609  df-f1 5610  df-fo 5611  df-f1o 5612  df-fv 5613  df-riota 6282  df-ov 6323  df-oprab 6324  df-mpt2 6325  df-1st 6825  df-2nd 6826  df-er 7394  df-en 7601  df-dom 7602  df-sdom 7603  df-pnf 9708  df-mnf 9709  df-xr 9710  df-ltxr 9711  df-le 9712  df-sub 9893  df-neg 9894  df-div 10303  df-2 10701  df-ioo 11673  df-ico 11675  df-topgen 15397
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator