MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  opnmbllem Structured version   Unicode version

Theorem opnmbllem 21096
Description: Lemma for opnmbl 21097. (Contributed by Mario Carneiro, 26-Mar-2015.)
Hypothesis
Ref Expression
dyadmbl.1  |-  F  =  ( x  e.  ZZ ,  y  e.  NN0  |->  <. ( x  /  (
2 ^ y ) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) ) >.
)
Assertion
Ref Expression
opnmbllem  |-  ( A  e.  ( topGen `  ran  (,) )  ->  A  e.  dom  vol )
Distinct variable groups:    x, y, A    x, F, y

Proof of Theorem opnmbllem
Dummy variables  c 
a  b  n  w  z  r are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq2 5706 . . . . . . . . 9  |-  ( z  =  w  ->  ( [,] `  z )  =  ( [,] `  w
) )
21sseq1d 3398 . . . . . . . 8  |-  ( z  =  w  ->  (
( [,] `  z
)  C_  A  <->  ( [,] `  w )  C_  A
) )
32elrab 3132 . . . . . . 7  |-  ( w  e.  { z  e. 
ran  F  |  ( [,] `  z )  C_  A }  <->  ( w  e. 
ran  F  /\  ( [,] `  w )  C_  A ) )
4 simprr 756 . . . . . . . 8  |-  ( ( A  e.  ( topGen ` 
ran  (,) )  /\  (
w  e.  ran  F  /\  ( [,] `  w
)  C_  A )
)  ->  ( [,] `  w )  C_  A
)
5 fvex 5716 . . . . . . . . 9  |-  ( [,] `  w )  e.  _V
65elpw 3881 . . . . . . . 8  |-  ( ( [,] `  w )  e.  ~P A  <->  ( [,] `  w )  C_  A
)
74, 6sylibr 212 . . . . . . 7  |-  ( ( A  e.  ( topGen ` 
ran  (,) )  /\  (
w  e.  ran  F  /\  ( [,] `  w
)  C_  A )
)  ->  ( [,] `  w )  e.  ~P A )
83, 7sylan2b 475 . . . . . 6  |-  ( ( A  e.  ( topGen ` 
ran  (,) )  /\  w  e.  { z  e.  ran  F  |  ( [,] `  z
)  C_  A }
)  ->  ( [,] `  w )  e.  ~P A )
98ralrimiva 2814 . . . . 5  |-  ( A  e.  ( topGen `  ran  (,) )  ->  A. w  e.  { z  e.  ran  F  |  ( [,] `  z
)  C_  A } 
( [,] `  w
)  e.  ~P A
)
10 iccf 11403 . . . . . . 7  |-  [,] :
( RR*  X.  RR* ) --> ~P RR*
11 ffun 5576 . . . . . . 7  |-  ( [,]
: ( RR*  X.  RR* )
--> ~P RR*  ->  Fun  [,] )
1210, 11ax-mp 5 . . . . . 6  |-  Fun  [,]
13 ssrab2 3452 . . . . . . . 8  |-  { z  e.  ran  F  | 
( [,] `  z
)  C_  A }  C_ 
ran  F
14 dyadmbl.1 . . . . . . . . . . 11  |-  F  =  ( x  e.  ZZ ,  y  e.  NN0  |->  <. ( x  /  (
2 ^ y ) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) ) >.
)
1514dyadf 21086 . . . . . . . . . 10  |-  F :
( ZZ  X.  NN0 )
--> (  <_  i^i  ( RR  X.  RR ) )
16 frn 5580 . . . . . . . . . 10  |-  ( F : ( ZZ  X.  NN0 ) --> (  <_  i^i  ( RR  X.  RR ) )  ->  ran  F 
C_  (  <_  i^i  ( RR  X.  RR ) ) )
1715, 16ax-mp 5 . . . . . . . . 9  |-  ran  F  C_  (  <_  i^i  ( RR  X.  RR ) )
18 inss2 3586 . . . . . . . . . 10  |-  (  <_  i^i  ( RR  X.  RR ) )  C_  ( RR  X.  RR )
19 rexpssxrxp 9443 . . . . . . . . . 10  |-  ( RR 
X.  RR )  C_  ( RR*  X.  RR* )
2018, 19sstri 3380 . . . . . . . . 9  |-  (  <_  i^i  ( RR  X.  RR ) )  C_  ( RR*  X.  RR* )
2117, 20sstri 3380 . . . . . . . 8  |-  ran  F  C_  ( RR*  X.  RR* )
2213, 21sstri 3380 . . . . . . 7  |-  { z  e.  ran  F  | 
( [,] `  z
)  C_  A }  C_  ( RR*  X.  RR* )
2310fdmi 5579 . . . . . . 7  |-  dom  [,]  =  ( RR*  X.  RR* )
2422, 23sseqtr4i 3404 . . . . . 6  |-  { z  e.  ran  F  | 
( [,] `  z
)  C_  A }  C_ 
dom  [,]
25 funimass4 5757 . . . . . 6  |-  ( ( Fun  [,]  /\  { z  e.  ran  F  | 
( [,] `  z
)  C_  A }  C_ 
dom  [,] )  ->  (
( [,] " {
z  e.  ran  F  |  ( [,] `  z
)  C_  A }
)  C_  ~P A  <->  A. w  e.  { z  e.  ran  F  | 
( [,] `  z
)  C_  A } 
( [,] `  w
)  e.  ~P A
) )
2612, 24, 25mp2an 672 . . . . 5  |-  ( ( [,] " { z  e.  ran  F  | 
( [,] `  z
)  C_  A }
)  C_  ~P A  <->  A. w  e.  { z  e.  ran  F  | 
( [,] `  z
)  C_  A } 
( [,] `  w
)  e.  ~P A
)
279, 26sylibr 212 . . . 4  |-  ( A  e.  ( topGen `  ran  (,) )  ->  ( [,] " { z  e.  ran  F  |  ( [,] `  z
)  C_  A }
)  C_  ~P A
)
28 sspwuni 4271 . . . 4  |-  ( ( [,] " { z  e.  ran  F  | 
( [,] `  z
)  C_  A }
)  C_  ~P A  <->  U. ( [,] " {
z  e.  ran  F  |  ( [,] `  z
)  C_  A }
)  C_  A )
2927, 28sylib 196 . . 3  |-  ( A  e.  ( topGen `  ran  (,) )  ->  U. ( [,] " { z  e. 
ran  F  |  ( [,] `  z )  C_  A } )  C_  A
)
30 eqid 2443 . . . . . . . 8  |-  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) )  =  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) )
3130rexmet 20383 . . . . . . 7  |-  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) )  e.  ( *Met `  RR )
32 eqid 2443 . . . . . . . . 9  |-  ( MetOpen `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) )  =  ( MetOpen `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) )
3330, 32tgioo 20388 . . . . . . . 8  |-  ( topGen ` 
ran  (,) )  =  (
MetOpen `  ( ( abs 
o.  -  )  |`  ( RR  X.  RR ) ) )
3433mopni2 20083 . . . . . . 7  |-  ( ( ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) )  e.  ( *Met `  RR )  /\  A  e.  ( topGen `  ran  (,) )  /\  w  e.  A
)  ->  E. r  e.  RR+  ( w (
ball `  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) r )  C_  A )
3531, 34mp3an1 1301 . . . . . 6  |-  ( ( A  e.  ( topGen ` 
ran  (,) )  /\  w  e.  A )  ->  E. r  e.  RR+  ( w (
ball `  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) r )  C_  A )
36 elssuni 4136 . . . . . . . . . . . 12  |-  ( A  e.  ( topGen `  ran  (,) )  ->  A  C_  U. ( topGen `
 ran  (,) )
)
37 uniretop 20356 . . . . . . . . . . . 12  |-  RR  =  U. ( topGen `  ran  (,) )
3836, 37syl6sseqr 3418 . . . . . . . . . . 11  |-  ( A  e.  ( topGen `  ran  (,) )  ->  A  C_  RR )
3938sselda 3371 . . . . . . . . . 10  |-  ( ( A  e.  ( topGen ` 
ran  (,) )  /\  w  e.  A )  ->  w  e.  RR )
40 rpre 11012 . . . . . . . . . 10  |-  ( r  e.  RR+  ->  r  e.  RR )
4130bl2ioo 20384 . . . . . . . . . 10  |-  ( ( w  e.  RR  /\  r  e.  RR )  ->  ( w ( ball `  ( ( abs  o.  -  )  |`  ( RR 
X.  RR ) ) ) r )  =  ( ( w  -  r ) (,) (
w  +  r ) ) )
4239, 40, 41syl2an 477 . . . . . . . . 9  |-  ( ( ( A  e.  (
topGen `  ran  (,) )  /\  w  e.  A
)  /\  r  e.  RR+ )  ->  ( w
( ball `  ( ( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) r )  =  ( ( w  -  r ) (,) ( w  +  r ) ) )
4342sseq1d 3398 . . . . . . . 8  |-  ( ( ( A  e.  (
topGen `  ran  (,) )  /\  w  e.  A
)  /\  r  e.  RR+ )  ->  ( (
w ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) r )  C_  A  <->  ( (
w  -  r ) (,) ( w  +  r ) )  C_  A ) )
44 2re 10406 . . . . . . . . . . . 12  |-  2  e.  RR
45 1lt2 10503 . . . . . . . . . . . 12  |-  1  <  2
46 expnlbnd 12009 . . . . . . . . . . . 12  |-  ( ( r  e.  RR+  /\  2  e.  RR  /\  1  <  2 )  ->  E. n  e.  NN  ( 1  / 
( 2 ^ n
) )  <  r
)
4744, 45, 46mp3an23 1306 . . . . . . . . . . 11  |-  ( r  e.  RR+  ->  E. n  e.  NN  ( 1  / 
( 2 ^ n
) )  <  r
)
4847ad2antrl 727 . . . . . . . . . 10  |-  ( ( ( A  e.  (
topGen `  ran  (,) )  /\  w  e.  A
)  /\  ( r  e.  RR+  /\  ( ( w  -  r ) (,) ( w  +  r ) )  C_  A ) )  ->  E. n  e.  NN  ( 1  /  (
2 ^ n ) )  <  r )
4939ad2antrr 725 . . . . . . . . . . . . 13  |-  ( ( ( ( A  e.  ( topGen `  ran  (,) )  /\  w  e.  A
)  /\  ( r  e.  RR+  /\  ( ( w  -  r ) (,) ( w  +  r ) )  C_  A ) )  /\  ( n  e.  NN  /\  ( 1  /  (
2 ^ n ) )  <  r ) )  ->  w  e.  RR )
50 2nn 10494 . . . . . . . . . . . . . . . . . . 19  |-  2  e.  NN
51 nnnn0 10601 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  e.  NN  ->  n  e.  NN0 )
5251ad2antrl 727 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( A  e.  ( topGen `  ran  (,) )  /\  w  e.  A
)  /\  ( r  e.  RR+  /\  ( ( w  -  r ) (,) ( w  +  r ) )  C_  A ) )  /\  ( n  e.  NN  /\  ( 1  /  (
2 ^ n ) )  <  r ) )  ->  n  e.  NN0 )
53 nnexpcl 11893 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 2  e.  NN  /\  n  e.  NN0 )  -> 
( 2 ^ n
)  e.  NN )
5450, 52, 53sylancr 663 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( A  e.  ( topGen `  ran  (,) )  /\  w  e.  A
)  /\  ( r  e.  RR+  /\  ( ( w  -  r ) (,) ( w  +  r ) )  C_  A ) )  /\  ( n  e.  NN  /\  ( 1  /  (
2 ^ n ) )  <  r ) )  ->  ( 2 ^ n )  e.  NN )
5554nnred 10352 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( A  e.  ( topGen `  ran  (,) )  /\  w  e.  A
)  /\  ( r  e.  RR+  /\  ( ( w  -  r ) (,) ( w  +  r ) )  C_  A ) )  /\  ( n  e.  NN  /\  ( 1  /  (
2 ^ n ) )  <  r ) )  ->  ( 2 ^ n )  e.  RR )
5649, 55remulcld 9429 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( A  e.  ( topGen `  ran  (,) )  /\  w  e.  A
)  /\  ( r  e.  RR+  /\  ( ( w  -  r ) (,) ( w  +  r ) )  C_  A ) )  /\  ( n  e.  NN  /\  ( 1  /  (
2 ^ n ) )  <  r ) )  ->  ( w  x.  ( 2 ^ n
) )  e.  RR )
57 fllelt 11662 . . . . . . . . . . . . . . . 16  |-  ( ( w  x.  ( 2 ^ n ) )  e.  RR  ->  (
( |_ `  (
w  x.  ( 2 ^ n ) ) )  <_  ( w  x.  ( 2 ^ n
) )  /\  (
w  x.  ( 2 ^ n ) )  <  ( ( |_
`  ( w  x.  ( 2 ^ n
) ) )  +  1 ) ) )
5856, 57syl 16 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A  e.  ( topGen `  ran  (,) )  /\  w  e.  A
)  /\  ( r  e.  RR+  /\  ( ( w  -  r ) (,) ( w  +  r ) )  C_  A ) )  /\  ( n  e.  NN  /\  ( 1  /  (
2 ^ n ) )  <  r ) )  ->  ( ( |_ `  ( w  x.  ( 2 ^ n
) ) )  <_ 
( w  x.  (
2 ^ n ) )  /\  ( w  x.  ( 2 ^ n ) )  < 
( ( |_ `  ( w  x.  (
2 ^ n ) ) )  +  1 ) ) )
5958simpld 459 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  ( topGen `  ran  (,) )  /\  w  e.  A
)  /\  ( r  e.  RR+  /\  ( ( w  -  r ) (,) ( w  +  r ) )  C_  A ) )  /\  ( n  e.  NN  /\  ( 1  /  (
2 ^ n ) )  <  r ) )  ->  ( |_ `  ( w  x.  (
2 ^ n ) ) )  <_  (
w  x.  ( 2 ^ n ) ) )
60 reflcl 11661 . . . . . . . . . . . . . . . 16  |-  ( ( w  x.  ( 2 ^ n ) )  e.  RR  ->  ( |_ `  ( w  x.  ( 2 ^ n
) ) )  e.  RR )
6156, 60syl 16 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A  e.  ( topGen `  ran  (,) )  /\  w  e.  A
)  /\  ( r  e.  RR+  /\  ( ( w  -  r ) (,) ( w  +  r ) )  C_  A ) )  /\  ( n  e.  NN  /\  ( 1  /  (
2 ^ n ) )  <  r ) )  ->  ( |_ `  ( w  x.  (
2 ^ n ) ) )  e.  RR )
6254nngt0d 10380 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A  e.  ( topGen `  ran  (,) )  /\  w  e.  A
)  /\  ( r  e.  RR+  /\  ( ( w  -  r ) (,) ( w  +  r ) )  C_  A ) )  /\  ( n  e.  NN  /\  ( 1  /  (
2 ^ n ) )  <  r ) )  ->  0  <  ( 2 ^ n ) )
63 ledivmul2 10224 . . . . . . . . . . . . . . 15  |-  ( ( ( |_ `  (
w  x.  ( 2 ^ n ) ) )  e.  RR  /\  w  e.  RR  /\  (
( 2 ^ n
)  e.  RR  /\  0  <  ( 2 ^ n ) ) )  ->  ( ( ( |_ `  ( w  x.  ( 2 ^ n ) ) )  /  ( 2 ^ n ) )  <_  w 
<->  ( |_ `  (
w  x.  ( 2 ^ n ) ) )  <_  ( w  x.  ( 2 ^ n
) ) ) )
6461, 49, 55, 62, 63syl112anc 1222 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  ( topGen `  ran  (,) )  /\  w  e.  A
)  /\  ( r  e.  RR+  /\  ( ( w  -  r ) (,) ( w  +  r ) )  C_  A ) )  /\  ( n  e.  NN  /\  ( 1  /  (
2 ^ n ) )  <  r ) )  ->  ( (
( |_ `  (
w  x.  ( 2 ^ n ) ) )  /  ( 2 ^ n ) )  <_  w  <->  ( |_ `  ( w  x.  (
2 ^ n ) ) )  <_  (
w  x.  ( 2 ^ n ) ) ) )
6559, 64mpbird 232 . . . . . . . . . . . . 13  |-  ( ( ( ( A  e.  ( topGen `  ran  (,) )  /\  w  e.  A
)  /\  ( r  e.  RR+  /\  ( ( w  -  r ) (,) ( w  +  r ) )  C_  A ) )  /\  ( n  e.  NN  /\  ( 1  /  (
2 ^ n ) )  <  r ) )  ->  ( ( |_ `  ( w  x.  ( 2 ^ n
) ) )  / 
( 2 ^ n
) )  <_  w
)
66 peano2re 9557 . . . . . . . . . . . . . . . 16  |-  ( ( |_ `  ( w  x.  ( 2 ^ n ) ) )  e.  RR  ->  (
( |_ `  (
w  x.  ( 2 ^ n ) ) )  +  1 )  e.  RR )
6761, 66syl 16 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A  e.  ( topGen `  ran  (,) )  /\  w  e.  A
)  /\  ( r  e.  RR+  /\  ( ( w  -  r ) (,) ( w  +  r ) )  C_  A ) )  /\  ( n  e.  NN  /\  ( 1  /  (
2 ^ n ) )  <  r ) )  ->  ( ( |_ `  ( w  x.  ( 2 ^ n
) ) )  +  1 )  e.  RR )
6867, 54nndivred 10385 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  ( topGen `  ran  (,) )  /\  w  e.  A
)  /\  ( r  e.  RR+  /\  ( ( w  -  r ) (,) ( w  +  r ) )  C_  A ) )  /\  ( n  e.  NN  /\  ( 1  /  (
2 ^ n ) )  <  r ) )  ->  ( (
( |_ `  (
w  x.  ( 2 ^ n ) ) )  +  1 )  /  ( 2 ^ n ) )  e.  RR )
6958simprd 463 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A  e.  ( topGen `  ran  (,) )  /\  w  e.  A
)  /\  ( r  e.  RR+  /\  ( ( w  -  r ) (,) ( w  +  r ) )  C_  A ) )  /\  ( n  e.  NN  /\  ( 1  /  (
2 ^ n ) )  <  r ) )  ->  ( w  x.  ( 2 ^ n
) )  <  (
( |_ `  (
w  x.  ( 2 ^ n ) ) )  +  1 ) )
70 ltmuldiv 10217 . . . . . . . . . . . . . . . 16  |-  ( ( w  e.  RR  /\  ( ( |_ `  ( w  x.  (
2 ^ n ) ) )  +  1 )  e.  RR  /\  ( ( 2 ^ n )  e.  RR  /\  0  <  ( 2 ^ n ) ) )  ->  ( (
w  x.  ( 2 ^ n ) )  <  ( ( |_
`  ( w  x.  ( 2 ^ n
) ) )  +  1 )  <->  w  <  ( ( ( |_ `  ( w  x.  (
2 ^ n ) ) )  +  1 )  /  ( 2 ^ n ) ) ) )
7149, 67, 55, 62, 70syl112anc 1222 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A  e.  ( topGen `  ran  (,) )  /\  w  e.  A
)  /\  ( r  e.  RR+  /\  ( ( w  -  r ) (,) ( w  +  r ) )  C_  A ) )  /\  ( n  e.  NN  /\  ( 1  /  (
2 ^ n ) )  <  r ) )  ->  ( (
w  x.  ( 2 ^ n ) )  <  ( ( |_
`  ( w  x.  ( 2 ^ n
) ) )  +  1 )  <->  w  <  ( ( ( |_ `  ( w  x.  (
2 ^ n ) ) )  +  1 )  /  ( 2 ^ n ) ) ) )
7269, 71mpbid 210 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  ( topGen `  ran  (,) )  /\  w  e.  A
)  /\  ( r  e.  RR+  /\  ( ( w  -  r ) (,) ( w  +  r ) )  C_  A ) )  /\  ( n  e.  NN  /\  ( 1  /  (
2 ^ n ) )  <  r ) )  ->  w  <  ( ( ( |_ `  ( w  x.  (
2 ^ n ) ) )  +  1 )  /  ( 2 ^ n ) ) )
7349, 68, 72ltled 9537 . . . . . . . . . . . . 13  |-  ( ( ( ( A  e.  ( topGen `  ran  (,) )  /\  w  e.  A
)  /\  ( r  e.  RR+  /\  ( ( w  -  r ) (,) ( w  +  r ) )  C_  A ) )  /\  ( n  e.  NN  /\  ( 1  /  (
2 ^ n ) )  <  r ) )  ->  w  <_  ( ( ( |_ `  ( w  x.  (
2 ^ n ) ) )  +  1 )  /  ( 2 ^ n ) ) )
7461, 54nndivred 10385 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  ( topGen `  ran  (,) )  /\  w  e.  A
)  /\  ( r  e.  RR+  /\  ( ( w  -  r ) (,) ( w  +  r ) )  C_  A ) )  /\  ( n  e.  NN  /\  ( 1  /  (
2 ^ n ) )  <  r ) )  ->  ( ( |_ `  ( w  x.  ( 2 ^ n
) ) )  / 
( 2 ^ n
) )  e.  RR )
75 elicc2 11375 . . . . . . . . . . . . . 14  |-  ( ( ( ( |_ `  ( w  x.  (
2 ^ n ) ) )  /  (
2 ^ n ) )  e.  RR  /\  ( ( ( |_
`  ( w  x.  ( 2 ^ n
) ) )  +  1 )  /  (
2 ^ n ) )  e.  RR )  ->  ( w  e.  ( ( ( |_
`  ( w  x.  ( 2 ^ n
) ) )  / 
( 2 ^ n
) ) [,] (
( ( |_ `  ( w  x.  (
2 ^ n ) ) )  +  1 )  /  ( 2 ^ n ) ) )  <->  ( w  e.  RR  /\  ( ( |_ `  ( w  x.  ( 2 ^ n ) ) )  /  ( 2 ^ n ) )  <_  w  /\  w  <_  (
( ( |_ `  ( w  x.  (
2 ^ n ) ) )  +  1 )  /  ( 2 ^ n ) ) ) ) )
7674, 68, 75syl2anc 661 . . . . . . . . . . . . 13  |-  ( ( ( ( A  e.  ( topGen `  ran  (,) )  /\  w  e.  A
)  /\  ( r  e.  RR+  /\  ( ( w  -  r ) (,) ( w  +  r ) )  C_  A ) )  /\  ( n  e.  NN  /\  ( 1  /  (
2 ^ n ) )  <  r ) )  ->  ( w  e.  ( ( ( |_
`  ( w  x.  ( 2 ^ n
) ) )  / 
( 2 ^ n
) ) [,] (
( ( |_ `  ( w  x.  (
2 ^ n ) ) )  +  1 )  /  ( 2 ^ n ) ) )  <->  ( w  e.  RR  /\  ( ( |_ `  ( w  x.  ( 2 ^ n ) ) )  /  ( 2 ^ n ) )  <_  w  /\  w  <_  (
( ( |_ `  ( w  x.  (
2 ^ n ) ) )  +  1 )  /  ( 2 ^ n ) ) ) ) )
7749, 65, 73, 76mpbir3and 1171 . . . . . . . . . . . 12  |-  ( ( ( ( A  e.  ( topGen `  ran  (,) )  /\  w  e.  A
)  /\  ( r  e.  RR+  /\  ( ( w  -  r ) (,) ( w  +  r ) )  C_  A ) )  /\  ( n  e.  NN  /\  ( 1  /  (
2 ^ n ) )  <  r ) )  ->  w  e.  ( ( ( |_
`  ( w  x.  ( 2 ^ n
) ) )  / 
( 2 ^ n
) ) [,] (
( ( |_ `  ( w  x.  (
2 ^ n ) ) )  +  1 )  /  ( 2 ^ n ) ) ) )
7856flcld 11663 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A  e.  ( topGen `  ran  (,) )  /\  w  e.  A
)  /\  ( r  e.  RR+  /\  ( ( w  -  r ) (,) ( w  +  r ) )  C_  A ) )  /\  ( n  e.  NN  /\  ( 1  /  (
2 ^ n ) )  <  r ) )  ->  ( |_ `  ( w  x.  (
2 ^ n ) ) )  e.  ZZ )
7914dyadval 21087 . . . . . . . . . . . . . . 15  |-  ( ( ( |_ `  (
w  x.  ( 2 ^ n ) ) )  e.  ZZ  /\  n  e.  NN0 )  -> 
( ( |_ `  ( w  x.  (
2 ^ n ) ) ) F n )  =  <. (
( |_ `  (
w  x.  ( 2 ^ n ) ) )  /  ( 2 ^ n ) ) ,  ( ( ( |_ `  ( w  x.  ( 2 ^ n ) ) )  +  1 )  / 
( 2 ^ n
) ) >. )
8078, 52, 79syl2anc 661 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  ( topGen `  ran  (,) )  /\  w  e.  A
)  /\  ( r  e.  RR+  /\  ( ( w  -  r ) (,) ( w  +  r ) )  C_  A ) )  /\  ( n  e.  NN  /\  ( 1  /  (
2 ^ n ) )  <  r ) )  ->  ( ( |_ `  ( w  x.  ( 2 ^ n
) ) ) F n )  =  <. ( ( |_ `  (
w  x.  ( 2 ^ n ) ) )  /  ( 2 ^ n ) ) ,  ( ( ( |_ `  ( w  x.  ( 2 ^ n ) ) )  +  1 )  / 
( 2 ^ n
) ) >. )
8180fveq2d 5710 . . . . . . . . . . . . 13  |-  ( ( ( ( A  e.  ( topGen `  ran  (,) )  /\  w  e.  A
)  /\  ( r  e.  RR+  /\  ( ( w  -  r ) (,) ( w  +  r ) )  C_  A ) )  /\  ( n  e.  NN  /\  ( 1  /  (
2 ^ n ) )  <  r ) )  ->  ( [,] `  ( ( |_ `  ( w  x.  (
2 ^ n ) ) ) F n ) )  =  ( [,] `  <. (
( |_ `  (
w  x.  ( 2 ^ n ) ) )  /  ( 2 ^ n ) ) ,  ( ( ( |_ `  ( w  x.  ( 2 ^ n ) ) )  +  1 )  / 
( 2 ^ n
) ) >. )
)
82 df-ov 6109 . . . . . . . . . . . . 13  |-  ( ( ( |_ `  (
w  x.  ( 2 ^ n ) ) )  /  ( 2 ^ n ) ) [,] ( ( ( |_ `  ( w  x.  ( 2 ^ n ) ) )  +  1 )  / 
( 2 ^ n
) ) )  =  ( [,] `  <. ( ( |_ `  (
w  x.  ( 2 ^ n ) ) )  /  ( 2 ^ n ) ) ,  ( ( ( |_ `  ( w  x.  ( 2 ^ n ) ) )  +  1 )  / 
( 2 ^ n
) ) >. )
8381, 82syl6eqr 2493 . . . . . . . . . . . 12  |-  ( ( ( ( A  e.  ( topGen `  ran  (,) )  /\  w  e.  A
)  /\  ( r  e.  RR+  /\  ( ( w  -  r ) (,) ( w  +  r ) )  C_  A ) )  /\  ( n  e.  NN  /\  ( 1  /  (
2 ^ n ) )  <  r ) )  ->  ( [,] `  ( ( |_ `  ( w  x.  (
2 ^ n ) ) ) F n ) )  =  ( ( ( |_ `  ( w  x.  (
2 ^ n ) ) )  /  (
2 ^ n ) ) [,] ( ( ( |_ `  (
w  x.  ( 2 ^ n ) ) )  +  1 )  /  ( 2 ^ n ) ) ) )
8477, 83eleqtrrd 2520 . . . . . . . . . . 11  |-  ( ( ( ( A  e.  ( topGen `  ran  (,) )  /\  w  e.  A
)  /\  ( r  e.  RR+  /\  ( ( w  -  r ) (,) ( w  +  r ) )  C_  A ) )  /\  ( n  e.  NN  /\  ( 1  /  (
2 ^ n ) )  <  r ) )  ->  w  e.  ( [,] `  ( ( |_ `  ( w  x.  ( 2 ^ n ) ) ) F n ) ) )
85 ffn 5574 . . . . . . . . . . . . . . . 16  |-  ( F : ( ZZ  X.  NN0 ) --> (  <_  i^i  ( RR  X.  RR ) )  ->  F  Fn  ( ZZ  X.  NN0 ) )
8615, 85ax-mp 5 . . . . . . . . . . . . . . 15  |-  F  Fn  ( ZZ  X.  NN0 )
87 fnovrn 6253 . . . . . . . . . . . . . . 15  |-  ( ( F  Fn  ( ZZ 
X.  NN0 )  /\  ( |_ `  ( w  x.  ( 2 ^ n
) ) )  e.  ZZ  /\  n  e. 
NN0 )  ->  (
( |_ `  (
w  x.  ( 2 ^ n ) ) ) F n )  e.  ran  F )
8886, 87mp3an1 1301 . . . . . . . . . . . . . 14  |-  ( ( ( |_ `  (
w  x.  ( 2 ^ n ) ) )  e.  ZZ  /\  n  e.  NN0 )  -> 
( ( |_ `  ( w  x.  (
2 ^ n ) ) ) F n )  e.  ran  F
)
8978, 52, 88syl2anc 661 . . . . . . . . . . . . 13  |-  ( ( ( ( A  e.  ( topGen `  ran  (,) )  /\  w  e.  A
)  /\  ( r  e.  RR+  /\  ( ( w  -  r ) (,) ( w  +  r ) )  C_  A ) )  /\  ( n  e.  NN  /\  ( 1  /  (
2 ^ n ) )  <  r ) )  ->  ( ( |_ `  ( w  x.  ( 2 ^ n
) ) ) F n )  e.  ran  F )
90 simplrl 759 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( A  e.  ( topGen `  ran  (,) )  /\  w  e.  A
)  /\  ( r  e.  RR+  /\  ( ( w  -  r ) (,) ( w  +  r ) )  C_  A ) )  /\  ( n  e.  NN  /\  ( 1  /  (
2 ^ n ) )  <  r ) )  ->  r  e.  RR+ )
9190rpred 11042 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( A  e.  ( topGen `  ran  (,) )  /\  w  e.  A
)  /\  ( r  e.  RR+  /\  ( ( w  -  r ) (,) ( w  +  r ) )  C_  A ) )  /\  ( n  e.  NN  /\  ( 1  /  (
2 ^ n ) )  <  r ) )  ->  r  e.  RR )
9249, 91resubcld 9791 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( A  e.  ( topGen `  ran  (,) )  /\  w  e.  A
)  /\  ( r  e.  RR+  /\  ( ( w  -  r ) (,) ( w  +  r ) )  C_  A ) )  /\  ( n  e.  NN  /\  ( 1  /  (
2 ^ n ) )  <  r ) )  ->  ( w  -  r )  e.  RR )
9392rexrd 9448 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( A  e.  ( topGen `  ran  (,) )  /\  w  e.  A
)  /\  ( r  e.  RR+  /\  ( ( w  -  r ) (,) ( w  +  r ) )  C_  A ) )  /\  ( n  e.  NN  /\  ( 1  /  (
2 ^ n ) )  <  r ) )  ->  ( w  -  r )  e. 
RR* )
9449, 91readdcld 9428 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( A  e.  ( topGen `  ran  (,) )  /\  w  e.  A
)  /\  ( r  e.  RR+  /\  ( ( w  -  r ) (,) ( w  +  r ) )  C_  A ) )  /\  ( n  e.  NN  /\  ( 1  /  (
2 ^ n ) )  <  r ) )  ->  ( w  +  r )  e.  RR )
9594rexrd 9448 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( A  e.  ( topGen `  ran  (,) )  /\  w  e.  A
)  /\  ( r  e.  RR+  /\  ( ( w  -  r ) (,) ( w  +  r ) )  C_  A ) )  /\  ( n  e.  NN  /\  ( 1  /  (
2 ^ n ) )  <  r ) )  ->  ( w  +  r )  e. 
RR* )
9674, 91readdcld 9428 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( A  e.  ( topGen `  ran  (,) )  /\  w  e.  A
)  /\  ( r  e.  RR+  /\  ( ( w  -  r ) (,) ( w  +  r ) )  C_  A ) )  /\  ( n  e.  NN  /\  ( 1  /  (
2 ^ n ) )  <  r ) )  ->  ( (
( |_ `  (
w  x.  ( 2 ^ n ) ) )  /  ( 2 ^ n ) )  +  r )  e.  RR )
9761recnd 9427 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( A  e.  ( topGen `  ran  (,) )  /\  w  e.  A
)  /\  ( r  e.  RR+  /\  ( ( w  -  r ) (,) ( w  +  r ) )  C_  A ) )  /\  ( n  e.  NN  /\  ( 1  /  (
2 ^ n ) )  <  r ) )  ->  ( |_ `  ( w  x.  (
2 ^ n ) ) )  e.  CC )
98 1cnd 9417 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( A  e.  ( topGen `  ran  (,) )  /\  w  e.  A
)  /\  ( r  e.  RR+  /\  ( ( w  -  r ) (,) ( w  +  r ) )  C_  A ) )  /\  ( n  e.  NN  /\  ( 1  /  (
2 ^ n ) )  <  r ) )  ->  1  e.  CC )
9955recnd 9427 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( A  e.  ( topGen `  ran  (,) )  /\  w  e.  A
)  /\  ( r  e.  RR+  /\  ( ( w  -  r ) (,) ( w  +  r ) )  C_  A ) )  /\  ( n  e.  NN  /\  ( 1  /  (
2 ^ n ) )  <  r ) )  ->  ( 2 ^ n )  e.  CC )
10054nnne0d 10381 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( A  e.  ( topGen `  ran  (,) )  /\  w  e.  A
)  /\  ( r  e.  RR+  /\  ( ( w  -  r ) (,) ( w  +  r ) )  C_  A ) )  /\  ( n  e.  NN  /\  ( 1  /  (
2 ^ n ) )  <  r ) )  ->  ( 2 ^ n )  =/=  0 )
10197, 98, 99, 100divdird 10160 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( A  e.  ( topGen `  ran  (,) )  /\  w  e.  A
)  /\  ( r  e.  RR+  /\  ( ( w  -  r ) (,) ( w  +  r ) )  C_  A ) )  /\  ( n  e.  NN  /\  ( 1  /  (
2 ^ n ) )  <  r ) )  ->  ( (
( |_ `  (
w  x.  ( 2 ^ n ) ) )  +  1 )  /  ( 2 ^ n ) )  =  ( ( ( |_
`  ( w  x.  ( 2 ^ n
) ) )  / 
( 2 ^ n
) )  +  ( 1  /  ( 2 ^ n ) ) ) )
10254nnrecred 10382 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( A  e.  ( topGen `  ran  (,) )  /\  w  e.  A
)  /\  ( r  e.  RR+  /\  ( ( w  -  r ) (,) ( w  +  r ) )  C_  A ) )  /\  ( n  e.  NN  /\  ( 1  /  (
2 ^ n ) )  <  r ) )  ->  ( 1  /  ( 2 ^ n ) )  e.  RR )
103 simprr 756 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( A  e.  ( topGen `  ran  (,) )  /\  w  e.  A
)  /\  ( r  e.  RR+  /\  ( ( w  -  r ) (,) ( w  +  r ) )  C_  A ) )  /\  ( n  e.  NN  /\  ( 1  /  (
2 ^ n ) )  <  r ) )  ->  ( 1  /  ( 2 ^ n ) )  < 
r )
104102, 91, 74, 103ltadd2dd 9545 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( A  e.  ( topGen `  ran  (,) )  /\  w  e.  A
)  /\  ( r  e.  RR+  /\  ( ( w  -  r ) (,) ( w  +  r ) )  C_  A ) )  /\  ( n  e.  NN  /\  ( 1  /  (
2 ^ n ) )  <  r ) )  ->  ( (
( |_ `  (
w  x.  ( 2 ^ n ) ) )  /  ( 2 ^ n ) )  +  ( 1  / 
( 2 ^ n
) ) )  < 
( ( ( |_
`  ( w  x.  ( 2 ^ n
) ) )  / 
( 2 ^ n
) )  +  r ) )
105101, 104eqbrtrd 4327 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( A  e.  ( topGen `  ran  (,) )  /\  w  e.  A
)  /\  ( r  e.  RR+  /\  ( ( w  -  r ) (,) ( w  +  r ) )  C_  A ) )  /\  ( n  e.  NN  /\  ( 1  /  (
2 ^ n ) )  <  r ) )  ->  ( (
( |_ `  (
w  x.  ( 2 ^ n ) ) )  +  1 )  /  ( 2 ^ n ) )  < 
( ( ( |_
`  ( w  x.  ( 2 ^ n
) ) )  / 
( 2 ^ n
) )  +  r ) )
10649, 68, 96, 72, 105lttrd 9547 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( A  e.  ( topGen `  ran  (,) )  /\  w  e.  A
)  /\  ( r  e.  RR+  /\  ( ( w  -  r ) (,) ( w  +  r ) )  C_  A ) )  /\  ( n  e.  NN  /\  ( 1  /  (
2 ^ n ) )  <  r ) )  ->  w  <  ( ( ( |_ `  ( w  x.  (
2 ^ n ) ) )  /  (
2 ^ n ) )  +  r ) )
10749, 91, 74ltsubaddd 9950 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( A  e.  ( topGen `  ran  (,) )  /\  w  e.  A
)  /\  ( r  e.  RR+  /\  ( ( w  -  r ) (,) ( w  +  r ) )  C_  A ) )  /\  ( n  e.  NN  /\  ( 1  /  (
2 ^ n ) )  <  r ) )  ->  ( (
w  -  r )  <  ( ( |_
`  ( w  x.  ( 2 ^ n
) ) )  / 
( 2 ^ n
) )  <->  w  <  ( ( ( |_ `  ( w  x.  (
2 ^ n ) ) )  /  (
2 ^ n ) )  +  r ) ) )
108106, 107mpbird 232 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( A  e.  ( topGen `  ran  (,) )  /\  w  e.  A
)  /\  ( r  e.  RR+  /\  ( ( w  -  r ) (,) ( w  +  r ) )  C_  A ) )  /\  ( n  e.  NN  /\  ( 1  /  (
2 ^ n ) )  <  r ) )  ->  ( w  -  r )  < 
( ( |_ `  ( w  x.  (
2 ^ n ) ) )  /  (
2 ^ n ) ) )
10949, 102readdcld 9428 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( A  e.  ( topGen `  ran  (,) )  /\  w  e.  A
)  /\  ( r  e.  RR+  /\  ( ( w  -  r ) (,) ( w  +  r ) )  C_  A ) )  /\  ( n  e.  NN  /\  ( 1  /  (
2 ^ n ) )  <  r ) )  ->  ( w  +  ( 1  / 
( 2 ^ n
) ) )  e.  RR )
11074, 49, 102, 65leadd1dd 9968 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( A  e.  ( topGen `  ran  (,) )  /\  w  e.  A
)  /\  ( r  e.  RR+  /\  ( ( w  -  r ) (,) ( w  +  r ) )  C_  A ) )  /\  ( n  e.  NN  /\  ( 1  /  (
2 ^ n ) )  <  r ) )  ->  ( (
( |_ `  (
w  x.  ( 2 ^ n ) ) )  /  ( 2 ^ n ) )  +  ( 1  / 
( 2 ^ n
) ) )  <_ 
( w  +  ( 1  /  ( 2 ^ n ) ) ) )
111101, 110eqbrtrd 4327 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( A  e.  ( topGen `  ran  (,) )  /\  w  e.  A
)  /\  ( r  e.  RR+  /\  ( ( w  -  r ) (,) ( w  +  r ) )  C_  A ) )  /\  ( n  e.  NN  /\  ( 1  /  (
2 ^ n ) )  <  r ) )  ->  ( (
( |_ `  (
w  x.  ( 2 ^ n ) ) )  +  1 )  /  ( 2 ^ n ) )  <_ 
( w  +  ( 1  /  ( 2 ^ n ) ) ) )
112102, 91, 49, 103ltadd2dd 9545 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( A  e.  ( topGen `  ran  (,) )  /\  w  e.  A
)  /\  ( r  e.  RR+  /\  ( ( w  -  r ) (,) ( w  +  r ) )  C_  A ) )  /\  ( n  e.  NN  /\  ( 1  /  (
2 ^ n ) )  <  r ) )  ->  ( w  +  ( 1  / 
( 2 ^ n
) ) )  < 
( w  +  r ) )
11368, 109, 94, 111, 112lelttrd 9544 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( A  e.  ( topGen `  ran  (,) )  /\  w  e.  A
)  /\  ( r  e.  RR+  /\  ( ( w  -  r ) (,) ( w  +  r ) )  C_  A ) )  /\  ( n  e.  NN  /\  ( 1  /  (
2 ^ n ) )  <  r ) )  ->  ( (
( |_ `  (
w  x.  ( 2 ^ n ) ) )  +  1 )  /  ( 2 ^ n ) )  < 
( w  +  r ) )
114 iccssioo 11379 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( w  -  r )  e.  RR*  /\  ( w  +  r )  e.  RR* )  /\  ( ( w  -  r )  <  (
( |_ `  (
w  x.  ( 2 ^ n ) ) )  /  ( 2 ^ n ) )  /\  ( ( ( |_ `  ( w  x.  ( 2 ^ n ) ) )  +  1 )  / 
( 2 ^ n
) )  <  (
w  +  r ) ) )  ->  (
( ( |_ `  ( w  x.  (
2 ^ n ) ) )  /  (
2 ^ n ) ) [,] ( ( ( |_ `  (
w  x.  ( 2 ^ n ) ) )  +  1 )  /  ( 2 ^ n ) ) ) 
C_  ( ( w  -  r ) (,) ( w  +  r ) ) )
11593, 95, 108, 113, 114syl22anc 1219 . . . . . . . . . . . . . . 15  |-  ( ( ( ( A  e.  ( topGen `  ran  (,) )  /\  w  e.  A
)  /\  ( r  e.  RR+  /\  ( ( w  -  r ) (,) ( w  +  r ) )  C_  A ) )  /\  ( n  e.  NN  /\  ( 1  /  (
2 ^ n ) )  <  r ) )  ->  ( (
( |_ `  (
w  x.  ( 2 ^ n ) ) )  /  ( 2 ^ n ) ) [,] ( ( ( |_ `  ( w  x.  ( 2 ^ n ) ) )  +  1 )  / 
( 2 ^ n
) ) )  C_  ( ( w  -  r ) (,) (
w  +  r ) ) )
11683, 115eqsstrd 3405 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  ( topGen `  ran  (,) )  /\  w  e.  A
)  /\  ( r  e.  RR+  /\  ( ( w  -  r ) (,) ( w  +  r ) )  C_  A ) )  /\  ( n  e.  NN  /\  ( 1  /  (
2 ^ n ) )  <  r ) )  ->  ( [,] `  ( ( |_ `  ( w  x.  (
2 ^ n ) ) ) F n ) )  C_  (
( w  -  r
) (,) ( w  +  r ) ) )
117 simplrr 760 . . . . . . . . . . . . . 14  |-  ( ( ( ( A  e.  ( topGen `  ran  (,) )  /\  w  e.  A
)  /\  ( r  e.  RR+  /\  ( ( w  -  r ) (,) ( w  +  r ) )  C_  A ) )  /\  ( n  e.  NN  /\  ( 1  /  (
2 ^ n ) )  <  r ) )  ->  ( (
w  -  r ) (,) ( w  +  r ) )  C_  A )
118116, 117sstrd 3381 . . . . . . . . . . . . 13  |-  ( ( ( ( A  e.  ( topGen `  ran  (,) )  /\  w  e.  A
)  /\  ( r  e.  RR+  /\  ( ( w  -  r ) (,) ( w  +  r ) )  C_  A ) )  /\  ( n  e.  NN  /\  ( 1  /  (
2 ^ n ) )  <  r ) )  ->  ( [,] `  ( ( |_ `  ( w  x.  (
2 ^ n ) ) ) F n ) )  C_  A
)
119 fveq2 5706 . . . . . . . . . . . . . . 15  |-  ( z  =  ( ( |_
`  ( w  x.  ( 2 ^ n
) ) ) F n )  ->  ( [,] `  z )  =  ( [,] `  (
( |_ `  (
w  x.  ( 2 ^ n ) ) ) F n ) ) )
120119sseq1d 3398 . . . . . . . . . . . . . 14  |-  ( z  =  ( ( |_
`  ( w  x.  ( 2 ^ n
) ) ) F n )  ->  (
( [,] `  z
)  C_  A  <->  ( [,] `  ( ( |_ `  ( w  x.  (
2 ^ n ) ) ) F n ) )  C_  A
) )
121120elrab 3132 . . . . . . . . . . . . 13  |-  ( ( ( |_ `  (
w  x.  ( 2 ^ n ) ) ) F n )  e.  { z  e. 
ran  F  |  ( [,] `  z )  C_  A }  <->  ( ( ( |_ `  ( w  x.  ( 2 ^ n ) ) ) F n )  e. 
ran  F  /\  ( [,] `  ( ( |_
`  ( w  x.  ( 2 ^ n
) ) ) F n ) )  C_  A ) )
12289, 118, 121sylanbrc 664 . . . . . . . . . . . 12  |-  ( ( ( ( A  e.  ( topGen `  ran  (,) )  /\  w  e.  A
)  /\  ( r  e.  RR+  /\  ( ( w  -  r ) (,) ( w  +  r ) )  C_  A ) )  /\  ( n  e.  NN  /\  ( 1  /  (
2 ^ n ) )  <  r ) )  ->  ( ( |_ `  ( w  x.  ( 2 ^ n
) ) ) F n )  e.  {
z  e.  ran  F  |  ( [,] `  z
)  C_  A }
)
123 funfvima2 5968 . . . . . . . . . . . . 13  |-  ( ( Fun  [,]  /\  { z  e.  ran  F  | 
( [,] `  z
)  C_  A }  C_ 
dom  [,] )  ->  (
( ( |_ `  ( w  x.  (
2 ^ n ) ) ) F n )  e.  { z  e.  ran  F  | 
( [,] `  z
)  C_  A }  ->  ( [,] `  (
( |_ `  (
w  x.  ( 2 ^ n ) ) ) F n ) )  e.  ( [,] " { z  e.  ran  F  |  ( [,] `  z
)  C_  A }
) ) )
12412, 24, 123mp2an 672 . . . . . . . . . . . 12  |-  ( ( ( |_ `  (
w  x.  ( 2 ^ n ) ) ) F n )  e.  { z  e. 
ran  F  |  ( [,] `  z )  C_  A }  ->  ( [,] `  ( ( |_ `  ( w  x.  (
2 ^ n ) ) ) F n ) )  e.  ( [,] " { z  e.  ran  F  | 
( [,] `  z
)  C_  A }
) )
125122, 124syl 16 . . . . . . . . . . 11  |-  ( ( ( ( A  e.  ( topGen `  ran  (,) )  /\  w  e.  A
)  /\  ( r  e.  RR+  /\  ( ( w  -  r ) (,) ( w  +  r ) )  C_  A ) )  /\  ( n  e.  NN  /\  ( 1  /  (
2 ^ n ) )  <  r ) )  ->  ( [,] `  ( ( |_ `  ( w  x.  (
2 ^ n ) ) ) F n ) )  e.  ( [,] " { z  e.  ran  F  | 
( [,] `  z
)  C_  A }
) )
126 elunii 4111 . . . . . . . . . . 11  |-  ( ( w  e.  ( [,] `  ( ( |_ `  ( w  x.  (
2 ^ n ) ) ) F n ) )  /\  ( [,] `  ( ( |_
`  ( w  x.  ( 2 ^ n
) ) ) F n ) )  e.  ( [,] " {
z  e.  ran  F  |  ( [,] `  z
)  C_  A }
) )  ->  w  e.  U. ( [,] " {
z  e.  ran  F  |  ( [,] `  z
)  C_  A }
) )
12784, 125, 126syl2anc 661 . . . . . . . . . 10  |-  ( ( ( ( A  e.  ( topGen `  ran  (,) )  /\  w  e.  A
)  /\  ( r  e.  RR+  /\  ( ( w  -  r ) (,) ( w  +  r ) )  C_  A ) )  /\  ( n  e.  NN  /\  ( 1  /  (
2 ^ n ) )  <  r ) )  ->  w  e.  U. ( [,] " {
z  e.  ran  F  |  ( [,] `  z
)  C_  A }
) )
12848, 127rexlimddv 2860 . . . . . . . . 9  |-  ( ( ( A  e.  (
topGen `  ran  (,) )  /\  w  e.  A
)  /\  ( r  e.  RR+  /\  ( ( w  -  r ) (,) ( w  +  r ) )  C_  A ) )  ->  w  e.  U. ( [,] " { z  e. 
ran  F  |  ( [,] `  z )  C_  A } ) )
129128expr 615 . . . . . . . 8  |-  ( ( ( A  e.  (
topGen `  ran  (,) )  /\  w  e.  A
)  /\  r  e.  RR+ )  ->  ( (
( w  -  r
) (,) ( w  +  r ) ) 
C_  A  ->  w  e.  U. ( [,] " {
z  e.  ran  F  |  ( [,] `  z
)  C_  A }
) ) )
13043, 129sylbid 215 . . . . . . 7  |-  ( ( ( A  e.  (
topGen `  ran  (,) )  /\  w  e.  A
)  /\  r  e.  RR+ )  ->  ( (
w ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) r )  C_  A  ->  w  e.  U. ( [,] " { z  e.  ran  F  |  ( [,] `  z
)  C_  A }
) ) )
131130rexlimdva 2856 . . . . . 6  |-  ( ( A  e.  ( topGen ` 
ran  (,) )  /\  w  e.  A )  ->  ( E. r  e.  RR+  (
w ( ball `  (
( abs  o.  -  )  |`  ( RR  X.  RR ) ) ) r )  C_  A  ->  w  e.  U. ( [,] " { z  e.  ran  F  |  ( [,] `  z
)  C_  A }
) ) )
13235, 131mpd 15 . . . . 5  |-  ( ( A  e.  ( topGen ` 
ran  (,) )  /\  w  e.  A )  ->  w  e.  U. ( [,] " {
z  e.  ran  F  |  ( [,] `  z
)  C_  A }
) )
133132ex 434 . . . 4  |-  ( A  e.  ( topGen `  ran  (,) )  ->  ( w  e.  A  ->  w  e. 
U. ( [,] " {
z  e.  ran  F  |  ( [,] `  z
)  C_  A }
) ) )
134133ssrdv 3377 . . 3  |-  ( A  e.  ( topGen `  ran  (,) )  ->  A  C_  U. ( [,] " { z  e. 
ran  F  |  ( [,] `  z )  C_  A } ) )
13529, 134eqssd 3388 . 2  |-  ( A  e.  ( topGen `  ran  (,) )  ->  U. ( [,] " { z  e. 
ran  F  |  ( [,] `  z )  C_  A } )  =  A )
136 fveq2 5706 . . . . . . 7  |-  ( c  =  a  ->  ( [,] `  c )  =  ( [,] `  a
) )
137136sseq1d 3398 . . . . . 6  |-  ( c  =  a  ->  (
( [,] `  c
)  C_  ( [,] `  b )  <->  ( [,] `  a )  C_  ( [,] `  b ) ) )
138 equequ1 1736 . . . . . 6  |-  ( c  =  a  ->  (
c  =  b  <->  a  =  b ) )
139137, 138imbi12d 320 . . . . 5  |-  ( c  =  a  ->  (
( ( [,] `  c
)  C_  ( [,] `  b )  ->  c  =  b )  <->  ( ( [,] `  a )  C_  ( [,] `  b )  ->  a  =  b ) ) )
140139ralbidv 2750 . . . 4  |-  ( c  =  a  ->  ( A. b  e.  { z  e.  ran  F  | 
( [,] `  z
)  C_  A } 
( ( [,] `  c
)  C_  ( [,] `  b )  ->  c  =  b )  <->  A. b  e.  { z  e.  ran  F  |  ( [,] `  z
)  C_  A } 
( ( [,] `  a
)  C_  ( [,] `  b )  ->  a  =  b ) ) )
141140cbvrabv 2986 . . 3  |-  { c  e.  { z  e. 
ran  F  |  ( [,] `  z )  C_  A }  |  A. b  e.  { z  e.  ran  F  |  ( [,] `  z ) 
C_  A }  (
( [,] `  c
)  C_  ( [,] `  b )  ->  c  =  b ) }  =  { a  e. 
{ z  e.  ran  F  |  ( [,] `  z
)  C_  A }  |  A. b  e.  {
z  e.  ran  F  |  ( [,] `  z
)  C_  A } 
( ( [,] `  a
)  C_  ( [,] `  b )  ->  a  =  b ) }
14213a1i 11 . . 3  |-  ( A  e.  ( topGen `  ran  (,) )  ->  { z  e.  ran  F  |  ( [,] `  z ) 
C_  A }  C_  ran  F )
14314, 141, 142dyadmbl 21095 . 2  |-  ( A  e.  ( topGen `  ran  (,) )  ->  U. ( [,] " { z  e. 
ran  F  |  ( [,] `  z )  C_  A } )  e.  dom  vol )
144135, 143eqeltrrd 2518 1  |-  ( A  e.  ( topGen `  ran  (,) )  ->  A  e.  dom  vol )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 965    = wceq 1369    e. wcel 1756   A.wral 2730   E.wrex 2731   {crab 2734    i^i cin 3342    C_ wss 3343   ~Pcpw 3875   <.cop 3898   U.cuni 4106   class class class wbr 4307    X. cxp 4853   dom cdm 4855   ran crn 4856    |` cres 4857   "cima 4858    o. ccom 4859   Fun wfun 5427    Fn wfn 5428   -->wf 5429   ` cfv 5433  (class class class)co 6106    e. cmpt2 6108   RRcr 9296   0cc0 9297   1c1 9298    + caddc 9300    x. cmul 9302   RR*cxr 9432    < clt 9433    <_ cle 9434    - cmin 9610    / cdiv 10008   NNcn 10337   2c2 10386   NN0cn0 10594   ZZcz 10661   RR+crp 11006   (,)cioo 11315   [,]cicc 11318   |_cfl 11655   ^cexp 11880   abscabs 12738   topGenctg 14391   *Metcxmt 17816   ballcbl 17818   MetOpencmopn 17821   volcvol 20962
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4418  ax-sep 4428  ax-nul 4436  ax-pow 4485  ax-pr 4546  ax-un 6387  ax-inf2 7862  ax-cnex 9353  ax-resscn 9354  ax-1cn 9355  ax-icn 9356  ax-addcl 9357  ax-addrcl 9358  ax-mulcl 9359  ax-mulrcl 9360  ax-mulcom 9361  ax-addass 9362  ax-mulass 9363  ax-distr 9364  ax-i2m1 9365  ax-1ne0 9366  ax-1rid 9367  ax-rnegex 9368  ax-rrecex 9369  ax-cnre 9370  ax-pre-lttri 9371  ax-pre-lttrn 9372  ax-pre-ltadd 9373  ax-pre-mulgt0 9374  ax-pre-sup 9375
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-fal 1375  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-nel 2623  df-ral 2735  df-rex 2736  df-reu 2737  df-rmo 2738  df-rab 2739  df-v 2989  df-sbc 3202  df-csb 3304  df-dif 3346  df-un 3348  df-in 3350  df-ss 3357  df-pss 3359  df-nul 3653  df-if 3807  df-pw 3877  df-sn 3893  df-pr 3895  df-tp 3897  df-op 3899  df-uni 4107  df-int 4144  df-iun 4188  df-disj 4278  df-br 4308  df-opab 4366  df-mpt 4367  df-tr 4401  df-eprel 4647  df-id 4651  df-po 4656  df-so 4657  df-fr 4694  df-se 4695  df-we 4696  df-ord 4737  df-on 4738  df-lim 4739  df-suc 4740  df-xp 4861  df-rel 4862  df-cnv 4863  df-co 4864  df-dm 4865  df-rn 4866  df-res 4867  df-ima 4868  df-iota 5396  df-fun 5435  df-fn 5436  df-f 5437  df-f1 5438  df-fo 5439  df-f1o 5440  df-fv 5441  df-isom 5442  df-riota 6067  df-ov 6109  df-oprab 6110  df-mpt2 6111  df-of 6335  df-om 6492  df-1st 6592  df-2nd 6593  df-recs 6847  df-rdg 6881  df-1o 6935  df-2o 6936  df-oadd 6939  df-omul 6940  df-er 7116  df-map 7231  df-pm 7232  df-en 7326  df-dom 7327  df-sdom 7328  df-fin 7329  df-fi 7676  df-sup 7706  df-oi 7739  df-card 8124  df-acn 8127  df-cda 8352  df-pnf 9435  df-mnf 9436  df-xr 9437  df-ltxr 9438  df-le 9439  df-sub 9612  df-neg 9613  df-div 10009  df-nn 10338  df-2 10395  df-3 10396  df-4 10397  df-n0 10595  df-z 10662  df-uz 10877  df-q 10969  df-rp 11007  df-xneg 11104  df-xadd 11105  df-xmul 11106  df-ioo 11319  df-ico 11321  df-icc 11322  df-fz 11453  df-fzo 11564  df-fl 11657  df-seq 11822  df-exp 11881  df-hash 12119  df-cj 12603  df-re 12604  df-im 12605  df-sqr 12739  df-abs 12740  df-clim 12981  df-rlim 12982  df-sum 13179  df-rest 14376  df-topgen 14397  df-psmet 17824  df-xmet 17825  df-met 17826  df-bl 17827  df-mopn 17828  df-top 18518  df-bases 18520  df-topon 18521  df-cmp 19005  df-ovol 20963  df-vol 20964
This theorem is referenced by:  opnmbl  21097
  Copyright terms: Public domain W3C validator