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

Theorem mblfinlem2 26284
Description: Lemma for ismblfin 26287, effectively one direction of the same fact for open sets, made necessary by Viaclovsky's slightly different defintion of outer measure. Note that unlike the main theorem, this holds for sets of infinite measure. (Contributed by Brendan Leahy, 21-Feb-2018.) (Revised by Brendan Leahy, 13-Jul-2018.)
Assertion
Ref Expression
mblfinlem2  |-  ( ( A  e.  ( topGen ` 
ran  (,) )  /\  M  e.  RR  /\  M  < 
( vol * `  A ) )  ->  E. s  e.  ( Clsd `  ( topGen `  ran  (,) ) ) ( s 
C_  A  /\  M  <  ( vol * `  s ) ) )
Distinct variable groups:    A, s    M, s

Proof of Theorem mblfinlem2
Dummy variables  a 
b  c  f  m  n  p  t  u  v  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 retop 18833 . . . 4  |-  ( topGen ` 
ran  (,) )  e.  Top
2 0cld 17140 . . . 4  |-  ( (
topGen `  ran  (,) )  e.  Top  ->  (/)  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) )
31, 2ax-mp 5 . . 3  |-  (/)  e.  (
Clsd `  ( topGen ` 
ran  (,) ) )
4 simpl3 963 . . . . 5  |-  ( ( ( A  e.  (
topGen `  ran  (,) )  /\  M  e.  RR  /\  M  <  ( vol
* `  A )
)  /\  A  =  (/) )  ->  M  <  ( vol * `  A
) )
5 fveq2 5763 . . . . . 6  |-  ( A  =  (/)  ->  ( vol
* `  A )  =  ( vol * `  (/) ) )
65adantl 454 . . . . 5  |-  ( ( ( A  e.  (
topGen `  ran  (,) )  /\  M  e.  RR  /\  M  <  ( vol
* `  A )
)  /\  A  =  (/) )  ->  ( vol * `
 A )  =  ( vol * `  (/) ) )
74, 6breqtrd 4267 . . . 4  |-  ( ( ( A  e.  (
topGen `  ran  (,) )  /\  M  e.  RR  /\  M  <  ( vol
* `  A )
)  /\  A  =  (/) )  ->  M  <  ( vol * `  (/) ) )
8 0ss 3644 . . . 4  |-  (/)  C_  A
97, 8jctil 525 . . 3  |-  ( ( ( A  e.  (
topGen `  ran  (,) )  /\  M  e.  RR  /\  M  <  ( vol
* `  A )
)  /\  A  =  (/) )  ->  ( (/)  C_  A  /\  M  <  ( vol
* `  (/) ) ) )
10 sseq1 3358 . . . . 5  |-  ( s  =  (/)  ->  ( s 
C_  A  <->  (/)  C_  A
) )
11 fveq2 5763 . . . . . 6  |-  ( s  =  (/)  ->  ( vol
* `  s )  =  ( vol * `  (/) ) )
1211breq2d 4255 . . . . 5  |-  ( s  =  (/)  ->  ( M  <  ( vol * `  s )  <->  M  <  ( vol * `  (/) ) ) )
1310, 12anbi12d 693 . . . 4  |-  ( s  =  (/)  ->  ( ( s  C_  A  /\  M  <  ( vol * `  s ) )  <->  ( (/)  C_  A  /\  M  <  ( vol
* `  (/) ) ) ) )
1413rspcev 3061 . . 3  |-  ( (
(/)  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( (/)  C_  A  /\  M  <  ( vol
* `  (/) ) ) )  ->  E. s  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( s  C_  A  /\  M  <  ( vol * `  s ) ) )
153, 9, 14sylancr 646 . 2  |-  ( ( ( A  e.  (
topGen `  ran  (,) )  /\  M  e.  RR  /\  M  <  ( vol
* `  A )
)  /\  A  =  (/) )  ->  E. s  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( s  C_  A  /\  M  <  ( vol * `  s ) ) )
16 mblfinlem1 26283 . . . 4  |-  ( ( A  e.  ( topGen ` 
ran  (,) )  /\  A  =/=  (/) )  ->  E. f 
f : NN -1-1-onto-> { a  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A }  |  A. c  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A } 
( ( [,] `  a
)  C_  ( [,] `  c )  ->  a  =  c ) } )
17163ad2antl1 1120 . . 3  |-  ( ( ( A  e.  (
topGen `  ran  (,) )  /\  M  e.  RR  /\  M  <  ( vol
* `  A )
)  /\  A  =/=  (/) )  ->  E. f 
f : NN -1-1-onto-> { a  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A }  |  A. c  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A } 
( ( [,] `  a
)  C_  ( [,] `  c )  ->  a  =  c ) } )
18 simpl3 963 . . . . . . . . 9  |-  ( ( ( A  e.  (
topGen `  ran  (,) )  /\  M  e.  RR  /\  M  <  ( vol
* `  A )
)  /\  f : NN
-1-1-onto-> { a  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A }  |  A. c  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A } 
( ( [,] `  a
)  C_  ( [,] `  c )  ->  a  =  c ) } )  ->  M  <  ( vol * `  A
) )
19 f1ofo 5716 . . . . . . . . . . . . . 14  |-  ( f : NN -1-1-onto-> { a  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A }  |  A. c  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A } 
( ( [,] `  a
)  C_  ( [,] `  c )  ->  a  =  c ) }  ->  f : NN -onto-> { a  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A }  |  A. c  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A } 
( ( [,] `  a
)  C_  ( [,] `  c )  ->  a  =  c ) } )
20 rnco2 5412 . . . . . . . . . . . . . . . 16  |-  ran  ( [,]  o.  f )  =  ( [,] " ran  f )
21 forn 5691 . . . . . . . . . . . . . . . . 17  |-  ( f : NN -onto-> { a  e.  { b  e. 
ran  ( x  e.  ZZ ,  y  e. 
NN0  |->  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>. )  |  ( [,] `  b )  C_  A }  |  A. c  e.  { b  e.  ran  ( x  e.  ZZ ,  y  e. 
NN0  |->  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>. )  |  ( [,] `  b )  C_  A }  ( ( [,] `  a )  C_  ( [,] `  c )  ->  a  =  c ) }  ->  ran  f  =  { a  e.  { b  e.  ran  ( x  e.  ZZ ,  y  e.  NN0  |->  <. ( x  /  (
2 ^ y ) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) ) >.
)  |  ( [,] `  b )  C_  A }  |  A. c  e.  { b  e.  ran  ( x  e.  ZZ ,  y  e.  NN0  |->  <. ( x  /  (
2 ^ y ) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) ) >.
)  |  ( [,] `  b )  C_  A }  ( ( [,] `  a )  C_  ( [,] `  c )  -> 
a  =  c ) } )
2221imaeq2d 5238 . . . . . . . . . . . . . . . 16  |-  ( f : NN -onto-> { a  e.  { b  e. 
ran  ( x  e.  ZZ ,  y  e. 
NN0  |->  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>. )  |  ( [,] `  b )  C_  A }  |  A. c  e.  { b  e.  ran  ( x  e.  ZZ ,  y  e. 
NN0  |->  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>. )  |  ( [,] `  b )  C_  A }  ( ( [,] `  a )  C_  ( [,] `  c )  ->  a  =  c ) }  ->  ( [,] " ran  f )  =  ( [,] " {
a  e.  { b  e.  ran  ( x  e.  ZZ ,  y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A }  |  A. c  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A } 
( ( [,] `  a
)  C_  ( [,] `  c )  ->  a  =  c ) } ) )
2320, 22syl5eq 2487 . . . . . . . . . . . . . . 15  |-  ( f : NN -onto-> { a  e.  { b  e. 
ran  ( x  e.  ZZ ,  y  e. 
NN0  |->  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>. )  |  ( [,] `  b )  C_  A }  |  A. c  e.  { b  e.  ran  ( x  e.  ZZ ,  y  e. 
NN0  |->  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>. )  |  ( [,] `  b )  C_  A }  ( ( [,] `  a )  C_  ( [,] `  c )  ->  a  =  c ) }  ->  ran  ( [,]  o.  f )  =  ( [,] " {
a  e.  { b  e.  ran  ( x  e.  ZZ ,  y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A }  |  A. c  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A } 
( ( [,] `  a
)  C_  ( [,] `  c )  ->  a  =  c ) } ) )
2423unieqd 4055 . . . . . . . . . . . . . 14  |-  ( f : NN -onto-> { a  e.  { b  e. 
ran  ( x  e.  ZZ ,  y  e. 
NN0  |->  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>. )  |  ( [,] `  b )  C_  A }  |  A. c  e.  { b  e.  ran  ( x  e.  ZZ ,  y  e. 
NN0  |->  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>. )  |  ( [,] `  b )  C_  A }  ( ( [,] `  a )  C_  ( [,] `  c )  ->  a  =  c ) }  ->  U. ran  ( [,]  o.  f )  =  U. ( [,] " { a  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A }  |  A. c  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A } 
( ( [,] `  a
)  C_  ( [,] `  c )  ->  a  =  c ) } ) )
2519, 24syl 16 . . . . . . . . . . . . 13  |-  ( f : NN -1-1-onto-> { a  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A }  |  A. c  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A } 
( ( [,] `  a
)  C_  ( [,] `  c )  ->  a  =  c ) }  ->  U. ran  ( [,] 
o.  f )  = 
U. ( [,] " {
a  e.  { b  e.  ran  ( x  e.  ZZ ,  y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A }  |  A. c  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A } 
( ( [,] `  a
)  C_  ( [,] `  c )  ->  a  =  c ) } ) )
2625adantl 454 . . . . . . . . . . . 12  |-  ( ( ( A  e.  (
topGen `  ran  (,) )  /\  M  e.  RR  /\  M  <  ( vol
* `  A )
)  /\  f : NN
-1-1-onto-> { a  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A }  |  A. c  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A } 
( ( [,] `  a
)  C_  ( [,] `  c )  ->  a  =  c ) } )  ->  U. ran  ( [,]  o.  f )  = 
U. ( [,] " {
a  e.  { b  e.  ran  ( x  e.  ZZ ,  y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A }  |  A. c  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A } 
( ( [,] `  a
)  C_  ( [,] `  c )  ->  a  =  c ) } ) )
27 oveq1 6124 . . . . . . . . . . . . . . . 16  |-  ( x  =  u  ->  (
x  /  ( 2 ^ y ) )  =  ( u  / 
( 2 ^ y
) ) )
28 oveq1 6124 . . . . . . . . . . . . . . . . 17  |-  ( x  =  u  ->  (
x  +  1 )  =  ( u  + 
1 ) )
2928oveq1d 6132 . . . . . . . . . . . . . . . 16  |-  ( x  =  u  ->  (
( x  +  1 )  /  ( 2 ^ y ) )  =  ( ( u  +  1 )  / 
( 2 ^ y
) ) )
3027, 29opeq12d 4021 . . . . . . . . . . . . . . 15  |-  ( x  =  u  ->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >.  =  <. ( u  /  ( 2 ^ y ) ) ,  ( ( u  +  1 )  / 
( 2 ^ y
) ) >. )
31 oveq2 6125 . . . . . . . . . . . . . . . . 17  |-  ( y  =  v  ->  (
2 ^ y )  =  ( 2 ^ v ) )
3231oveq2d 6133 . . . . . . . . . . . . . . . 16  |-  ( y  =  v  ->  (
u  /  ( 2 ^ y ) )  =  ( u  / 
( 2 ^ v
) ) )
3331oveq2d 6133 . . . . . . . . . . . . . . . 16  |-  ( y  =  v  ->  (
( u  +  1 )  /  ( 2 ^ y ) )  =  ( ( u  +  1 )  / 
( 2 ^ v
) ) )
3432, 33opeq12d 4021 . . . . . . . . . . . . . . 15  |-  ( y  =  v  ->  <. (
u  /  ( 2 ^ y ) ) ,  ( ( u  +  1 )  / 
( 2 ^ y
) ) >.  =  <. ( u  /  ( 2 ^ v ) ) ,  ( ( u  +  1 )  / 
( 2 ^ v
) ) >. )
3530, 34cbvmpt2v 6188 . . . . . . . . . . . . . 14  |-  ( x  e.  ZZ ,  y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  =  ( u  e.  ZZ ,  v  e. 
NN0  |->  <. ( u  / 
( 2 ^ v
) ) ,  ( ( u  +  1 )  /  ( 2 ^ v ) )
>. )
36 fveq2 5763 . . . . . . . . . . . . . . . . . 18  |-  ( a  =  z  ->  ( [,] `  a )  =  ( [,] `  z
) )
3736sseq1d 3364 . . . . . . . . . . . . . . . . 17  |-  ( a  =  z  ->  (
( [,] `  a
)  C_  ( [,] `  c )  <->  ( [,] `  z )  C_  ( [,] `  c ) ) )
38 eqeq1 2449 . . . . . . . . . . . . . . . . 17  |-  ( a  =  z  ->  (
a  =  c  <->  z  =  c ) )
3937, 38imbi12d 313 . . . . . . . . . . . . . . . 16  |-  ( a  =  z  ->  (
( ( [,] `  a
)  C_  ( [,] `  c )  ->  a  =  c )  <->  ( ( [,] `  z )  C_  ( [,] `  c )  ->  z  =  c ) ) )
4039ralbidv 2732 . . . . . . . . . . . . . . 15  |-  ( a  =  z  ->  ( A. c  e.  { b  e.  ran  ( x  e.  ZZ ,  y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A } 
( ( [,] `  a
)  C_  ( [,] `  c )  ->  a  =  c )  <->  A. c  e.  { b  e.  ran  ( x  e.  ZZ ,  y  e.  NN0  |->  <. ( x  /  (
2 ^ y ) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) ) >.
)  |  ( [,] `  b )  C_  A }  ( ( [,] `  z )  C_  ( [,] `  c )  -> 
z  =  c ) ) )
4140cbvrabv 2964 . . . . . . . . . . . . . 14  |-  { a  e.  { b  e. 
ran  ( x  e.  ZZ ,  y  e. 
NN0  |->  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>. )  |  ( [,] `  b )  C_  A }  |  A. c  e.  { b  e.  ran  ( x  e.  ZZ ,  y  e. 
NN0  |->  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>. )  |  ( [,] `  b )  C_  A }  ( ( [,] `  a )  C_  ( [,] `  c )  ->  a  =  c ) }  =  {
z  e.  { b  e.  ran  ( x  e.  ZZ ,  y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A }  |  A. c  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A } 
( ( [,] `  z
)  C_  ( [,] `  c )  ->  z  =  c ) }
42 ssrab2 3417 . . . . . . . . . . . . . . 15  |-  { b  e.  ran  ( x  e.  ZZ ,  y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A }  C_ 
ran  ( x  e.  ZZ ,  y  e. 
NN0  |->  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>. )
4342a1i 11 . . . . . . . . . . . . . 14  |-  ( ( A  e.  ( topGen ` 
ran  (,) )  /\  M  e.  RR  /\  M  < 
( vol * `  A ) )  ->  { b  e.  ran  ( x  e.  ZZ ,  y  e.  NN0  |->  <. ( x  /  (
2 ^ y ) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) ) >.
)  |  ( [,] `  b )  C_  A }  C_  ran  ( x  e.  ZZ ,  y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )
)
4435, 41, 43dyadmbllem 19529 . . . . . . . . . . . . 13  |-  ( ( A  e.  ( topGen ` 
ran  (,) )  /\  M  e.  RR  /\  M  < 
( vol * `  A ) )  ->  U. ( [,] " {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A }
)  =  U. ( [,] " { a  e. 
{ b  e.  ran  ( x  e.  ZZ ,  y  e.  NN0  |->  <. ( x  /  (
2 ^ y ) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) ) >.
)  |  ( [,] `  b )  C_  A }  |  A. c  e.  { b  e.  ran  ( x  e.  ZZ ,  y  e.  NN0  |->  <. ( x  /  (
2 ^ y ) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) ) >.
)  |  ( [,] `  b )  C_  A }  ( ( [,] `  a )  C_  ( [,] `  c )  -> 
a  =  c ) } ) )
4544adantr 453 . . . . . . . . . . . 12  |-  ( ( ( A  e.  (
topGen `  ran  (,) )  /\  M  e.  RR  /\  M  <  ( vol
* `  A )
)  /\  f : NN
-1-1-onto-> { a  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A }  |  A. c  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A } 
( ( [,] `  a
)  C_  ( [,] `  c )  ->  a  =  c ) } )  ->  U. ( [,] " { b  e. 
ran  ( x  e.  ZZ ,  y  e. 
NN0  |->  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>. )  |  ( [,] `  b )  C_  A } )  =  U. ( [,] " { a  e.  { b  e. 
ran  ( x  e.  ZZ ,  y  e. 
NN0  |->  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>. )  |  ( [,] `  b )  C_  A }  |  A. c  e.  { b  e.  ran  ( x  e.  ZZ ,  y  e. 
NN0  |->  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>. )  |  ( [,] `  b )  C_  A }  ( ( [,] `  a )  C_  ( [,] `  c )  ->  a  =  c ) } ) )
46 opnmbllem0 26282 . . . . . . . . . . . . . 14  |-  ( A  e.  ( topGen `  ran  (,) )  ->  U. ( [,] " { b  e. 
ran  ( x  e.  ZZ ,  y  e. 
NN0  |->  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>. )  |  ( [,] `  b )  C_  A } )  =  A )
47463ad2ant1 979 . . . . . . . . . . . . 13  |-  ( ( A  e.  ( topGen ` 
ran  (,) )  /\  M  e.  RR  /\  M  < 
( vol * `  A ) )  ->  U. ( [,] " {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A }
)  =  A )
4847adantr 453 . . . . . . . . . . . 12  |-  ( ( ( A  e.  (
topGen `  ran  (,) )  /\  M  e.  RR  /\  M  <  ( vol
* `  A )
)  /\  f : NN
-1-1-onto-> { a  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A }  |  A. c  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A } 
( ( [,] `  a
)  C_  ( [,] `  c )  ->  a  =  c ) } )  ->  U. ( [,] " { b  e. 
ran  ( x  e.  ZZ ,  y  e. 
NN0  |->  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>. )  |  ( [,] `  b )  C_  A } )  =  A )
4926, 45, 483eqtr2d 2481 . . . . . . . . . . 11  |-  ( ( ( A  e.  (
topGen `  ran  (,) )  /\  M  e.  RR  /\  M  <  ( vol
* `  A )
)  /\  f : NN
-1-1-onto-> { a  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A }  |  A. c  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A } 
( ( [,] `  a
)  C_  ( [,] `  c )  ->  a  =  c ) } )  ->  U. ran  ( [,]  o.  f )  =  A )
5049fveq2d 5767 . . . . . . . . . 10  |-  ( ( ( A  e.  (
topGen `  ran  (,) )  /\  M  e.  RR  /\  M  <  ( vol
* `  A )
)  /\  f : NN
-1-1-onto-> { a  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A }  |  A. c  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A } 
( ( [,] `  a
)  C_  ( [,] `  c )  ->  a  =  c ) } )  ->  ( vol * `
 U. ran  ( [,]  o.  f ) )  =  ( vol * `  A ) )
51 f1of 5709 . . . . . . . . . . . . 13  |-  ( f : NN -1-1-onto-> { a  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A }  |  A. c  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A } 
( ( [,] `  a
)  C_  ( [,] `  c )  ->  a  =  c ) }  ->  f : NN --> { a  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A }  |  A. c  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A } 
( ( [,] `  a
)  C_  ( [,] `  c )  ->  a  =  c ) } )
52 ssrab2 3417 . . . . . . . . . . . . . 14  |-  { a  e.  { b  e. 
ran  ( x  e.  ZZ ,  y  e. 
NN0  |->  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>. )  |  ( [,] `  b )  C_  A }  |  A. c  e.  { b  e.  ran  ( x  e.  ZZ ,  y  e. 
NN0  |->  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>. )  |  ( [,] `  b )  C_  A }  ( ( [,] `  a )  C_  ( [,] `  c )  ->  a  =  c ) }  C_  { b  e.  ran  ( x  e.  ZZ ,  y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A }
5335dyadf 19521 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ZZ ,  y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. ) : ( ZZ  X.  NN0 ) --> (  <_  i^i  ( RR  X.  RR ) )
54 frn 5632 . . . . . . . . . . . . . . . 16  |-  ( ( 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 ) ) )
5553, 54ax-mp 5 . . . . . . . . . . . . . . 15  |-  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  C_  (  <_  i^i  ( RR  X.  RR ) )
5642, 55sstri 3346 . . . . . . . . . . . . . 14  |-  { b  e.  ran  ( x  e.  ZZ ,  y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A }  C_  (  <_  i^i  ( RR  X.  RR ) )
5752, 56sstri 3346 . . . . . . . . . . . . 13  |-  { a  e.  { b  e. 
ran  ( x  e.  ZZ ,  y  e. 
NN0  |->  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>. )  |  ( [,] `  b )  C_  A }  |  A. c  e.  { b  e.  ran  ( x  e.  ZZ ,  y  e. 
NN0  |->  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>. )  |  ( [,] `  b )  C_  A }  ( ( [,] `  a )  C_  ( [,] `  c )  ->  a  =  c ) }  C_  (  <_  i^i  ( RR  X.  RR ) )
58 fss 5634 . . . . . . . . . . . . 13  |-  ( ( f : NN --> { a  e.  { b  e. 
ran  ( x  e.  ZZ ,  y  e. 
NN0  |->  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>. )  |  ( [,] `  b )  C_  A }  |  A. c  e.  { b  e.  ran  ( x  e.  ZZ ,  y  e. 
NN0  |->  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>. )  |  ( [,] `  b )  C_  A }  ( ( [,] `  a )  C_  ( [,] `  c )  ->  a  =  c ) }  /\  {
a  e.  { b  e.  ran  ( x  e.  ZZ ,  y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A }  |  A. c  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A } 
( ( [,] `  a
)  C_  ( [,] `  c )  ->  a  =  c ) } 
C_  (  <_  i^i  ( RR  X.  RR ) ) )  -> 
f : NN --> (  <_  i^i  ( RR  X.  RR ) ) )
5951, 57, 58sylancl 645 . . . . . . . . . . . 12  |-  ( f : NN -1-1-onto-> { a  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A }  |  A. c  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A } 
( ( [,] `  a
)  C_  ( [,] `  c )  ->  a  =  c ) }  ->  f : NN --> (  <_  i^i  ( RR  X.  RR ) ) )
6052, 42sstri 3346 . . . . . . . . . . . . . . . . . . . 20  |-  { a  e.  { b  e. 
ran  ( x  e.  ZZ ,  y  e. 
NN0  |->  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>. )  |  ( [,] `  b )  C_  A }  |  A. c  e.  { b  e.  ran  ( x  e.  ZZ ,  y  e. 
NN0  |->  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>. )  |  ( [,] `  b )  C_  A }  ( ( [,] `  a )  C_  ( [,] `  c )  ->  a  =  c ) }  C_  ran  ( x  e.  ZZ ,  y  e.  NN0  |->  <. ( x  /  (
2 ^ y ) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) ) >.
)
61 ffvelrn 5904 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( f : NN --> { a  e.  { b  e. 
ran  ( x  e.  ZZ ,  y  e. 
NN0  |->  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>. )  |  ( [,] `  b )  C_  A }  |  A. c  e.  { b  e.  ran  ( x  e.  ZZ ,  y  e. 
NN0  |->  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>. )  |  ( [,] `  b )  C_  A }  ( ( [,] `  a )  C_  ( [,] `  c )  ->  a  =  c ) }  /\  m  e.  NN )  ->  (
f `  m )  e.  { a  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A }  |  A. c  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A } 
( ( [,] `  a
)  C_  ( [,] `  c )  ->  a  =  c ) } )
6260, 61sseldi 3335 . . . . . . . . . . . . . . . . . . 19  |-  ( ( f : NN --> { a  e.  { b  e. 
ran  ( x  e.  ZZ ,  y  e. 
NN0  |->  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>. )  |  ( [,] `  b )  C_  A }  |  A. c  e.  { b  e.  ran  ( x  e.  ZZ ,  y  e. 
NN0  |->  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>. )  |  ( [,] `  b )  C_  A }  ( ( [,] `  a )  C_  ( [,] `  c )  ->  a  =  c ) }  /\  m  e.  NN )  ->  (
f `  m )  e.  ran  ( x  e.  ZZ ,  y  e. 
NN0  |->  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>. ) )
6362adantrr 699 . . . . . . . . . . . . . . . . . 18  |-  ( ( f : NN --> { a  e.  { b  e. 
ran  ( x  e.  ZZ ,  y  e. 
NN0  |->  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>. )  |  ( [,] `  b )  C_  A }  |  A. c  e.  { b  e.  ran  ( x  e.  ZZ ,  y  e. 
NN0  |->  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>. )  |  ( [,] `  b )  C_  A }  ( ( [,] `  a )  C_  ( [,] `  c )  ->  a  =  c ) }  /\  (
m  e.  NN  /\  z  e.  NN )
)  ->  ( f `  m )  e.  ran  ( x  e.  ZZ ,  y  e.  NN0  |->  <. ( x  /  (
2 ^ y ) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) ) >.
) )
64 ffvelrn 5904 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( f : NN --> { a  e.  { b  e. 
ran  ( x  e.  ZZ ,  y  e. 
NN0  |->  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>. )  |  ( [,] `  b )  C_  A }  |  A. c  e.  { b  e.  ran  ( x  e.  ZZ ,  y  e. 
NN0  |->  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>. )  |  ( [,] `  b )  C_  A }  ( ( [,] `  a )  C_  ( [,] `  c )  ->  a  =  c ) }  /\  z  e.  NN )  ->  (
f `  z )  e.  { a  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A }  |  A. c  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A } 
( ( [,] `  a
)  C_  ( [,] `  c )  ->  a  =  c ) } )
6560, 64sseldi 3335 . . . . . . . . . . . . . . . . . . 19  |-  ( ( f : NN --> { a  e.  { b  e. 
ran  ( x  e.  ZZ ,  y  e. 
NN0  |->  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>. )  |  ( [,] `  b )  C_  A }  |  A. c  e.  { b  e.  ran  ( x  e.  ZZ ,  y  e. 
NN0  |->  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>. )  |  ( [,] `  b )  C_  A }  ( ( [,] `  a )  C_  ( [,] `  c )  ->  a  =  c ) }  /\  z  e.  NN )  ->  (
f `  z )  e.  ran  ( x  e.  ZZ ,  y  e. 
NN0  |->  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>. ) )
6665adantrl 698 . . . . . . . . . . . . . . . . . 18  |-  ( ( f : NN --> { a  e.  { b  e. 
ran  ( x  e.  ZZ ,  y  e. 
NN0  |->  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>. )  |  ( [,] `  b )  C_  A }  |  A. c  e.  { b  e.  ran  ( x  e.  ZZ ,  y  e. 
NN0  |->  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>. )  |  ( [,] `  b )  C_  A }  ( ( [,] `  a )  C_  ( [,] `  c )  ->  a  =  c ) }  /\  (
m  e.  NN  /\  z  e.  NN )
)  ->  ( f `  z )  e.  ran  ( x  e.  ZZ ,  y  e.  NN0  |->  <. ( x  /  (
2 ^ y ) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) ) >.
) )
6735dyaddisj 19526 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( f `  m
)  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  /\  ( f `  z
)  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )
)  ->  ( ( [,] `  ( f `  m ) )  C_  ( [,] `  ( f `
 z ) )  \/  ( [,] `  (
f `  z )
)  C_  ( [,] `  ( f `  m
) )  \/  (
( (,) `  (
f `  m )
)  i^i  ( (,) `  ( f `  z
) ) )  =  (/) ) )
6863, 66, 67syl2anc 644 . . . . . . . . . . . . . . . . 17  |-  ( ( f : NN --> { a  e.  { b  e. 
ran  ( x  e.  ZZ ,  y  e. 
NN0  |->  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>. )  |  ( [,] `  b )  C_  A }  |  A. c  e.  { b  e.  ran  ( x  e.  ZZ ,  y  e. 
NN0  |->  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>. )  |  ( [,] `  b )  C_  A }  ( ( [,] `  a )  C_  ( [,] `  c )  ->  a  =  c ) }  /\  (
m  e.  NN  /\  z  e.  NN )
)  ->  ( ( [,] `  ( f `  m ) )  C_  ( [,] `  ( f `
 z ) )  \/  ( [,] `  (
f `  z )
)  C_  ( [,] `  ( f `  m
) )  \/  (
( (,) `  (
f `  m )
)  i^i  ( (,) `  ( f `  z
) ) )  =  (/) ) )
6951, 68sylan 459 . . . . . . . . . . . . . . . 16  |-  ( ( f : NN -1-1-onto-> { a  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A }  |  A. c  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A } 
( ( [,] `  a
)  C_  ( [,] `  c )  ->  a  =  c ) }  /\  ( m  e.  NN  /\  z  e.  NN ) )  -> 
( ( [,] `  (
f `  m )
)  C_  ( [,] `  ( f `  z
) )  \/  ( [,] `  ( f `  z ) )  C_  ( [,] `  ( f `
 m ) )  \/  ( ( (,) `  ( f `  m
) )  i^i  ( (,) `  ( f `  z ) ) )  =  (/) ) )
70 df-3or 938 . . . . . . . . . . . . . . . 16  |-  ( ( ( [,] `  (
f `  m )
)  C_  ( [,] `  ( f `  z
) )  \/  ( [,] `  ( f `  z ) )  C_  ( [,] `  ( f `
 m ) )  \/  ( ( (,) `  ( f `  m
) )  i^i  ( (,) `  ( f `  z ) ) )  =  (/) )  <->  ( (
( [,] `  (
f `  m )
)  C_  ( [,] `  ( f `  z
) )  \/  ( [,] `  ( f `  z ) )  C_  ( [,] `  ( f `
 m ) ) )  \/  ( ( (,) `  ( f `
 m ) )  i^i  ( (,) `  (
f `  z )
) )  =  (/) ) )
7169, 70sylib 190 . . . . . . . . . . . . . . 15  |-  ( ( f : NN -1-1-onto-> { a  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A }  |  A. c  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A } 
( ( [,] `  a
)  C_  ( [,] `  c )  ->  a  =  c ) }  /\  ( m  e.  NN  /\  z  e.  NN ) )  -> 
( ( ( [,] `  ( f `  m
) )  C_  ( [,] `  ( f `  z ) )  \/  ( [,] `  (
f `  z )
)  C_  ( [,] `  ( f `  m
) ) )  \/  ( ( (,) `  (
f `  m )
)  i^i  ( (,) `  ( f `  z
) ) )  =  (/) ) )
72 elrabi 3099 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( f `  z )  e.  { a  e. 
{ b  e.  ran  ( x  e.  ZZ ,  y  e.  NN0  |->  <. ( x  /  (
2 ^ y ) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) ) >.
)  |  ( [,] `  b )  C_  A }  |  A. c  e.  { b  e.  ran  ( x  e.  ZZ ,  y  e.  NN0  |->  <. ( x  /  (
2 ^ y ) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) ) >.
)  |  ( [,] `  b )  C_  A }  ( ( [,] `  a )  C_  ( [,] `  c )  -> 
a  =  c ) }  ->  ( f `  z )  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A }
)
73 fveq2 5763 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( a  =  ( f `  m )  ->  ( [,] `  a )  =  ( [,] `  (
f `  m )
) )
7473sseq1d 3364 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( a  =  ( f `  m )  ->  (
( [,] `  a
)  C_  ( [,] `  c )  <->  ( [,] `  ( f `  m
) )  C_  ( [,] `  c ) ) )
75 eqeq1 2449 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( a  =  ( f `  m )  ->  (
a  =  c  <->  ( f `  m )  =  c ) )
7674, 75imbi12d 313 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( a  =  ( f `  m )  ->  (
( ( [,] `  a
)  C_  ( [,] `  c )  ->  a  =  c )  <->  ( ( [,] `  ( f `  m ) )  C_  ( [,] `  c )  ->  ( f `  m )  =  c ) ) )
7776ralbidv 2732 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( a  =  ( f `  m )  ->  ( A. c  e.  { b  e.  ran  ( x  e.  ZZ ,  y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A } 
( ( [,] `  a
)  C_  ( [,] `  c )  ->  a  =  c )  <->  A. c  e.  { b  e.  ran  ( x  e.  ZZ ,  y  e.  NN0  |->  <. ( x  /  (
2 ^ y ) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) ) >.
)  |  ( [,] `  b )  C_  A }  ( ( [,] `  ( f `  m
) )  C_  ( [,] `  c )  -> 
( f `  m
)  =  c ) ) )
7877elrab 3101 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( f `  m )  e.  { a  e. 
{ b  e.  ran  ( x  e.  ZZ ,  y  e.  NN0  |->  <. ( x  /  (
2 ^ y ) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) ) >.
)  |  ( [,] `  b )  C_  A }  |  A. c  e.  { b  e.  ran  ( x  e.  ZZ ,  y  e.  NN0  |->  <. ( x  /  (
2 ^ y ) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) ) >.
)  |  ( [,] `  b )  C_  A }  ( ( [,] `  a )  C_  ( [,] `  c )  -> 
a  =  c ) }  <->  ( ( f `
 m )  e. 
{ b  e.  ran  ( x  e.  ZZ ,  y  e.  NN0  |->  <. ( x  /  (
2 ^ y ) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) ) >.
)  |  ( [,] `  b )  C_  A }  /\  A. c  e. 
{ b  e.  ran  ( x  e.  ZZ ,  y  e.  NN0  |->  <. ( x  /  (
2 ^ y ) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) ) >.
)  |  ( [,] `  b )  C_  A }  ( ( [,] `  ( f `  m
) )  C_  ( [,] `  c )  -> 
( f `  m
)  =  c ) ) )
7978simprbi 452 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( f `  m )  e.  { a  e. 
{ b  e.  ran  ( x  e.  ZZ ,  y  e.  NN0  |->  <. ( x  /  (
2 ^ y ) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) ) >.
)  |  ( [,] `  b )  C_  A }  |  A. c  e.  { b  e.  ran  ( x  e.  ZZ ,  y  e.  NN0  |->  <. ( x  /  (
2 ^ y ) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) ) >.
)  |  ( [,] `  b )  C_  A }  ( ( [,] `  a )  C_  ( [,] `  c )  -> 
a  =  c ) }  ->  A. c  e.  { b  e.  ran  ( x  e.  ZZ ,  y  e.  NN0  |->  <. ( x  /  (
2 ^ y ) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) ) >.
)  |  ( [,] `  b )  C_  A }  ( ( [,] `  ( f `  m
) )  C_  ( [,] `  c )  -> 
( f `  m
)  =  c ) )
80 fveq2 5763 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( c  =  ( f `  z )  ->  ( [,] `  c )  =  ( [,] `  (
f `  z )
) )
8180sseq2d 3365 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( c  =  ( f `  z )  ->  (
( [,] `  (
f `  m )
)  C_  ( [,] `  c )  <->  ( [,] `  ( f `  m
) )  C_  ( [,] `  ( f `  z ) ) ) )
82 eqeq2 2452 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( c  =  ( f `  z )  ->  (
( f `  m
)  =  c  <->  ( f `  m )  =  ( f `  z ) ) )
8381, 82imbi12d 313 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( c  =  ( f `  z )  ->  (
( ( [,] `  (
f `  m )
)  C_  ( [,] `  c )  ->  (
f `  m )  =  c )  <->  ( ( [,] `  ( f `  m ) )  C_  ( [,] `  ( f `
 z ) )  ->  ( f `  m )  =  ( f `  z ) ) ) )
8483rspcva 3059 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( f `  z
)  e.  { b  e.  ran  ( x  e.  ZZ ,  y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A }  /\  A. c  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A } 
( ( [,] `  (
f `  m )
)  C_  ( [,] `  c )  ->  (
f `  m )  =  c ) )  ->  ( ( [,] `  ( f `  m
) )  C_  ( [,] `  ( f `  z ) )  -> 
( f `  m
)  =  ( f `
 z ) ) )
8572, 79, 84syl2anr 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( f `  m
)  e.  { a  e.  { b  e. 
ran  ( x  e.  ZZ ,  y  e. 
NN0  |->  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>. )  |  ( [,] `  b )  C_  A }  |  A. c  e.  { b  e.  ran  ( x  e.  ZZ ,  y  e. 
NN0  |->  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>. )  |  ( [,] `  b )  C_  A }  ( ( [,] `  a )  C_  ( [,] `  c )  ->  a  =  c ) }  /\  (
f `  z )  e.  { a  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A }  |  A. c  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A } 
( ( [,] `  a
)  C_  ( [,] `  c )  ->  a  =  c ) } )  ->  ( ( [,] `  ( f `  m ) )  C_  ( [,] `  ( f `
 z ) )  ->  ( f `  m )  =  ( f `  z ) ) )
86 elrabi 3099 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( f `  m )  e.  { a  e. 
{ b  e.  ran  ( x  e.  ZZ ,  y  e.  NN0  |->  <. ( x  /  (
2 ^ y ) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) ) >.
)  |  ( [,] `  b )  C_  A }  |  A. c  e.  { b  e.  ran  ( x  e.  ZZ ,  y  e.  NN0  |->  <. ( x  /  (
2 ^ y ) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) ) >.
)  |  ( [,] `  b )  C_  A }  ( ( [,] `  a )  C_  ( [,] `  c )  -> 
a  =  c ) }  ->  ( f `  m )  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A }
)
87 fveq2 5763 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( a  =  ( f `  z )  ->  ( [,] `  a )  =  ( [,] `  (
f `  z )
) )
8887sseq1d 3364 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( a  =  ( f `  z )  ->  (
( [,] `  a
)  C_  ( [,] `  c )  <->  ( [,] `  ( f `  z
) )  C_  ( [,] `  c ) ) )
89 eqeq1 2449 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( a  =  ( f `  z )  ->  (
a  =  c  <->  ( f `  z )  =  c ) )
9088, 89imbi12d 313 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( a  =  ( f `  z )  ->  (
( ( [,] `  a
)  C_  ( [,] `  c )  ->  a  =  c )  <->  ( ( [,] `  ( f `  z ) )  C_  ( [,] `  c )  ->  ( f `  z )  =  c ) ) )
9190ralbidv 2732 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( a  =  ( f `  z )  ->  ( A. c  e.  { b  e.  ran  ( x  e.  ZZ ,  y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A } 
( ( [,] `  a
)  C_  ( [,] `  c )  ->  a  =  c )  <->  A. c  e.  { b  e.  ran  ( x  e.  ZZ ,  y  e.  NN0  |->  <. ( x  /  (
2 ^ y ) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) ) >.
)  |  ( [,] `  b )  C_  A }  ( ( [,] `  ( f `  z
) )  C_  ( [,] `  c )  -> 
( f `  z
)  =  c ) ) )
9291elrab 3101 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( f `  z )  e.  { a  e. 
{ b  e.  ran  ( x  e.  ZZ ,  y  e.  NN0  |->  <. ( x  /  (
2 ^ y ) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) ) >.
)  |  ( [,] `  b )  C_  A }  |  A. c  e.  { b  e.  ran  ( x  e.  ZZ ,  y  e.  NN0  |->  <. ( x  /  (
2 ^ y ) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) ) >.
)  |  ( [,] `  b )  C_  A }  ( ( [,] `  a )  C_  ( [,] `  c )  -> 
a  =  c ) }  <->  ( ( f `
 z )  e. 
{ b  e.  ran  ( x  e.  ZZ ,  y  e.  NN0  |->  <. ( x  /  (
2 ^ y ) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) ) >.
)  |  ( [,] `  b )  C_  A }  /\  A. c  e. 
{ b  e.  ran  ( x  e.  ZZ ,  y  e.  NN0  |->  <. ( x  /  (
2 ^ y ) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) ) >.
)  |  ( [,] `  b )  C_  A }  ( ( [,] `  ( f `  z
) )  C_  ( [,] `  c )  -> 
( f `  z
)  =  c ) ) )
9392simprbi 452 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( f `  z )  e.  { a  e. 
{ b  e.  ran  ( x  e.  ZZ ,  y  e.  NN0  |->  <. ( x  /  (
2 ^ y ) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) ) >.
)  |  ( [,] `  b )  C_  A }  |  A. c  e.  { b  e.  ran  ( x  e.  ZZ ,  y  e.  NN0  |->  <. ( x  /  (
2 ^ y ) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) ) >.
)  |  ( [,] `  b )  C_  A }  ( ( [,] `  a )  C_  ( [,] `  c )  -> 
a  =  c ) }  ->  A. c  e.  { b  e.  ran  ( x  e.  ZZ ,  y  e.  NN0  |->  <. ( x  /  (
2 ^ y ) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) ) >.
)  |  ( [,] `  b )  C_  A }  ( ( [,] `  ( f `  z
) )  C_  ( [,] `  c )  -> 
( f `  z
)  =  c ) )
94 fveq2 5763 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( c  =  ( f `  m )  ->  ( [,] `  c )  =  ( [,] `  (
f `  m )
) )
9594sseq2d 3365 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( c  =  ( f `  m )  ->  (
( [,] `  (
f `  z )
)  C_  ( [,] `  c )  <->  ( [,] `  ( f `  z
) )  C_  ( [,] `  ( f `  m ) ) ) )
96 eqeq2 2452 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( c  =  ( f `  m )  ->  (
( f `  z
)  =  c  <->  ( f `  z )  =  ( f `  m ) ) )
9795, 96imbi12d 313 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( c  =  ( f `  m )  ->  (
( ( [,] `  (
f `  z )
)  C_  ( [,] `  c )  ->  (
f `  z )  =  c )  <->  ( ( [,] `  ( f `  z ) )  C_  ( [,] `  ( f `
 m ) )  ->  ( f `  z )  =  ( f `  m ) ) ) )
9897rspcva 3059 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( f `  m
)  e.  { b  e.  ran  ( x  e.  ZZ ,  y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A }  /\  A. c  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A } 
( ( [,] `  (
f `  z )
)  C_  ( [,] `  c )  ->  (
f `  z )  =  c ) )  ->  ( ( [,] `  ( f `  z
) )  C_  ( [,] `  ( f `  m ) )  -> 
( f `  z
)  =  ( f `
 m ) ) )
9986, 93, 98syl2an 465 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( f `  m
)  e.  { a  e.  { b  e. 
ran  ( x  e.  ZZ ,  y  e. 
NN0  |->  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>. )  |  ( [,] `  b )  C_  A }  |  A. c  e.  { b  e.  ran  ( x  e.  ZZ ,  y  e. 
NN0  |->  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>. )  |  ( [,] `  b )  C_  A }  ( ( [,] `  a )  C_  ( [,] `  c )  ->  a  =  c ) }  /\  (
f `  z )  e.  { a  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A }  |  A. c  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A } 
( ( [,] `  a
)  C_  ( [,] `  c )  ->  a  =  c ) } )  ->  ( ( [,] `  ( f `  z ) )  C_  ( [,] `  ( f `
 m ) )  ->  ( f `  z )  =  ( f `  m ) ) )
100 eqcom 2445 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( f `  z )  =  ( f `  m )  <->  ( f `  m )  =  ( f `  z ) )
10199, 100syl6ib 219 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( f `  m
)  e.  { a  e.  { b  e. 
ran  ( x  e.  ZZ ,  y  e. 
NN0  |->  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>. )  |  ( [,] `  b )  C_  A }  |  A. c  e.  { b  e.  ran  ( x  e.  ZZ ,  y  e. 
NN0  |->  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>. )  |  ( [,] `  b )  C_  A }  ( ( [,] `  a )  C_  ( [,] `  c )  ->  a  =  c ) }  /\  (
f `  z )  e.  { a  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A }  |  A. c  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A } 
( ( [,] `  a
)  C_  ( [,] `  c )  ->  a  =  c ) } )  ->  ( ( [,] `  ( f `  z ) )  C_  ( [,] `  ( f `
 m ) )  ->  ( f `  m )  =  ( f `  z ) ) )
10285, 101jaod 371 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( f `  m
)  e.  { a  e.  { b  e. 
ran  ( x  e.  ZZ ,  y  e. 
NN0  |->  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>. )  |  ( [,] `  b )  C_  A }  |  A. c  e.  { b  e.  ran  ( x  e.  ZZ ,  y  e. 
NN0  |->  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>. )  |  ( [,] `  b )  C_  A }  ( ( [,] `  a )  C_  ( [,] `  c )  ->  a  =  c ) }  /\  (
f `  z )  e.  { a  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A }  |  A. c  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A } 
( ( [,] `  a
)  C_  ( [,] `  c )  ->  a  =  c ) } )  ->  ( (
( [,] `  (
f `  m )
)  C_  ( [,] `  ( f `  z
) )  \/  ( [,] `  ( f `  z ) )  C_  ( [,] `  ( f `
 m ) ) )  ->  ( f `  m )  =  ( f `  z ) ) )
10361, 64, 102syl2an 465 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( f : NN --> { a  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A }  |  A. c  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A } 
( ( [,] `  a
)  C_  ( [,] `  c )  ->  a  =  c ) }  /\  m  e.  NN )  /\  ( f : NN --> { a  e. 
{ b  e.  ran  ( x  e.  ZZ ,  y  e.  NN0  |->  <. ( x  /  (
2 ^ y ) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) ) >.
)  |  ( [,] `  b )  C_  A }  |  A. c  e.  { b  e.  ran  ( x  e.  ZZ ,  y  e.  NN0  |->  <. ( x  /  (
2 ^ y ) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) ) >.
)  |  ( [,] `  b )  C_  A }  ( ( [,] `  a )  C_  ( [,] `  c )  -> 
a  =  c ) }  /\  z  e.  NN ) )  -> 
( ( ( [,] `  ( f `  m
) )  C_  ( [,] `  ( f `  z ) )  \/  ( [,] `  (
f `  z )
)  C_  ( [,] `  ( f `  m
) ) )  -> 
( f `  m
)  =  ( f `
 z ) ) )
104103anandis 805 . . . . . . . . . . . . . . . . . 18  |-  ( ( f : NN --> { a  e.  { b  e. 
ran  ( x  e.  ZZ ,  y  e. 
NN0  |->  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>. )  |  ( [,] `  b )  C_  A }  |  A. c  e.  { b  e.  ran  ( x  e.  ZZ ,  y  e. 
NN0  |->  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>. )  |  ( [,] `  b )  C_  A }  ( ( [,] `  a )  C_  ( [,] `  c )  ->  a  =  c ) }  /\  (
m  e.  NN  /\  z  e.  NN )
)  ->  ( (
( [,] `  (
f `  m )
)  C_  ( [,] `  ( f `  z
) )  \/  ( [,] `  ( f `  z ) )  C_  ( [,] `  ( f `
 m ) ) )  ->  ( f `  m )  =  ( f `  z ) ) )
10551, 104sylan 459 . . . . . . . . . . . . . . . . 17  |-  ( ( f : NN -1-1-onto-> { a  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A }  |  A. c  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A } 
( ( [,] `  a
)  C_  ( [,] `  c )  ->  a  =  c ) }  /\  ( m  e.  NN  /\  z  e.  NN ) )  -> 
( ( ( [,] `  ( f `  m
) )  C_  ( [,] `  ( f `  z ) )  \/  ( [,] `  (
f `  z )
)  C_  ( [,] `  ( f `  m
) ) )  -> 
( f `  m
)  =  ( f `
 z ) ) )
106 f1of1 5708 . . . . . . . . . . . . . . . . . 18  |-  ( f : NN -1-1-onto-> { a  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A }  |  A. c  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A } 
( ( [,] `  a
)  C_  ( [,] `  c )  ->  a  =  c ) }  ->  f : NN -1-1-> { a  e.  { b  e.  ran  ( x  e.  ZZ ,  y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A }  |  A. c  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A } 
( ( [,] `  a
)  C_  ( [,] `  c )  ->  a  =  c ) } )
107 f1veqaeq 6041 . . . . . . . . . . . . . . . . . 18  |-  ( ( f : NN -1-1-> {
a  e.  { b  e.  ran  ( x  e.  ZZ ,  y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A }  |  A. c  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A } 
( ( [,] `  a
)  C_  ( [,] `  c )  ->  a  =  c ) }  /\  ( m  e.  NN  /\  z  e.  NN ) )  -> 
( ( f `  m )  =  ( f `  z )  ->  m  =  z ) )
108106, 107sylan 459 . . . . . . . . . . . . . . . . 17  |-  ( ( f : NN -1-1-onto-> { a  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A }  |  A. c  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A } 
( ( [,] `  a
)  C_  ( [,] `  c )  ->  a  =  c ) }  /\  ( m  e.  NN  /\  z  e.  NN ) )  -> 
( ( f `  m )  =  ( f `  z )  ->  m  =  z ) )
109105, 108syld 43 . . . . . . . . . . . . . . . 16  |-  ( ( f : NN -1-1-onto-> { a  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A }  |  A. c  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A } 
( ( [,] `  a
)  C_  ( [,] `  c )  ->  a  =  c ) }  /\  ( m  e.  NN  /\  z  e.  NN ) )  -> 
( ( ( [,] `  ( f `  m
) )  C_  ( [,] `  ( f `  z ) )  \/  ( [,] `  (
f `  z )
)  C_  ( [,] `  ( f `  m
) ) )  ->  m  =  z )
)
110109orim1d 814 . . . . . . . . . . . . . . 15  |-  ( ( f : NN -1-1-onto-> { a  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A }  |  A. c  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A } 
( ( [,] `  a
)  C_  ( [,] `  c )  ->  a  =  c ) }  /\  ( m  e.  NN  /\  z  e.  NN ) )  -> 
( ( ( ( [,] `  ( f `
 m ) ) 
C_  ( [,] `  (
f `  z )
)  \/  ( [,] `  ( f `  z
) )  C_  ( [,] `  ( f `  m ) ) )  \/  ( ( (,) `  ( f `  m
) )  i^i  ( (,) `  ( f `  z ) ) )  =  (/) )  ->  (
m  =  z  \/  ( ( (,) `  (
f `  m )
)  i^i  ( (,) `  ( f `  z
) ) )  =  (/) ) ) )
11171, 110mpd 15 . . . . . . . . . . . . . 14  |-  ( ( f : NN -1-1-onto-> { a  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A }  |  A. c  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A } 
( ( [,] `  a
)  C_  ( [,] `  c )  ->  a  =  c ) }  /\  ( m  e.  NN  /\  z  e.  NN ) )  -> 
( m  =  z  \/  ( ( (,) `  ( f `  m
) )  i^i  ( (,) `  ( f `  z ) ) )  =  (/) ) )
112111ralrimivva 2805 . . . . . . . . . . . . 13  |-  ( f : NN -1-1-onto-> { a  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A }  |  A. c  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A } 
( ( [,] `  a
)  C_  ( [,] `  c )  ->  a  =  c ) }  ->  A. m  e.  NN  A. z  e.  NN  (
m  =  z  \/  ( ( (,) `  (
f `  m )
)  i^i  ( (,) `  ( f `  z
) ) )  =  (/) ) )
113 eqeq1 2449 . . . . . . . . . . . . . . . . 17  |-  ( m  =  z  ->  (
m  =  p  <->  z  =  p ) )
114 fveq2 5763 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  =  z  ->  (
f `  m )  =  ( f `  z ) )
115114fveq2d 5767 . . . . . . . . . . . . . . . . . . 19  |-  ( m  =  z  ->  ( (,) `  ( f `  m ) )  =  ( (,) `  (
f `  z )
) )
116115ineq1d 3530 . . . . . . . . . . . . . . . . . 18  |-  ( m  =  z  ->  (
( (,) `  (
f `  m )
)  i^i  ( (,) `  ( f `  p
) ) )  =  ( ( (,) `  (
f `  z )
)  i^i  ( (,) `  ( f `  p
) ) ) )
117116eqeq1d 2451 . . . . . . . . . . . . . . . . 17  |-  ( m  =  z  ->  (
( ( (,) `  (
f `  m )
)  i^i  ( (,) `  ( f `  p
) ) )  =  (/) 
<->  ( ( (,) `  (
f `  z )
)  i^i  ( (,) `  ( f `  p
) ) )  =  (/) ) )
118113, 117orbi12d 692 . . . . . . . . . . . . . . . 16  |-  ( m  =  z  ->  (
( m  =  p  \/  ( ( (,) `  ( f `  m
) )  i^i  ( (,) `  ( f `  p ) ) )  =  (/) )  <->  ( z  =  p  \/  (
( (,) `  (
f `  z )
)  i^i  ( (,) `  ( f `  p
) ) )  =  (/) ) ) )
119118ralbidv 2732 . . . . . . . . . . . . . . 15  |-  ( m  =  z  ->  ( A. p  e.  NN  ( m  =  p  \/  ( ( (,) `  (
f `  m )
)  i^i  ( (,) `  ( f `  p
) ) )  =  (/) )  <->  A. p  e.  NN  ( z  =  p  \/  ( ( (,) `  ( f `  z
) )  i^i  ( (,) `  ( f `  p ) ) )  =  (/) ) ) )
120119cbvralv 2941 . . . . . . . . . . . . . 14  |-  ( A. m  e.  NN  A. p  e.  NN  ( m  =  p  \/  ( ( (,) `  ( f `
 m ) )  i^i  ( (,) `  (
f `  p )
) )  =  (/) ) 
<-> 
A. z  e.  NN  A. p  e.  NN  (
z  =  p  \/  ( ( (,) `  (
f `  z )
)  i^i  ( (,) `  ( f `  p
) ) )  =  (/) ) )
121 eqeq2 2452 . . . . . . . . . . . . . . . . 17  |-  ( z  =  p  ->  (
m  =  z  <->  m  =  p ) )
122 fveq2 5763 . . . . . . . . . . . . . . . . . . . 20  |-  ( z  =  p  ->  (
f `  z )  =  ( f `  p ) )
123122fveq2d 5767 . . . . . . . . . . . . . . . . . . 19  |-  ( z  =  p  ->  ( (,) `  ( f `  z ) )  =  ( (,) `  (
f `  p )
) )
124123ineq2d 3531 . . . . . . . . . . . . . . . . . 18  |-  ( z  =  p  ->  (
( (,) `  (
f `  m )
)  i^i  ( (,) `  ( f `  z
) ) )  =  ( ( (,) `  (
f `  m )
)  i^i  ( (,) `  ( f `  p
) ) ) )
125124eqeq1d 2451 . . . . . . . . . . . . . . . . 17  |-  ( z  =  p  ->  (
( ( (,) `  (
f `  m )
)  i^i  ( (,) `  ( f `  z
) ) )  =  (/) 
<->  ( ( (,) `  (
f `  m )
)  i^i  ( (,) `  ( f `  p
) ) )  =  (/) ) )
126121, 125orbi12d 692 . . . . . . . . . . . . . . . 16  |-  ( z  =  p  ->  (
( m  =  z  \/  ( ( (,) `  ( f `  m
) )  i^i  ( (,) `  ( f `  z ) ) )  =  (/) )  <->  ( m  =  p  \/  (
( (,) `  (
f `  m )
)  i^i  ( (,) `  ( f `  p
) ) )  =  (/) ) ) )
127126cbvralv 2941 . . . . . . . . . . . . . . 15  |-  ( A. z  e.  NN  (
m  =  z  \/  ( ( (,) `  (
f `  m )
)  i^i  ( (,) `  ( f `  z
) ) )  =  (/) )  <->  A. p  e.  NN  ( m  =  p  \/  ( ( (,) `  (
f `  m )
)  i^i  ( (,) `  ( f `  p
) ) )  =  (/) ) )
128127ralbii 2736 . . . . . . . . . . . . . 14  |-  ( A. m  e.  NN  A. z  e.  NN  ( m  =  z  \/  ( ( (,) `  ( f `
 m ) )  i^i  ( (,) `  (
f `  z )
) )  =  (/) ) 
<-> 
A. m  e.  NN  A. p  e.  NN  (
m  =  p  \/  ( ( (,) `  (
f `  m )
)  i^i  ( (,) `  ( f `  p
) ) )  =  (/) ) )
129123disjor 4227 . . . . . . . . . . . . . 14  |-  (Disj  z  e.  NN ( (,) `  (
f `  z )
)  <->  A. z  e.  NN  A. p  e.  NN  (
z  =  p  \/  ( ( (,) `  (
f `  z )
)  i^i  ( (,) `  ( f `  p
) ) )  =  (/) ) )
130120, 128, 1293bitr4ri 271 . . . . . . . . . . . . 13  |-  (Disj  z  e.  NN ( (,) `  (
f `  z )
)  <->  A. m  e.  NN  A. z  e.  NN  (
m  =  z  \/  ( ( (,) `  (
f `  m )
)  i^i  ( (,) `  ( f `  z
) ) )  =  (/) ) )
131112, 130sylibr 205 . . . . . . . . . . . 12  |-  ( f : NN -1-1-onto-> { a  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A }  |  A. c  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A } 
( ( [,] `  a
)  C_  ( [,] `  c )  ->  a  =  c ) }  -> Disj  z  e.  NN ( (,) `  ( f `
 z ) ) )
132 eqid 2443 . . . . . . . . . . . 12  |-  seq  1
(  +  ,  ( ( abs  o.  -  )  o.  f )
)  =  seq  1
(  +  ,  ( ( abs  o.  -  )  o.  f )
)
13359, 131, 132uniiccvol 19510 . . . . . . . . . . 11  |-  ( f : NN -1-1-onto-> { a  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A }  |  A. c  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A } 
( ( [,] `  a
)  C_  ( [,] `  c )  ->  a  =  c ) }  ->  ( vol * `  U. ran  ( [,] 
o.  f ) )  =  sup ( ran 
seq  1 (  +  ,  ( ( abs 
o.  -  )  o.  f ) ) , 
RR* ,  <  ) )
134133adantl 454 . . . . . . . . . 10  |-  ( ( ( A  e.  (
topGen `  ran  (,) )  /\  M  e.  RR  /\  M  <  ( vol
* `  A )
)  /\  f : NN
-1-1-onto-> { a  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A }  |  A. c  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A } 
( ( [,] `  a
)  C_  ( [,] `  c )  ->  a  =  c ) } )  ->  ( vol * `
 U. ran  ( [,]  o.  f ) )  =  sup ( ran 
seq  1 (  +  ,  ( ( abs 
o.  -  )  o.  f ) ) , 
RR* ,  <  ) )
13550, 134eqtr3d 2477 . . . . . . . . 9  |-  ( ( ( A  e.  (
topGen `  ran  (,) )  /\  M  e.  RR  /\  M  <  ( vol
* `  A )
)  /\  f : NN
-1-1-onto-> { a  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A }  |  A. c  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A } 
( ( [,] `  a
)  C_  ( [,] `  c )  ->  a  =  c ) } )  ->  ( vol * `
 A )  =  sup ( ran  seq  1 (  +  , 
( ( abs  o.  -  )  o.  f
) ) ,  RR* ,  <  ) )
13618, 135breqtrd 4267 . . . . . . . 8  |-  ( ( ( A  e.  (
topGen `  ran  (,) )  /\  M  e.  RR  /\  M  <  ( vol
* `  A )
)  /\  f : NN
-1-1-onto-> { a  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A }  |  A. c  e.  {
b  e.  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A } 
( ( [,] `  a
)  C_  ( [,] `  c )  ->  a  =  c ) } )  ->  M  <  sup ( ran  seq  1
(  +  ,  ( ( abs  o.  -  )  o.  f )
) ,  RR* ,  <  ) )
137 absf 12179 . . . . . . . . . . . 12  |-  abs : CC
--> RR
138 subf 9345 . . . . . . . . . . . 12  |-  -  :
( CC  X.  CC )
--> CC
139 fco 5635 . . . . . . . . . . . 12  |-  ( ( abs : CC --> RR  /\  -  : ( CC  X.  CC ) --> CC )  -> 
( abs  o.  -  ) : ( CC  X.  CC ) --> RR )
140137, 138, 139mp2an 655 . . . . . . . . . . 11  |-  ( abs 
o.  -  ) :
( CC  X.  CC )
--> RR
141 zre 10324 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  ZZ  ->  x  e.  RR )
142 2re 10107 . . . . . . . . . . . . . . . . . . . . 21  |-  2  e.  RR
143 reexpcl 11436 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 2  e.  RR  /\  y  e.  NN0 )  -> 
( 2 ^ y
)  e.  RR )
144142, 143mpan 653 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  NN0  ->  ( 2 ^ y )  e.  RR )
145 nn0z 10342 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  NN0  ->  y  e.  ZZ )
146 2cn 10108 . . . . . . . . . . . . . . . . . . . . . 22  |-  2  e.  CC
147 2ne0 10121 . . . . . . . . . . . . . . . . . . . . . 22  |-  2  =/=  0
148 expne0i 11450 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( 2  e.  CC  /\  2  =/=  0  /\  y  e.  ZZ )  ->  (
2 ^ y )  =/=  0 )
149146, 147, 148mp3an12 1270 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  ZZ  ->  (
2 ^ y )  =/=  0 )
150145, 149syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  NN0  ->  ( 2 ^ y )  =/=  0 )
151144, 150jca 520 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  NN0  ->  ( ( 2 ^ y )  e.  RR  /\  (
2 ^ y )  =/=  0 ) )
152 redivcl 9771 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  e.  RR  /\  ( 2 ^ y
)  e.  RR  /\  ( 2 ^ y
)  =/=  0 )  ->  ( x  / 
( 2 ^ y
) )  e.  RR )
153 peano2re 9277 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  RR  ->  (
x  +  1 )  e.  RR )
154 redivcl 9771 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( x  +  1 )  e.  RR  /\  ( 2 ^ y
)  e.  RR  /\  ( 2 ^ y
)  =/=  0 )  ->  ( ( x  +  1 )  / 
( 2 ^ y
) )  e.  RR )
155153, 154syl3an1 1218 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  e.  RR  /\  ( 2 ^ y
)  e.  RR  /\  ( 2 ^ y
)  =/=  0 )  ->  ( ( x  +  1 )  / 
( 2 ^ y
) )  e.  RR )
156 opelxpi 4945 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( x  /  (
2 ^ y ) )  e.  RR  /\  ( ( x  + 
1 )  /  (
2 ^ y ) )  e.  RR )  ->  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>.  e.  ( RR  X.  RR ) )
157152, 155, 156syl2anc 644 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( x  e.  RR  /\  ( 2 ^ y
)  e.  RR  /\  ( 2 ^ y
)  =/=  0 )  ->  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>.  e.  ( RR  X.  RR ) )
1581573expb 1155 . . . . . . . . . . . . . . . . . . 19  |-  ( ( x  e.  RR  /\  ( ( 2 ^ y )  e.  RR  /\  ( 2 ^ y
)  =/=  0 ) )  ->  <. ( x  /  ( 2 ^ y ) ) ,  ( ( x  + 
1 )  /  (
2 ^ y ) ) >.  e.  ( RR  X.  RR ) )
159141, 151, 158syl2an 465 . . . . . . . . . . . . . . . . . 18  |-  ( ( x  e.  ZZ  /\  y  e.  NN0 )  ->  <. ( x  /  (
2 ^ y ) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) ) >.  e.  ( RR  X.  RR ) )
160159rgen2 2809 . . . . . . . . . . . . . . . . 17  |-  A. x  e.  ZZ  A. y  e. 
NN0  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>.  e.  ( RR  X.  RR )
161 eqid 2443 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  ZZ ,  y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  =  ( x  e.  ZZ