Metamath Proof Explorer

Theorem opnmbllem0

Description: Lemma for ismblfin ; could also be used to shorten proof of opnmbllem . (Contributed by Brendan Leahy, 13-Jul-2018)

Ref Expression
Assertion opnmbllem0 
|- ( A e. ( topGen ` ran (,) ) -> U. ( [,] " { z e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` z ) C_ A } ) = A )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( z = w -> ( [,] ` z ) = ( [,] ` w ) )
2 1 sseq1d 
 |-  ( z = w -> ( ( [,] ` z ) C_ A <-> ( [,] ` w ) C_ A ) )
3 2 elrab 
 |-  ( w e. { z e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` z ) C_ A } <-> ( w e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) /\ ( [,] ` w ) C_ A ) )
4 simprr 
 |-  ( ( A e. ( topGen ` ran (,) ) /\ ( w e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) /\ ( [,] ` w ) C_ A ) ) -> ( [,] ` w ) C_ A )
5 fvex 
 |-  ( [,] ` w ) e. _V
6 5 elpw 
 |-  ( ( [,] ` w ) e. ~P A <-> ( [,] ` w ) C_ A )
7 4 6 sylibr 
 |-  ( ( A e. ( topGen ` ran (,) ) /\ ( w e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) /\ ( [,] ` w ) C_ A ) ) -> ( [,] ` w ) e. ~P A )
8 3 7 sylan2b 
 |-  ( ( A e. ( topGen ` ran (,) ) /\ w e. { z e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` z ) C_ A } ) -> ( [,] ` w ) e. ~P A )
9 8 ralrimiva 
 |-  ( A e. ( topGen ` ran (,) ) -> A. w e. { z e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` z ) C_ A } ( [,] ` w ) e. ~P A )
10 iccf 
 |-  [,] : ( RR* X. RR* ) --> ~P RR*
11 ffun 
 |-  ( [,] : ( RR* X. RR* ) --> ~P RR* -> Fun [,] )
12 10 11 ax-mp 
 |-  Fun [,]
13 ssrab2 
 |-  { z e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` z ) C_ A } C_ ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. )
14 oveq1 
 |-  ( x = r -> ( x / ( 2 ^ y ) ) = ( r / ( 2 ^ y ) ) )
15 oveq1 
 |-  ( x = r -> ( x + 1 ) = ( r + 1 ) )
16 15 oveq1d 
 |-  ( x = r -> ( ( x + 1 ) / ( 2 ^ y ) ) = ( ( r + 1 ) / ( 2 ^ y ) ) )
17 14 16 opeq12d 
 |-  ( x = r -> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. = <. ( r / ( 2 ^ y ) ) , ( ( r + 1 ) / ( 2 ^ y ) ) >. )
18 oveq2 
 |-  ( y = s -> ( 2 ^ y ) = ( 2 ^ s ) )
19 18 oveq2d 
 |-  ( y = s -> ( r / ( 2 ^ y ) ) = ( r / ( 2 ^ s ) ) )
20 18 oveq2d 
 |-  ( y = s -> ( ( r + 1 ) / ( 2 ^ y ) ) = ( ( r + 1 ) / ( 2 ^ s ) ) )
21 19 20 opeq12d 
 |-  ( y = s -> <. ( r / ( 2 ^ y ) ) , ( ( r + 1 ) / ( 2 ^ y ) ) >. = <. ( r / ( 2 ^ s ) ) , ( ( r + 1 ) / ( 2 ^ s ) ) >. )
22 17 21 cbvmpov 
 |-  ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) = ( r e. ZZ , s e. NN0 |-> <. ( r / ( 2 ^ s ) ) , ( ( r + 1 ) / ( 2 ^ s ) ) >. )
23 22 dyadf 
 |-  ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) : ( ZZ X. NN0 ) --> ( <_ i^i ( RR X. RR ) )
24 frn 
 |-  ( ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) : ( ZZ X. NN0 ) --> ( <_ i^i ( RR X. RR ) ) -> ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) C_ ( <_ i^i ( RR X. RR ) ) )
25 23 24 ax-mp 
 |-  ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) C_ ( <_ i^i ( RR X. RR ) )
26 inss2 
 |-  ( <_ i^i ( RR X. RR ) ) C_ ( RR X. RR )
