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

Theorem relowlpssretop 31732
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 31731 . 2  |-  ( topGen ` 
ran  (,) )  C_  ( topGen `
 I )
3 2re 10687 . . . . 5  |-  2  e.  RR
4 1lt2 10784 . . . . 5  |-  1  <  2
5 ovex 6334 . . . . . . . . . . . 12  |-  ( 1 [,) c )  e. 
_V
6 sbcan 3342 . . . . . . . . . . . . . . 15  |-  ( [.
1  /  x ]. ( c  e.  RR  /\  x  <  c )  <-> 
( [. 1  /  x ]. c  e.  RR  /\ 
[. 1  /  x ]. x  <  c ) )
7 1re 9650 . . . . . . . . . . . . . . . . 17  |-  1  e.  RR
8 sbcg 3365 . . . . . . . . . . . . . . . . 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 4475 . . . . . . . . . . . . . . . . 17  |-  ( [.
1  /  x ]. x  <  c  <->  [_ 1  /  x ]_ x [_
1  /  x ]_  <  [_ 1  /  x ]_ c )
11 csbvarg 3822 . . . . . . . . . . . . . . . . . . 19  |-  ( 1  e.  RR  ->  [_ 1  /  x ]_ x  =  1 )
127, 11ax-mp 5 . . . . . . . . . . . . . . . . . 18  |-  [_ 1  /  x ]_ x  =  1
13 csbconstg 3408 . . . . . . . . . . . . . . . . . . 19  |-  ( 1  e.  RR  ->  [_ 1  /  x ]_ c  =  c )
147, 13ax-mp 5 . . . . . . . . . . . . . . . . . 18  |-  [_ 1  /  x ]_ c  =  c
1512, 14breq12i 4432 . . . . . . . . . . . . . . . . 17  |-  ( [_
1  /  x ]_ x [_ 1  /  x ]_  <  [_ 1  /  x ]_ c  <->  1 [_ 1  /  x ]_  <  c
)
16 csbconstg 3408 . . . . . . . . . . . . . . . . . . 19  |-  ( 1  e.  RR  ->  [_ 1  /  x ]_  <  =  <  )
177, 16ax-mp 5 . . . . . . . . . . . . . . . . . 18  |-  [_ 1  /  x ]_  <  =  <
1817breqi 4429 . . . . . . . . . . . . . . . . 17  |-  ( 1
[_ 1  /  x ]_  <  c  <->  1  <  c )
1910, 15, 183bitri 274 . . . . . . . . . . . . . . . 16  |-  ( [.
1  /  x ]. x  <  c  <->  1  <  c )
209, 19anbi12i 701 . . . . . . . . . . . . . . 15  |-  ( (
[. 1  /  x ]. c  e.  RR  /\ 
[. 1  /  x ]. x  <  c )  <-> 
( c  e.  RR  /\  1  <  c ) )
216, 20bitri 252 . . . . . . . . . . . . . 14  |-  ( [.
1  /  x ]. ( c  e.  RR  /\  x  <  c )  <-> 
( c  e.  RR  /\  1  <  c ) )
22 sbceqg 3803 . . . . . . . . . . . . . . . 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 3408 . . . . . . . . . . . . . . . . 17  |-  ( 1  e.  RR  ->  [_ 1  /  x ]_ i  =  i )
257, 24ax-mp 5 . . . . . . . . . . . . . . . 16  |-  [_ 1  /  x ]_ i  =  i
26 csbov123 6340 . . . . . . . . . . . . . . . . 17  |-  [_ 1  /  x ]_ ( x [,) c )  =  ( [_ 1  /  x ]_ x [_ 1  /  x ]_ [,) [_ 1  /  x ]_ c )
27 csbconstg 3408 . . . . . . . . . . . . . . . . . . 19  |-  ( 1  e.  RR  ->  [_ 1  /  x ]_ [,)  =  [,) )
287, 27ax-mp 5 . . . . . . . . . . . . . . . . . 18  |-  [_ 1  /  x ]_ [,)  =  [,)
2912, 14, 28oveq123i 6320 . . . . . . . . . . . . . . . . 17  |-  ( [_
1  /  x ]_ x [_ 1  /  x ]_ [,) [_ 1  /  x ]_ c )  =  ( 1 [,) c
)
3026, 29eqtri 2451 . . . . . . . . . . . . . . . 16  |-  [_ 1  /  x ]_ ( x [,) c )  =  ( 1 [,) c
)
3125, 30eqeq12i 2442 . . . . . . . . . . . . . . 15  |-  ( [_
1  /  x ]_ i  =  [_ 1  /  x ]_ ( x [,) c )  <->  i  =  ( 1 [,) c
) )
3223, 31bitri 252 . . . . . . . . . . . . . 14  |-  ( [.
1  /  x ]. i  =  ( x [,) c )  <->  i  =  ( 1 [,) c
) )
33 sbcan 3342 . . . . . . . . . . . . . . 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 462 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( c  e.  RR  /\  x  < 
c )  /\  i  =  ( x [,) c ) )  /\  x  e.  RR )  ->  x  e.  RR )
35 simpl 458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( x  e.  RR  /\  c  e.  RR )  ->  x  e.  RR )
36 leid 9737 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( x  e.  RR  ->  x  <_  x )
3735, 36jccir 541 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( x  e.  RR  /\  c  e.  RR )  ->  ( x  e.  RR  /\  x  <_  x )
)
38 rexr 9694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( c  e.  RR  ->  c  e.  RR* )
39 elico2 11706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( x  e.  RR  /\  c  e.  RR* )  -> 
( x  e.  ( x [,) c )  <-> 
( x  e.  RR  /\  x  <_  x  /\  x  <  c ) ) )
4038, 39sylan2 476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( x  e.  RR  /\  c  e.  RR )  ->  ( x  e.  ( x [,) c )  <-> 
( x  e.  RR  /\  x  <_  x  /\  x  <  c ) ) )
41 df-3an 984 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( x  e.  RR  /\  x  <_  x  /\  x  <  c )  <->  ( (
x  e.  RR  /\  x  <_  x )  /\  x  <  c ) )
4240, 41syl6bb 264 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( x  e.  RR  /\  c  e.  RR )  ->  ( x  e.  ( x [,) c )  <-> 
( ( x  e.  RR  /\  x  <_  x )  /\  x  <  c ) ) )
4342baibd 917 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( x  e.  RR  /\  c  e.  RR )  /\  ( x  e.  RR  /\  x  <_  x ) )  -> 
( x  e.  ( x [,) c )  <-> 
x  <  c )
)
4437, 43mpdan 672 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( x  e.  RR  /\  c  e.  RR )  ->  ( x  e.  ( x [,) c )  <-> 
x  <  c )
)
4544biimpar 487 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( x  e.  RR  /\  c  e.  RR )  /\  x  <  c
)  ->  x  e.  ( x [,) c
) )
4645adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( x  e.  RR  /\  c  e.  RR )  /\  x  <  c )  /\  i  =  ( x [,) c ) )  ->  x  e.  ( x [,) c ) )
47 eleq2 2496 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( i  =  ( x [,) c )  ->  (
x  e.  i  <->  x  e.  ( x [,) c
) ) )
4847adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( x  e.  RR  /\  c  e.  RR )  /\  x  <  c )  /\  i  =  ( x [,) c ) )  -> 
( x  e.  i  <-> 
x  e.  ( x [,) c ) ) )
4946, 48mpbird 235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( x  e.  RR  /\  c  e.  RR )  /\  x  <  c )  /\  i  =  ( x [,) c ) )  ->  x  e.  i )
50 rexpssxrxp 9693 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( RR 
X.  RR )  C_  ( RR*  X.  RR* )
51 opelxpi 4885 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( x  e.  RR  /\  c  e.  RR )  -> 
<. x ,  c >.  e.  ( RR  X.  RR ) )
5250, 51sseldi 3462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( x  e.  RR  /\  c  e.  RR )  -> 
<. x ,  c >.  e.  ( RR*  X.  RR* )
)
53 df-ico 11649 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  [,)  =  ( x  e.  RR* ,  c  e.  RR*  |->  { z  e.  RR*  |  (
x  <_  z  /\  z  <  c ) } )
5453ixxf 11653 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  [,) :
( RR*  X.  RR* ) --> ~P RR*
5554fdmi 5751 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  dom  [,)  =  ( RR*  X.  RR* )
5655eleq2i 2499 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( <.
x ,  c >.  e.  dom  [,)  <->  <. x ,  c
>.  e.  ( RR*  X.  RR* ) )
5753mpt2fun 6413 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  Fun  [,)
58 funfvima 6156 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( Fun  [,)  /\  <. x ,  c >.  e.  dom  [,) )  ->  ( <. x ,  c >.  e.  ( RR  X.  RR )  ->  ( [,) `  <. x ,  c >. )  e.  ( [,) " ( RR  X.  RR ) ) ) )
5957, 58mpan 674 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( <.
x ,  c >.  e.  dom  [,)  ->  ( <.
x ,  c >.  e.  ( RR  X.  RR )  ->  ( [,) `  <. x ,  c >. )  e.  ( [,) " ( RR  X.  RR ) ) ) )
6056, 59sylbir 216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6309 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( x [,) c )  =  ( [,) `  <. x ,  c >. )
6361, 62, 13eltr4g 2525 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( x  e.  RR  /\  c  e.  RR )  ->  ( x [,) c
)  e.  I )
64 eleq1 2495 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( i  =  ( x [,) c )  ->  (
i  e.  I  <->  ( x [,) c )  e.  I
) )
6563, 64syl5ibrcom 225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( x  e.  RR  /\  c  e.  RR )  ->  ( i  =  ( x [,) c )  ->  i  e.  I
) )
6665imp 430 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( x  e.  RR  /\  c  e.  RR )  /\  i  =  ( x [,) c ) )  ->  i  e.  I )
67 ioof 11740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  (,) :
( RR*  X.  RR* ) --> ~P RR
68 ffn 5746 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( (,)
: ( RR*  X.  RR* )
--> ~P RR  ->  (,)  Fn  ( RR*  X.  RR* )
)
6967, 68ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  (,)  Fn  ( RR*  X.  RR* )
70 ovelrn 6460 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 31730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( x  e.  ( a (,) b )  ->  E. y  e.  ( a (,) b
) y  <  x
)
73 df-rex 2777 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( E. y  e.  ( a (,) b ) y  <  x  <->  E. y
( y  e.  ( a (,) b )  /\  y  <  x
) )
7472, 73sylib 199 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( x  e.  ( a (,) b )  ->  E. y
( y  e.  ( a (,) b )  /\  y  <  x
) )
75 simpl 458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6528 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( y  e.  ( x [,) c )  ->  c  e.  RR* )
78 elioore 11674 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57  |-  ( x  e.  ( a (,) b )  ->  x  e.  RR )
79 elico2 11706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57  |-  ( ( x  e.  RR  /\  c  e.  RR* )  -> 
( y  e.  ( x [,) c )  <-> 
( y  e.  RR  /\  x  <_  y  /\  y  <  c ) ) )
8078, 79sylan 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56  |-  ( ( x  e.  ( a (,) b )  /\  c  e.  RR* )  -> 
( y  e.  ( x [,) c )  <-> 
( y  e.  RR  /\  x  <_  y  /\  y  <  c ) ) )
81 simp2 1006 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56  |-  ( ( y  e.  RR  /\  x  <_  y  /\  y  <  c )  ->  x  <_  y )
8280, 81syl6bi 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55  |-  ( ( x  e.  ( a (,) b )  /\  c  e.  RR* )  -> 
( y  e.  ( x [,) c )  ->  x  <_  y
) )
8382ex 435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 430 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( ( x  e.  ( a (,) b )  /\  y  e.  ( x [,) c ) )  ->  x  <_  y )
8778rexrd 9698 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( x  e.  ( a (,) b )  ->  x  e.  RR* )
8887adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( ( x  e.  ( a (,) b )  /\  y  e.  ( x [,) c ) )  ->  x  e.  RR* )
89 elicore 11695 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54  |-  ( ( x  e.  RR  /\  y  e.  ( x [,) c ) )  -> 
y  e.  RR )
9078, 89sylan 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( ( x  e.  ( a (,) b )  /\  y  e.  ( x [,) c ) )  -> 
y  e.  RR )
9190rexrd 9698 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( ( x  e.  ( a (,) b )  /\  y  e.  ( x [,) c ) )  -> 
y  e.  RR* )
92 xrlenlt 9707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54  |-  ( ( x  e.  RR*  /\  y  e.  RR* )  ->  (
x  <_  y  <->  -.  y  <  x ) )
9392biimpd 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( ( x  e.  RR*  /\  y  e.  RR* )  ->  (
x  <_  y  ->  -.  y  <  x ) )
9493con2d 118 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( ( x  e.  RR*  /\  y  e.  RR* )  ->  (
y  <  x  ->  -.  x  <_  y )
)
9588, 91, 94syl2anc 665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( ( x  e.  ( a (,) b )  /\  y  e.  ( x [,) c ) )  -> 
( y  <  x  ->  -.  x  <_  y
) )
9686, 95mt2d 120 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( ( x  e.  ( a (,) b )  /\  y  e.  ( x [,) c ) )  ->  -.  y  <  x )
9796intnand 924 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( ( x  e.  ( a (,) b )  /\  y  e.  ( x [,) c ) )  ->  -.  ( y  e.  ( a (,) b )  /\  y  <  x
) )
9897ex 435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( x  e.  ( a (,) b )  ->  (
y  e.  ( x [,) c )  ->  -.  ( y  e.  ( a (,) b )  /\  y  <  x
) ) )
9998con2d 118 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( x  e.  ( a (,) b )  ->  (
( y  e.  ( a (,) b )  /\  y  <  x
)  ->  -.  y  e.  ( x [,) c
) ) )
10076, 99jcad 535 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( x  e.  ( a (,) b )  ->  (
( y  e.  ( a (,) b )  /\  y  <  x
)  ->  ( y  e.  ( a (,) b
)  /\  -.  y  e.  ( x [,) c
) ) ) )
101 annim 426 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( ( y  e.  ( a (,) b )  /\  -.  y  e.  (
x [,) c ) )  <->  -.  ( y  e.  ( a (,) b
)  ->  y  e.  ( x [,) c
) ) )
102100, 101syl6ib 229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( x  e.  ( a (,) b )  ->  (
( y  e.  ( a (,) b )  /\  y  <  x
)  ->  -.  (
y  e.  ( a (,) b )  -> 
y  e.  ( x [,) c ) ) ) )
103102eximdv 1758 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1693 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( E. y  -.  ( y  e.  ( a (,) b )  ->  y  e.  ( x [,) c
) )  <->  -.  A. y
( y  e.  ( a (,) b )  ->  y  e.  ( x [,) c ) ) )
106104, 105sylib 199 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( x  e.  ( a (,) b )  ->  -.  A. y ( y  e.  ( a (,) b
)  ->  y  e.  ( x [,) c
) ) )
107 dfss2 3453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( a (,) b ) 
C_  ( x [,) c )  <->  A. y
( y  e.  ( a (,) b )  ->  y  e.  ( x [,) c ) ) )
108106, 107sylnibr 306 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( x  e.  ( a (,) b )  ->  -.  ( a (,) b
)  C_  ( x [,) c ) )
109 imnan 423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( x  e.  ( a (,) b )  ->  -.  ( a (,) b
)  C_  ( x [,) c ) )  <->  -.  (
x  e.  ( a (,) b )  /\  ( a (,) b
)  C_  ( x [,) c ) ) )
110108, 109mpbi 211 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  -.  (
x  e.  ( a (,) b )  /\  ( a (,) b
)  C_  ( x [,) c ) )
111 eleq2 2496 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( o  =  ( a (,) b )  ->  (
x  e.  o  <->  x  e.  ( a (,) b
) ) )
112 sseq1 3485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( o  =  ( a (,) b )  ->  (
o  C_  ( x [,) c )  <->  ( a (,) b )  C_  (
x [,) c ) ) )
113111, 112anbi12d 715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( o  =  ( a (,) b )  ->  (
( x  e.  o  /\  o  C_  (
x [,) c ) )  <->  ( x  e.  ( a (,) b
)  /\  ( a (,) b )  C_  (
x [,) c ) ) ) )
114110, 113mtbiri 304 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( o  =  ( a (,) b )  ->  -.  ( x  e.  o  /\  o  C_  ( x [,) c ) ) )
115 sseq2 3486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( i  =  ( x [,) c )  ->  (
o  C_  i  <->  o  C_  ( x [,) c
) ) )
116115anbi2d 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( i  =  ( x [,) c )  ->  (
( x  e.  o  /\  o  C_  i
)  <->  ( x  e.  o  /\  o  C_  ( x [,) c
) ) ) )
117116notbid 295 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( i  =  ( x [,) c )  ->  ( -.  ( x  e.  o  /\  o  C_  i
)  <->  -.  ( x  e.  o  /\  o  C_  ( x [,) c
) ) ) )
118114, 117syl5ibrcom 225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2919 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( E. a  e.  RR*  E. b  e.  RR*  o  =  ( a (,) b )  ->  ( i  =  ( x [,) c
)  ->  -.  (
x  e.  o  /\  o  C_  i ) ) )
12171, 120sylbi 198 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2834 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( i  =  ( x [,) c )  ->  A. o  e.  ran  (,)  -.  (
x  e.  o  /\  o  C_  i ) )
124 ralnex 2868 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( A. o  e.  ran  (,)  -.  ( x  e.  o  /\  o  C_  i )  <->  -.  E. o  e.  ran  (,) ( x  e.  o  /\  o  C_  i
) )
125123, 124sylib 199 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( i  =  ( x [,) c )  ->  -.  E. o  e.  ran  (,) ( x  e.  o  /\  o  C_  i ) )
126125adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( x  e.  RR  /\  c  e.  RR )  /\  i  =  ( x [,) c ) )  ->  -.  E. o  e.  ran  (,) ( x  e.  o  /\  o  C_  i ) )
12766, 126jca 534 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( x  e.  RR  /\  c  e.  RR )  /\  i  =  ( x [,) c ) )  ->  ( i  e.  I  /\  -.  E. o  e.  ran  (,) (
x  e.  o  /\  o  C_  i ) ) )
128127adantlr 719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 534 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 804 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 426 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 698 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 252 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 199 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2880 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2870 . . . . . . . . . . . . . . . . . . . . . . . . . 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 199 . . . . . . . . . . . . . . . . . . . . . . . . 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 613 . . . . . . . . . . . . . . . . . . . . . . . 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 596 . . . . . . . . . . . . . . . . . . . . . 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 2880 . . . . . . . . . . . . . . . . . . . . . 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 665 . . . . . . . . . . . . . . . . . . . . 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 2870 . . . . . . . . . . . . . . . . . . . . 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 199 . . . . . . . . . . . . . . . . . . . 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 11649 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  [,)  =  ( m  e.  RR* ,  n  e.  RR*  |->  { z  e. 
RR*  |  ( m  <_  z  /\  z  < 
n ) } )
147146ixxex 11654 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  [,)  e.  _V
148 imaexg 6745 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( [,) 
e.  _V  ->  ( [,) " ( RR  X.  RR ) )  e.  _V )
149147, 148ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( [,) " ( RR  X.  RR ) )  e.  _V
1501, 149eqeltri 2503 . . . . . . . . . . . . . . . . . . . . . 22  |-  I  e. 
_V
1511icoreunrn 31727 . . . . . . . . . . . . . . . . . . . . . . 23  |-  RR  =  U. I
152 unirnioo 11742 . . . . . . . . . . . . . . . . . . . . . . 23  |-  RR  =  U. ran  (,)
153151, 152eqtr3i 2453 . . . . . . . . . . . . . . . . . . . . . 22  |-  U. I  =  U. ran  (,)
154 tgss2 20002 . . . . . . . . . . . . . . . . . . . . . 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 676 . . . . . . . . . . . . . . . . . . . . 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 3026 . . . . . . . . . . . . . . . . . . . . 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 255 . . . . . . . . . . . . . . . . . . . 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 306 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( c  e.  RR  /\  x  < 
c )  /\  i  =  ( x [,) c ) )  /\  x  e.  RR )  ->  -.  ( topGen `  I
)  C_  ( topGen ` 
ran  (,) ) )
159158sbcth 3314 . . . . . . . . . . . . . . . . . 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 3341 . . . . . . . . . . . . . . . . . 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 211 . . . . . . . . . . . . . . . 16  |-  ( [.
1  /  x ]. ( ( ( c  e.  RR  /\  x  <  c )  /\  i  =  ( x [,) c ) )  /\  x  e.  RR )  ->  [. 1  /  x ].  -.  ( topGen `  I
)  C_  ( topGen ` 
ran  (,) ) )
164 sbcel1v 3358 . . . . . . . . . . . . . . . . . 18  |-  ( [.
1  /  x ]. x  e.  RR  <->  1  e.  RR )
1657, 164mpbir 212 . . . . . . . . . . . . . . . . 17  |-  [. 1  /  x ]. x  e.  RR
166 sbcan 3342 . . . . . . . . . . . . . . . . 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 927 . . . . . . . . . . . . . . . 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 3365 . . . . . . . . . . . . . . . . 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 268 . . . . . . . . . . . . . . 15  |-  ( [.
1  /  x ]. ( ( c  e.  RR  /\  x  < 
c )  /\  i  =  ( x [,) c ) )  ->  -.  ( topGen `  I )  C_  ( topGen `  ran  (,) )
)
17133, 170sylbir 216 . . . . . . . . . . . . . 14  |-  ( (
[. 1  /  x ]. ( c  e.  RR  /\  x  <  c )  /\  [. 1  /  x ]. i  =  ( x [,) c ) )  ->  -.  ( topGen `
 I )  C_  ( topGen `  ran  (,) )
)
17221, 32, 171syl2anbr 482 . . . . . . . . . . . . 13  |-  ( ( ( c  e.  RR  /\  1  <  c )  /\  i  =  ( 1 [,) c ) )  ->  -.  ( topGen `
 I )  C_  ( topGen `  ran  (,) )
)
173172sbcth 3314 . . . . . . . . . . . 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 3341 . . . . . . . . . . . 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 211 . . . . . . . . . 10  |-  ( [. ( 1 [,) c
)  /  i ]. ( ( c  e.  RR  /\  1  < 
c )  /\  i  =  ( 1 [,) c ) )  ->  [. ( 1 [,) c
)  /  i ].  -.  ( topGen `  I )  C_  ( topGen `  ran  (,) )
)
178 sbcan 3342 . . . . . . . . . . 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 2422 . . . . . . . . . . . . 13  |-  ( 1 [,) c )  =  ( 1 [,) c
)
180 eqsbc3 3339 . . . . . . . . . . . . . 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 212 . . . . . . . . . . . 12  |-  [. (
1 [,) c )  /  i ]. i  =  ( 1 [,) c )
183 sbcg 3365 . . . . . . . . . . . . . 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 699 . . . . . . . . . . . 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 927 . . . . . . . . . . 11  |-  ( (
[. ( 1 [,) c )  /  i ]. ( c  e.  RR  /\  1  <  c )  /\  [. ( 1 [,) c )  / 
i ]. i  =  ( 1 [,) c ) )  <->  ( c  e.  RR  /\  1  < 
c ) )
187178, 186bitri 252 . . . . . . . . . 10  |-  ( [. ( 1 [,) c
)  /  i ]. ( ( c  e.  RR  /\  1  < 
c )  /\  i  =  ( 1 [,) c ) )  <->  ( c  e.  RR  /\  1  < 
c ) )
188 sbcg 3365 . . . . . . . . . . 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 268 . . . . . . . . 9  |-  ( ( c  e.  RR  /\  1  <  c )  ->  -.  ( topGen `  I )  C_  ( topGen `  ran  (,) )
)
191190sbcth 3314 . . . . . . . 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 3341 . . . . . . . 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 211 . . . . . 6  |-  ( [.
2  /  c ]. ( c  e.  RR  /\  1  <  c )  ->  [. 2  /  c ].  -.  ( topGen `  I
)  C_  ( topGen ` 
ran  (,) ) )
196 sbcan 3342 . . . . . . 7  |-  ( [.
2  /  c ]. ( c  e.  RR  /\  1  <  c )  <-> 
( [. 2  /  c ]. c  e.  RR  /\ 
[. 2  /  c ]. 1  <  c ) )
197 sbcel1v 3358 . . . . . . . 8  |-  ( [.
2  /  c ]. c  e.  RR  <->  2  e.  RR )
198 sbcbr123 4475 . . . . . . . . 9  |-  ( [.
2  /  c ].
1  <  c  <->  [_ 2  /  c ]_ 1 [_ 2  /  c ]_  <  [_ 2  /  c ]_ c )
199 csbconstg 3408 . . . . . . . . . . 11  |-  ( 2  e.  RR  ->  [_ 2  /  c ]_ 1  =  1 )
2003, 199ax-mp 5 . . . . . . . . . 10  |-  [_ 2  /  c ]_ 1  =  1
201 csbvarg 3822 . . . . . . . . . . 11  |-  ( 2  e.  RR  ->  [_ 2  /  c ]_ c  =  2 )
2023, 201ax-mp 5 . . . . . . . . . 10  |-  [_ 2  /  c ]_ c  =  2
203200, 202breq12i 4432 . . . . . . . . 9  |-  ( [_
2  /  c ]_
1 [_ 2  /  c ]_  <  [_ 2  /  c ]_ c  <->  1 [_ 2  /  c ]_  <  2 )
204 csbconstg 3408 . . . . . . . . . . 11  |-  ( 2  e.  RR  ->  [_ 2  /  c ]_  <  =  <  )
2053, 204ax-mp 5 . . . . . . . . . 10  |-  [_ 2  /  c ]_  <  =  <
206205breqi 4429 . . . . . . . . 9  |-  ( 1
[_ 2  /  c ]_  <  2  <->  1  <  2 )
207198, 203, 2063bitri 274 . . . . . . . 8  |-  ( [.
2  /  c ].
1  <  c  <->  1  <  2 )
208197, 207anbi12i 701 . . . . . . 7  |-  ( (
[. 2  /  c ]. c  e.  RR  /\ 
[. 2  /  c ]. 1  <  c )  <-> 
( 2  e.  RR  /\  1  <  2 ) )
209196, 208bitri 252 . . . . . 6  |-  ( [.
2  /  c ]. ( c  e.  RR  /\  1  <  c )  <-> 
( 2  e.  RR  /\  1  <  2 ) )
210 sbcg 3365 . . . . . . 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 268 . . . . 5  |-  ( ( 2  e.  RR  /\  1  <  2 )  ->  -.  ( topGen `  I )  C_  ( topGen `  ran  (,) )
)
2133, 4, 212mp2an 676 . . . 4  |-  -.  ( topGen `
 I )  C_  ( topGen `  ran  (,) )
214 eqimss 3516 . . . 4  |-  ( (
topGen `  I )  =  ( topGen `  ran  (,) )  ->  ( topGen `  I )  C_  ( topGen `  ran  (,) )
)
215213, 214mto 179 . . 3  |-  -.  ( topGen `
 I )  =  ( topGen `  ran  (,) )
216215nesymir 2695 . 2  |-  ( topGen ` 
ran  (,) )  =/=  ( topGen `
 I )
217 df-pss 3452 . 2  |-  ( (
topGen `  ran  (,) )  C.  ( topGen `  I )  <->  ( ( topGen `  ran  (,) )  C_  ( topGen `  I )  /\  ( topGen `  ran  (,) )  =/=  ( topGen `  I )
) )
2182, 216, 217mpbir2an 928 1  |-  ( topGen ` 
ran  (,) )  C.  ( topGen `
 I )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 187    /\ wa 370    /\ w3a 982   A.wal 1435    = wceq 1437   E.wex 1657    e. wcel 1872    =/= wne 2614   A.wral 2771   E.wrex 2772   {crab 2775   _Vcvv 3080   [.wsbc 3299   [_csb 3395    C_ wss 3436    C. wpss 3437   ~Pcpw 3981   <.cop 4004   U.cuni 4219   class class class wbr 4423    X. cxp 4851   dom cdm 4853   ran crn 4854   "cima 4856   Fun wfun 5595    Fn wfn 5596   -->wf 5597   ` cfv 5601  (class class class)co 6306   RRcr 9546   1c1 9548   RR*cxr 9682    < clt 9683    <_ cle 9684   2c2 10667   (,)cioo 11643   [,)cico 11645   topGenctg 15336
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6598  ax-cnex 9603  ax-resscn 9604  ax-1cn 9605  ax-icn 9606  ax-addcl 9607  ax-addrcl 9608  ax-mulcl 9609  ax-mulrcl 9610  ax-mulcom 9611  ax-addass 9612  ax-mulass 9613  ax-distr 9614  ax-i2m1 9615  ax-1ne0 9616  ax-1rid 9617  ax-rnegex 9618  ax-rrecex 9619  ax-cnre 9620  ax-pre-lttri 9621  ax-pre-lttrn 9622  ax-pre-ltadd 9623  ax-pre-mulgt0 9624
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-fal 1443  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-nel 2617  df-ral 2776  df-rex 2777  df-reu 2778  df-rmo 2779  df-rab 2780  df-v 3082  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-op 4005  df-uni 4220  df-iun 4301  df-br 4424  df-opab 4483  df-mpt 4484  df-id 4768  df-po 4774  df-so 4775  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6268  df-ov 6309  df-oprab 6310  df-mpt2 6311  df-1st 6808  df-2nd 6809  df-er 7375  df-en 7582  df-dom 7583  df-sdom 7584  df-pnf 9685  df-mnf 9686  df-xr 9687  df-ltxr 9688  df-le 9689  df-sub 9870  df-neg 9871  df-div 10278  df-2 10676  df-ioo 11647  df-ico 11649  df-topgen 15342
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator