Metamath Proof Explorer

Theorem opnmbllem

Description: Lemma for opnmbl . (Contributed by Mario Carneiro, 26-Mar-2015)

Ref Expression
Hypothesis dyadmbl.1 
|- F = ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. )
Assertion opnmbllem 
|- ( A e. ( topGen ` ran (,) ) -> A e. dom vol )

Proof

Step Hyp Ref Expression
1 dyadmbl.1 
 |-  F = ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. )
2 fveq2 
 |-  ( z = w -> ( [,] ` z ) = ( [,] ` w ) )
3 2 sseq1d 
 |-  ( z = w -> ( ( [,] ` z ) C_ A <-> ( [,] ` w ) C_ A ) )
4 3 elrab 
 |-  ( w e. { z e. ran F | ( [,] ` z ) C_ A } <-> ( w e. ran F /\ ( [,] ` w ) C_ A ) )
5 simprr 
 |-  ( ( A e. ( topGen ` ran (,) ) /\ ( w e. ran F /\ ( [,] ` w ) C_ A ) ) -> ( [,] ` w ) C_ A )
6 fvex 
 |-  ( [,] ` w ) e. _V
7 6 elpw 
 |-  ( ( [,] ` w ) e. ~P A <-> ( [,] ` w ) C_ A )
8 5 7 sylibr 
 |-  ( ( A e. ( topGen ` ran (,) ) /\ ( w e. ran F /\ ( [,] ` w ) C_ A ) ) -> ( [,] ` w ) e. ~P A )
9 4 8 sylan2b 
 |-  ( ( A e. ( topGen ` ran (,) ) /\ w e. { z e. ran F | ( [,] ` z ) C_ A } ) -> ( [,] ` w ) e. ~P A )
10 9 ralrimiva 
 |-  ( A e. ( topGen ` ran (,) ) -> A. w e. { z e. ran F | ( [,] ` z ) C_ A } ( [,] ` w ) e. ~P A )
11 iccf 
 |-  [,] : ( RR* X. RR* ) --> ~P RR*
12 ffun 
 |-  ( [,] : ( RR* X. RR* ) --> ~P RR* -> Fun [,] )
13 11 12 ax-mp 
 |-  Fun [,]
14 ssrab2 
 |-  { z e. ran F | ( [,] ` z ) C_ A } C_ ran F
15 1 dyadf 
 |-  F : ( ZZ X. NN0 ) --> ( <_ i^i ( RR X. RR ) )
16 frn 
 |-  ( F : ( ZZ X. NN0 ) --> ( <_ i^i ( RR X. RR ) ) -> ran F C_ ( <_ i^i ( RR X. RR ) ) )
17 15 16 ax-mp 
 |-  ran F C_ ( <_ i^i ( RR X. RR ) )
18 inss2 
 |-  ( <_ i^i ( RR X. RR ) ) C_ ( RR X. RR )
19 rexpssxrxp 
 |-  ( RR X. RR ) C_ ( RR* X. RR* )
20 18 19 sstri 
 |-  ( <_ i^i ( RR X. RR ) ) C_ ( RR* X. RR* )
21 17 20 sstri 
 |-  ran F C_ ( RR* X. RR* )
22 14 21 sstri 
 |-  { z e. ran F | ( [,] ` z ) C_ A } C_ ( RR* X. RR* )
23 11 fdmi 
 |-  dom [,] = ( RR* X. RR* )
24 22 23 sseqtrri 
 |-  { z e. ran F | ( [,] ` z ) C_ A } C_ dom [,]
25 funimass4 
 |-  ( ( 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 ) )
26 13 24 25 mp2an 
 |-  ( ( [,] " { z e. ran F | ( [,] ` z ) C_ A } ) C_ ~P A <-> A. w e. { z e. ran F | ( [,] ` z ) C_ A } ( [,] ` w ) e. ~P A )
27 10 26 sylibr 
 |-  ( A e. ( topGen ` ran (,) ) -> ( [,] " { z e. ran F | ( [,] ` z ) C_ A } ) C_ ~P A )
28 sspwuni 
 |-  ( ( [,] " { z e. ran F | ( [,] ` z ) C_ A } ) C_ ~P A <-> U. ( [,] " { z e. ran F | ( [,] ` z ) C_ A } ) C_ A )
29 27 28 sylib 
 |-  ( A e. ( topGen ` ran (,) ) -> U. ( [,] " { z e. ran F | ( [,] ` z ) C_ A } ) C_ A )
30 eqid 
 |-  ( ( abs o. - ) |` ( RR X. RR ) ) = ( ( abs o. - ) |` ( RR X. RR ) )
31 30 rexmet 
 |-  ( ( abs o. - ) |` ( RR X. RR ) ) e. ( *Met ` RR )
32 eqid 
 |-  ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) ) = ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) )
33 30 32 tgioo 
 |-  ( topGen ` ran (,) ) = ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) )
34 33 mopni2 
 |-  ( ( ( ( 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 )
35 31 34 mp3an1 
 |-  ( ( A e. ( topGen ` ran (,) ) /\ w e. A ) -> E. r e. RR+ ( w ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ A )
36 elssuni 
 |-  ( A e. ( topGen ` ran (,) ) -> A C_ U. ( topGen ` ran (,) ) )
37 uniretop 
 |-  RR = U. ( topGen ` ran (,) )
38 36 37 sseqtrrdi 
 |-  ( A e. ( topGen ` ran (,) ) -> A C_ RR )
39 38 sselda 
 |-  ( ( A e. ( topGen ` ran (,) ) /\ w e. A ) -> w e. RR )
40 rpre 
 |-  ( r e. RR+ -> r e. RR )
41 30 bl2ioo 
 |-  ( ( w e. RR /\ r e. RR ) -> ( w ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) = ( ( w - r ) (,) ( w + r ) ) )
42 39 40 41 syl2an 
 |-  ( ( ( A e. ( topGen ` ran (,) ) /\ w e. A ) /\ r e. RR+ ) -> ( w ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) = ( ( w - r ) (,) ( w + r ) ) )
43 42 sseq1d 
 |-  ( ( ( 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 
 |-  2 e. RR
45 1lt2 
 |-  1 < 2
46 expnlbnd 
 |-  ( ( r e. RR+ /\ 2 e. RR /\ 1 < 2 ) -> E. n e. NN ( 1 / ( 2 ^ n ) ) < r )
47 44 45 46 mp3an23 
 |-  ( r e. RR+ -> E. n e. NN ( 1 / ( 2 ^ n ) ) < r )
48 47 ad2antrl 
 |-  ( ( ( A e. ( topGen ` ran (,) ) /\ w e. A ) /\ ( r e. RR+ /\ ( ( w - r ) (,) ( w + r ) ) C_ A ) ) -> E. n e. NN ( 1 / ( 2 ^ n ) ) < r )
49 39 ad2antrr 
 |-  ( ( ( ( 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 
 |-  2 e. NN
51 nnnn0 
 |-  ( n e. NN -> n e. NN0 )
52 51 ad2antrl 
 |-  ( ( ( ( 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 
 |-  ( ( 2 e. NN /\ n e. NN0 ) -> ( 2 ^ n ) e. NN )
54 50 52 53 sylancr 
 |-  ( ( ( ( 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 )
55 54 nnred 
 |-  ( ( ( ( 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 )
56 49 55 remulcld 
 |-  ( ( ( ( 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 
 |-  ( ( w x. ( 2 ^ n ) ) e. RR -> ( ( |_ ` ( w x. ( 2 ^ n ) ) ) <_ ( w x. ( 2 ^ n ) ) /\ ( w x. ( 2 ^ n ) ) < ( ( |_ ` ( w x. ( 2 ^ n ) ) ) + 1 ) ) )
58 56 57 syl 
 |-  ( ( ( ( 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 ) ) )
59 58 simpld 
 |-  ( ( ( ( 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 
 |-  ( ( w x. ( 2 ^ n ) ) e. RR -> ( |_ ` ( w x. ( 2 ^ n ) ) ) e. RR )
61 56 60 syl 
 |-  ( ( ( ( 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 )
62 54 nngt0d 
 |-  ( ( ( ( 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 
 |-  ( ( ( |_ ` ( 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 ) ) ) )
64 61 49 55 62 63 syl112anc 
 |-  ( ( ( ( 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 ) ) ) )
65 59 64 mpbird 
 |-  ( ( ( ( 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 
 |-  ( ( |_ ` ( w x. ( 2 ^ n ) ) ) e. RR -> ( ( |_ ` ( w x. ( 2 ^ n ) ) ) + 1 ) e. RR )
67 61 66 syl 
 |-  ( ( ( ( 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 )
68 67 54 nndivred 
 |-  ( ( ( ( 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 )
69 58 simprd 
 |-  ( ( ( ( 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 
 |-  ( ( 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 ) ) ) )
71 49 67 55 62 70 syl112anc 
 |-  ( ( ( ( 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 ) ) ) )
72 69 71 mpbid 
 |-  ( ( ( ( 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 ) ) )
73 49 68 72 ltled 
 |-  ( ( ( ( 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 ) ) )
74 61 54 nndivred 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( |_ ` ( 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 ) ) ) ) )
76 74 68 75 syl2anc 
 |-  ( ( ( ( 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 ) ) ) ) )
77 49 65 73 76 mpbir3and 
 |-  ( ( ( ( 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 ) ) ) )
78 56 flcld 
 |-  ( ( ( ( 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 )
79 1 dyadval 
 |-  ( ( ( |_ ` ( 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 ) ) >. )
80 78 52 79 syl2anc 
 |-  ( ( ( ( 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 ) ) >. )
81 80 fveq2d 
 |-  ( ( ( ( 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 
 |-  ( ( ( |_ ` ( 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 ) ) >. )
83 81 82 eqtr4di 
 |-  ( ( ( ( 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 ) ) ) )
84 77 83 eleqtrrd 
 |-  ( ( ( ( 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 fveq2 
 |-  ( z = ( ( |_ ` ( w x. ( 2 ^ n ) ) ) F n ) -> ( [,] ` z ) = ( [,] ` ( ( |_ ` ( w x. ( 2 ^ n ) ) ) F n ) ) )
86 85 sseq1d 
 |-  ( z = ( ( |_ ` ( w x. ( 2 ^ n ) ) ) F n ) -> ( ( [,] ` z ) C_ A <-> ( [,] ` ( ( |_ ` ( w x. ( 2 ^ n ) ) ) F n ) ) C_ A ) )
87 ffn 
 |-  ( F : ( ZZ X. NN0 ) --> ( <_ i^i ( RR X. RR ) ) -> F Fn ( ZZ X. NN0 ) )
88 15 87 ax-mp 
 |-  F Fn ( ZZ X. NN0 )
89 fnovrn 
 |-  ( ( F Fn ( ZZ X. NN0 ) /\ ( |_ ` ( w x. ( 2 ^ n ) ) ) e. ZZ /\ n e. NN0 ) -> ( ( |_ ` ( w x. ( 2 ^ n ) ) ) F n ) e. ran F )
90 88 78 52 89 mp3an2i 
 |-  ( ( ( ( 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 )
91 simplrl 
 |-  ( ( ( ( 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+ )
92 91 rpred 
 |-  ( ( ( ( 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 )
93 49 92 resubcld 
 |-  ( ( ( ( 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 )
94 93 rexrd 
 |-  ( ( ( ( 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* )
95 49 92 readdcld 
 |-  ( ( ( ( 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 )
96 95 rexrd 
 |-  ( ( ( ( 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* )
97 74 92 readdcld 
 |-  ( ( ( ( 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 )
98 61 recnd 
 |-  ( ( ( ( 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 )
99 1cnd 
 |-  ( ( ( ( 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 )
100 55 recnd 
 |-  ( ( ( ( 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 )
101 54 nnne0d 
 |-  ( ( ( ( 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 )
102 98 99 100 101 divdird 
 |-  ( ( ( ( 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 ) ) ) )
103 54 nnrecred 
 |-  ( ( ( ( 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 )
104 simprr 
 |-  ( ( ( ( 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 )
105 103 92 74 104 ltadd2dd 
 |-  ( ( ( ( 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 ) )
106 102 105 eqbrtrd 
 |-  ( ( ( ( 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 ) )
107 49 68 97 72 106 lttrd 
 |-  ( ( ( ( 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 ) )
108 49 92 74 ltsubaddd 
 |-  ( ( ( ( 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 ) ) )
109 107 108 mpbird 
 |-  ( ( ( ( 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 ) ) )
110 49 103 readdcld 
 |-  ( ( ( ( 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 )
111 74 49 103 65 leadd1dd 
 |-  ( ( ( ( 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 ) ) ) )
112 102 111 eqbrtrd 
 |-  ( ( ( ( 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 ) ) ) )
113 103 92 49 104 ltadd2dd 
 |-  ( ( ( ( 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 ) )
114 68 110 95 112 113 lelttrd 
 |-  ( ( ( ( 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 ) )
115 iccssioo 
 |-  ( ( ( ( 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 ) ) )
116 94 96 109 114 115 syl22anc 
 |-  ( ( ( ( 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 ) ) )
117 83 116 eqsstrd 
 |-  ( ( ( ( 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 ) ) )
118 simplrr 
 |-  ( ( ( ( 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 )
119 117 118 sstrd 
 |-  ( ( ( ( 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 )
120 86 90 119 elrabd 
 |-  ( ( ( ( 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 } )
121 funfvima2 
 |-  ( ( 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 } ) ) )
122 13 24 121 mp2an 
 |-  ( ( ( |_ ` ( 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 } ) )
123 120 122 syl 
 |-  ( ( ( ( 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 } ) )
124 elunii 
 |-  ( ( 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 } ) )
125 84 123 124 syl2anc 
 |-  ( ( ( ( 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 } ) )
126 48 125 rexlimddv 
 |-  ( ( ( 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 } ) )
127 126 expr 
 |-  ( ( ( 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 } ) ) )
128 43 127 sylbid 
 |-  ( ( ( 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 } ) ) )
129 128 rexlimdva 
 |-  ( ( 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 } ) ) )
130 35 129 mpd 
 |-  ( ( A e. ( topGen ` ran (,) ) /\ w e. A ) -> w e. U. ( [,] " { z e. ran F | ( [,] ` z ) C_ A } ) )
131 29 130 eqelssd 
 |-  ( A e. ( topGen ` ran (,) ) -> U. ( [,] " { z e. ran F | ( [,] ` z ) C_ A } ) = A )
132 fveq2 
 |-  ( c = a -> ( [,] ` c ) = ( [,] ` a ) )
133 132 sseq1d 
 |-  ( c = a -> ( ( [,] ` c ) C_ ( [,] ` b ) <-> ( [,] ` a ) C_ ( [,] ` b ) ) )
134 equequ1 
 |-  ( c = a -> ( c = b <-> a = b ) )
135 133 134 imbi12d 
 |-  ( c = a -> ( ( ( [,] ` c ) C_ ( [,] ` b ) -> c = b ) <-> ( ( [,] ` a ) C_ ( [,] ` b ) -> a = b ) ) )
136 135 ralbidv 
 |-  ( 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 ) ) )
137 136 cbvrabv 
 |-  { 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 ) }
138 14 a1i 
 |-  ( A e. ( topGen ` ran (,) ) -> { z e. ran F | ( [,] ` z ) C_ A } C_ ran F )
139 1 137 138 dyadmbl 
 |-  ( A e. ( topGen ` ran (,) ) -> U. ( [,] " { z e. ran F | ( [,] ` z ) C_ A } ) e. dom vol )
140 131 139 eqeltrrd 
 |-  ( A e. ( topGen ` ran (,) ) -> A e. dom vol )