27 rexpssxrxp 
 |-  ( RR X. RR ) C_ ( RR* X. RR* )
28 26 27 sstri 
 |-  ( <_ i^i ( RR X. RR ) ) C_ ( RR* X. RR* )
29 25 28 sstri 
 |-  ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) C_ ( RR* X. RR* )
30 13 29 sstri 
 |-  { z e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` z ) C_ A } C_ ( RR* X. RR* )
31 10 fdmi 
 |-  dom [,] = ( RR* X. RR* )
32 30 31 sseqtrri 
 |-  { z e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` z ) C_ A } C_ dom [,]
33 funimass4 
 |-  ( ( Fun [,] /\ { z e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` z ) C_ A } C_ dom [,] ) -> ( ( [,] " { z e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` z ) C_ A } ) C_ ~P A <-> A. w e. { z e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` z ) C_ A } ( [,] ` w ) e. ~P A ) )
34 12 32 33 mp2an 
 |-  ( ( [,] " { z e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` z ) C_ A } ) C_ ~P A <-> A. w e. { z e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` z ) C_ A } ( [,] ` w ) e. ~P A )
35 9 34 sylibr 
 |-  ( A e. ( topGen ` ran (,) ) -> ( [,] " { z e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` z ) C_ A } ) C_ ~P A )
36 sspwuni 
 |-  ( ( [,] " { z e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` z ) C_ A } ) C_ ~P A <-> U. ( [,] " { z e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` z ) C_ A } ) C_ A )
37 35 36 sylib 
 |-  ( A e. ( topGen ` ran (,) ) -> U. ( [,] " { z e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` z ) C_ A } ) C_ A )
38 eqid 
 |-  ( ( abs o. - ) |` ( RR X. RR ) ) = ( ( abs o. - ) |` ( RR X. RR ) )
39 38 rexmet 
 |-  ( ( abs o. - ) |` ( RR X. RR ) ) e. ( *Met ` RR )
40 eqid 
 |-  ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) ) = ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) )
41 38 40 tgioo 
 |-  ( topGen ` ran (,) ) = ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) )
42 41 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 )
43 39 42 mp3an1 
 |-  ( ( A e. ( topGen ` ran (,) ) /\ w e. A ) -> E. r e. RR+ ( w ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ A )
44 elssuni 
 |-  ( A e. ( topGen ` ran (,) ) -> A C_ U. ( topGen ` ran (,) ) )
45 uniretop 
 |-  RR = U. ( topGen ` ran (,) )
46 44 45 sseqtrrdi 
 |-  ( A e. ( topGen ` ran (,) ) -> A C_ RR )
47 46 sselda 
 |-  ( ( A e. ( topGen ` ran (,) ) /\ w e. A ) -> w e. RR )
48 rpre 
 |-  ( r e. RR+ -> r e. RR )
49 38 bl2ioo 
 |-  ( ( w e. RR /\ r e. RR ) -> ( w ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) = ( ( w - r ) (,) ( w + r ) ) )
50 47 48 49 syl2an 
 |-  ( ( ( A e. ( topGen ` ran (,) ) /\ w e. A ) /\ r e. RR+ ) -> ( w ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) = ( ( w - r ) (,) ( w + r ) ) )
51 50 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 ) )
52 2re 
 |-  2 e. RR
53 1lt2 
 |-  1 < 2
54 expnlbnd 
 |-  ( ( r e. RR+ /\ 2 e. RR /\ 1 < 2 ) -> E. n e. NN ( 1 / ( 2 ^ n ) ) < r )
55 52 53 54 mp3an23 
 |-  ( r e. RR+ -> E. n e. NN ( 1 / ( 2 ^ n ) ) < r )
56 55 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 )
57 47 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 )
58 2nn 
 |-  2 e. NN
59 nnnn0 
 |-  ( n e. NN -> n e. NN0 )
60 59 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 )
61 nnexpcl 
 |-  ( ( 2 e. NN /\ n e. NN0 ) -> ( 2 ^ n ) e. NN )
62 58 60 61 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 )
63 62 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 )
64 57 63 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 )
65 fllelt 
 |-  ( ( w x. ( 2 ^ n ) ) e. RR -> ( ( |_ ` ( w x. ( 2 ^ n ) ) ) <_ ( w x. ( 2 ^ n ) ) /\ ( w x. ( 2 ^ n ) ) < ( ( |_ ` ( w x. ( 2 ^ n ) ) ) + 1 ) ) )
66 64 65 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 ) ) )
67 66 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 ) ) )
68 reflcl 
 |-  ( ( w x. ( 2 ^ n ) ) e. RR -> ( |_ ` ( w x. ( 2 ^ n ) ) ) e. RR )
69 64 68 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 )
70 62 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 ) )
71 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 ) ) ) )
72 69 57 63 70 71 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 ) ) ) )
73 67 72 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 )
74 peano2re 
 |-  ( ( |_ ` ( w x. ( 2 ^ n ) ) ) e. RR -> ( ( |_ ` ( w x. ( 2 ^ n ) ) ) + 1 ) e. RR )
75 69 74 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 )
76 75 62 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 )
77 66 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 ) )
78 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 ) ) ) )
79 57 75 63 70 78 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 ) ) ) )
80 77 79 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 ) ) )
81 57 76 80 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 ) ) )
82 69 62 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 )
83 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 ) ) ) ) )
84 82 76 83 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 ) ) ) ) )
85 57 73 81 84 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 ) ) ) )
86 64 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 )
87 22 dyadval 
 |-  ( ( ( |_ ` ( w x. ( 2 ^ n ) ) ) e. ZZ /\ n e. NN0 ) -> ( ( |_ ` ( w x. ( 2 ^ n ) ) ) ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) n ) = <. ( ( |_ ` ( w x. ( 2 ^ n ) ) ) / ( 2 ^ n ) ) , ( ( ( |_ ` ( w x. ( 2 ^ n ) ) ) + 1 ) / ( 2 ^ n ) ) >. )
88 86 60 87 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 ) ) ) ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) n ) = <. ( ( |_ ` ( w x. ( 2 ^ n ) ) ) / ( 2 ^ n ) ) , ( ( ( |_ ` ( w x. ( 2 ^ n ) ) ) + 1 ) / ( 2 ^ n ) ) >. )
89 88 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 ) ) ) ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) n ) ) = ( [,] ` <. ( ( |_ ` ( w x. ( 2 ^ n ) ) ) / ( 2 ^ n ) ) , ( ( ( |_ ` ( w x. ( 2 ^ n ) ) ) + 1 ) / ( 2 ^ n ) ) >. ) )
90 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 ) ) >. )
91 89 90 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 ) ) ) ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) n ) ) = ( ( ( |_ ` ( w x. ( 2 ^ n ) ) ) / ( 2 ^ n ) ) [,] ( ( ( |_ ` ( w x. ( 2 ^ n ) ) ) + 1 ) / ( 2 ^ n ) ) ) )
92 85 91 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 ) ) ) ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) n ) ) )
93 ffn 
 |-  ( ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) : ( ZZ X. NN0 ) --> ( <_ i^i ( RR X. RR ) ) -> ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) Fn ( ZZ X. NN0 ) )
94 23 93 ax-mp 
 |-  ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) Fn ( ZZ X. NN0 )
95 fnovrn 
 |-  ( ( ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) Fn ( ZZ X. NN0 ) /\ ( |_ ` ( w x. ( 2 ^ n ) ) ) e. ZZ /\ n e. NN0 ) -> ( ( |_ ` ( w x. ( 2 ^ n ) ) ) ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) n ) e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) )
96 94 95 mp3an1 
 |-  ( ( ( |_ ` ( w x. ( 2 ^ n ) ) ) e. ZZ /\ n e. NN0 ) -> ( ( |_ ` ( w x. ( 2 ^ n ) ) ) ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) n ) e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) )
97 86 60 96 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 ) ) ) ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) n ) e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) )
98 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+ )
99 98 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 )
100 57 99 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 )
101 100 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* )
102 57 99 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 )
103 102 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* )
104 82 99 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 )
105 69 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 )
106 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 )
107 63 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 )
108 62 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 )
109 105 106 107 108 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 ) ) ) )
110 62 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 )
111 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 )
112 110 99 82 111 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 ) )
113 109 112 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 ) )
114 57 76 104 80 113 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 ) )
115 57 99 82 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 ) ) )
116 114 115 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 ) ) )
117 57 110 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 )
118 82 57 110 73 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 ) ) ) )
119 109 118 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 ) ) ) )
120 110 99 57 111 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 ) )
121 76 117 102 119 120 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 ) )
122 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 ) ) )
123 101 103 116 121 122 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 ) ) )
124 91 123 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 ) ) ) ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) n ) ) C_ ( ( w - r ) (,) ( w + r ) ) )
125 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 )
126 124 125 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 ) ) ) ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) n ) ) C_ A )
127 fveq2 
 |-  ( z = ( ( |_ ` ( w x. ( 2 ^ n ) ) ) ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) n ) -> ( [,] ` z ) = ( [,] ` ( ( |_ ` ( w x. ( 2 ^ n ) ) ) ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) n ) ) )
128 127 sseq1d 
 |-  ( z = ( ( |_ ` ( w x. ( 2 ^ n ) ) ) ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) n ) -> ( ( [,] ` z ) C_ A <-> ( [,] ` ( ( |_ ` ( w x. ( 2 ^ n ) ) ) ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) n ) ) C_ A ) )
129 128 elrab 
 |-  ( ( ( |_ ` ( w x. ( 2 ^ n ) ) ) ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) n ) e. { z e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` z ) C_ A } <-> ( ( ( |_ ` ( w x. ( 2 ^ n ) ) ) ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) n ) e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) /\ ( [,] ` ( ( |_ ` ( w x. ( 2 ^ n ) ) ) ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) n ) ) C_ A ) )
130 97 126 129 sylanbrc 
 |-  ( ( ( ( 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 ) ) ) ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) n ) e. { z e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` z ) C_ A } )
131 funfvima2 
 |-  ( ( Fun [,] /\ { z e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` z ) C_ A } C_ dom [,] ) -> ( ( ( |_ ` ( w x. ( 2 ^ n ) ) ) ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) n ) e. { z e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` z ) C_ A } -> ( [,] ` ( ( |_ ` ( w x. ( 2 ^ n ) ) ) ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) n ) ) e. ( [,] " { z e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` z ) C_ A } ) ) )
132 12 32 131 mp2an 
 |-  ( ( ( |_ ` ( w x. ( 2 ^ n ) ) ) ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) n ) e. { z e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` z ) C_ A } -> ( [,] ` ( ( |_ ` ( w x. ( 2 ^ n ) ) ) ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) n ) ) e. ( [,] " { z e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` z ) C_ A } ) )
133 130 132 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 ) ) ) ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) n ) ) e. ( [,] " { z e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` z ) C_ A } ) )
134 elunii 
 |-  ( ( w e. ( [,] ` ( ( |_ ` ( w x. ( 2 ^ n ) ) ) ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) n ) ) /\ ( [,] ` ( ( |_ ` ( w x. ( 2 ^ n ) ) ) ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) n ) ) e. ( [,] " { z e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` z ) C_ A } ) ) -> w e. U. ( [,] " { z e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` z ) C_ A } ) )
135 92 133 134 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 ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` z ) C_ A } ) )
136 56 135 rexlimddv 
 |-  ( ( ( A e. ( topGen ` ran (,) ) /\ w e. A ) /\ ( r e. RR+ /\ ( ( w - r ) (,) ( w + r ) ) C_ A ) ) -> w e. U. ( [,] " { z e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` z ) C_ A } ) )
137 136 expr 
 |-  ( ( ( A e. ( topGen ` ran (,) ) /\ w e. A ) /\ r e. RR+ ) -> ( ( ( w - r ) (,) ( w + r ) ) C_ A -> w e. U. ( [,] " { z e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` z ) C_ A } ) ) )
138 51 137 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 ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` z ) C_ A } ) ) )
139 138 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 ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` z ) C_ A } ) ) )
140 43 139 mpd 
 |-  ( ( A e. ( topGen ` ran (,) ) /\ w e. A ) -> w e. U. ( [,] " { z e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` z ) C_ A } ) )
141 37 140 eqelssd 
 |-  ( A e. ( topGen ` ran (,) ) -> U. ( [,] " { z e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` z ) C_ A } ) = A )