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

Theorem mblfinlem2 31892
Description: Lemma for ismblfin 31895, 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 21769 . . . 4  |-  ( topGen ` 
ran  (,) )  e.  Top
2 0cld 20040 . . . 4  |-  ( (
topGen `  ran  (,) )  e.  Top  ->  (/)  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) )
31, 2ax-mp 5 . . 3  |-  (/)  e.  (
Clsd `  ( topGen ` 
ran  (,) ) )
4 simpl3 1010 . . . . 5  |-  ( ( ( A  e.  (
topGen `  ran  (,) )  /\  M  e.  RR  /\  M  <  ( vol* `  A )
)  /\  A  =  (/) )  ->  M  <  ( vol* `  A
) )
5 fveq2 5878 . . . . . 6  |-  ( A  =  (/)  ->  ( vol* `  A )  =  ( vol* `  (/) ) )
65adantl 467 . . . . 5  |-  ( ( ( A  e.  (
topGen `  ran  (,) )  /\  M  e.  RR  /\  M  <  ( vol* `  A )
)  /\  A  =  (/) )  ->  ( vol* `  A )  =  ( vol* `  (/) ) )
74, 6breqtrd 4445 . . . 4  |-  ( ( ( A  e.  (
topGen `  ran  (,) )  /\  M  e.  RR  /\  M  <  ( vol* `  A )
)  /\  A  =  (/) )  ->  M  <  ( vol* `  (/) ) )
8 0ss 3791 . . . 4  |-  (/)  C_  A
97, 8jctil 539 . . 3  |-  ( ( ( A  e.  (
topGen `  ran  (,) )  /\  M  e.  RR  /\  M  <  ( vol* `  A )
)  /\  A  =  (/) )  ->  ( (/)  C_  A  /\  M  <  ( vol* `  (/) ) ) )
10 sseq1 3485 . . . . 5  |-  ( s  =  (/)  ->  ( s 
C_  A  <->  (/)  C_  A
) )
11 fveq2 5878 . . . . . 6  |-  ( s  =  (/)  ->  ( vol* `  s )  =  ( vol* `  (/) ) )
1211breq2d 4432 . . . . 5  |-  ( s  =  (/)  ->  ( M  <  ( vol* `  s )  <->  M  <  ( vol* `  (/) ) ) )
1310, 12anbi12d 715 . . . 4  |-  ( s  =  (/)  ->  ( ( s  C_  A  /\  M  <  ( vol* `  s ) )  <->  ( (/)  C_  A  /\  M  <  ( vol* `  (/) ) ) ) )
1413rspcev 3182 . . 3  |-  ( (
(/)  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( (/)  C_  A  /\  M  <  ( vol* `  (/) ) ) )  ->  E. s  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( s  C_  A  /\  M  <  ( vol* `  s ) ) )
153, 9, 14sylancr 667 . 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 31891 . . . 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 1167 . . 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 1010 . . . . . . . . 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 5835 . . . . . . . . . . . . . 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 5358 . . . . . . . . . . . . . . . 16  |-  ran  ( [,]  o.  f )  =  ( [,] " ran  f )
21 forn 5810 . . . . . . . . . . . . . . . . 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 5184 . . . . . . . . . . . . . . . 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 2475 . . . . . . . . . . . . . . 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 4226 . . . . . . . . . . . . . 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 17 . . . . . . . . . . . . 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 467 . . . . . . . . . . . 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 6309 . . . . . . . . . . . . . . . 16  |-  ( x  =  u  ->  (
x  /  ( 2 ^ y ) )  =  ( u  / 
( 2 ^ y
) ) )
28 oveq1 6309 . . . . . . . . . . . . . . . . 17  |-  ( x  =  u  ->  (
x  +  1 )  =  ( u  + 
1 ) )
2928oveq1d 6317 . . . . . . . . . . . . . . . 16  |-  ( x  =  u  ->  (
( x  +  1 )  /  ( 2 ^ y ) )  =  ( ( u  +  1 )  / 
( 2 ^ y
) ) )
3027, 29opeq12d 4192 . . . . . . . . . . . . . . 15  |-  ( x  =  u  ->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >.  =  <. ( u  /  ( 2 ^ y ) ) ,  ( ( u  +  1 )  / 
( 2 ^ y
) ) >. )
31 oveq2 6310 . . . . . . . . . . . . . . . . 17  |-  ( y  =  v  ->  (
2 ^ y )  =  ( 2 ^ v ) )
3231oveq2d 6318 . . . . . . . . . . . . . . . 16  |-  ( y  =  v  ->  (
u  /  ( 2 ^ y ) )  =  ( u  / 
( 2 ^ v
) ) )
3331oveq2d 6318 . . . . . . . . . . . . . . . 16  |-  ( y  =  v  ->  (
( u  +  1 )  /  ( 2 ^ y ) )  =  ( ( u  +  1 )  / 
( 2 ^ v
) ) )
3432, 33opeq12d 4192 . . . . . . . . . . . . . . 15  |-  ( y  =  v  ->  <. (
u  /  ( 2 ^ y ) ) ,  ( ( u  +  1 )  / 
( 2 ^ y
) ) >.  =  <. ( u  /  ( 2 ^ v ) ) ,  ( ( u  +  1 )  / 
( 2 ^ v
) ) >. )
3530, 34cbvmpt2v 6382 . . . . . . . . . . . . . 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 5878 . . . . . . . . . . . . . . . . . 18  |-  ( a  =  z  ->  ( [,] `  a )  =  ( [,] `  z
) )
3736sseq1d 3491 . . . . . . . . . . . . . . . . 17  |-  ( a  =  z  ->  (
( [,] `  a
)  C_  ( [,] `  c )  <->  ( [,] `  z )  C_  ( [,] `  c ) ) )
38 eqeq1 2426 . . . . . . . . . . . . . . . . 17  |-  ( a  =  z  ->  (
a  =  c  <->  z  =  c ) )
3937, 38imbi12d 321 . . . . . . . . . . . . . . . 16  |-  ( a  =  z  ->  (
( ( [,] `  a
)  C_  ( [,] `  c )  ->  a  =  c )  <->  ( ( [,] `  z )  C_  ( [,] `  c )  ->  z  =  c ) ) )
4039ralbidv 2864 . . . . . . . . . . . . . . 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 3080 . . . . . . . . . . . . . 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 3546 . . . . . . . . . . . . . . 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 22544 . . . . . . . . . . . . 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 466 . . . . . . . . . . . 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 31890 . . . . . . . . . . . . . 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 1026 . . . . . . . . . . . . 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 466 . . . . . . . . . . . 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 2469 . . . . . . . . . . 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 5882 . . . . . . . . . 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 5828 . . . . . . . . . . . . 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 3546 . . . . . . . . . . . . . 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 22536 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ZZ ,  y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. ) : ( ZZ  X.  NN0 ) --> (  <_  i^i  ( RR  X.  RR ) )
54 frn 5749 . . . . . . . . . . . . . . . 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 3473 . . . . . . . . . . . . . 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 3473 . . . . . . . . . . . . 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 5751 . . . . . . . . . . . . 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 666 . . . . . . . . . . . 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 3473 . . . . . . . . . . . . . . . . . . . 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 6032 . . . . . . . . . . . . . . . . . . . 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 3462 . . . . . . . . . . . . . . . . . . 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 721 . . . . . . . . . . . . . . . . . 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 6032 . . . . . . . . . . . . . . . . . . . 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 3462 . . . . . . . . . . . . . . . . . . 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 720 . . . . . . . . . . . . . . . . . 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 22541 . . . . . . . . . . . . . . . . . 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 665 . . . . . . . . . . . . . . . . 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 473 . . . . . . . . . . . . . . . 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 983 . . . . . . . . . . . . . . . 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 199 . . . . . . . . . . . . . . 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 3226 . . . . . . . . . . . . . . . . . . . . . 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 5878 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( a  =  ( f `  m )  ->  ( [,] `  a )  =  ( [,] `  (
f `  m )
) )
7473sseq1d 3491 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( a  =  ( f `  m )  ->  (
( [,] `  a
)  C_  ( [,] `  c )  <->  ( [,] `  ( f `  m
) )  C_  ( [,] `  c ) ) )
75 eqeq1 2426 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( a  =  ( f `  m )  ->  (
a  =  c  <->  ( f `  m )  =  c ) )
7674, 75imbi12d 321 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( a  =  ( f `  m )  ->  (
( ( [,] `  a
)  C_  ( [,] `  c )  ->  a  =  c )  <->  ( ( [,] `  ( f `  m ) )  C_  ( [,] `  c )  ->  ( f `  m )  =  c ) ) )
7776ralbidv 2864 . . . . . . . . . . . . . . . . . . . . . . . 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 3229 . . . . . . . . . . . . . . . . . . . . . . 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 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 ) }  ->  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 5878 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( c  =  ( f `  z )  ->  ( [,] `  c )  =  ( [,] `  (
f `  z )
) )
8180sseq2d 3492 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( c  =  ( f `  z )  ->  (
( [,] `  (
f `  m )
)  C_  ( [,] `  c )  <->  ( [,] `  ( f `  m
) )  C_  ( [,] `  ( f `  z ) ) ) )
82 eqeq2 2437 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( c  =  ( f `  z )  ->  (
( f `  m
)  =  c  <->  ( f `  m )  =  ( f `  z ) ) )
8381, 82imbi12d 321 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( c  =  ( f `  z )  ->  (
( ( [,] `  (
f `  m )
)  C_  ( [,] `  c )  ->  (
f `  m )  =  c )  <->  ( ( [,] `  ( f `  m ) )  C_  ( [,] `  ( f `
 z ) )  ->  ( f `  m )  =  ( f `  z ) ) ) )
8483rspcva 3180 . . . . . . . . . . . . . . . . . . . . . 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 480 . . . . . . . . . . . . . . . . . . . . 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 3226 . . . . . . . . . . . . . . . . . . . . . . 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 5878 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( a  =  ( f `  z )  ->  ( [,] `  a )  =  ( [,] `  (
f `  z )
) )
8887sseq1d 3491 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( a  =  ( f `  z )  ->  (
( [,] `  a
)  C_  ( [,] `  c )  <->  ( [,] `  ( f `  z
) )  C_  ( [,] `  c ) ) )
89 eqeq1 2426 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( a  =  ( f `  z )  ->  (
a  =  c  <->  ( f `  z )  =  c ) )
9088, 89imbi12d 321 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( a  =  ( f `  z )  ->  (
( ( [,] `  a
)  C_  ( [,] `  c )  ->  a  =  c )  <->  ( ( [,] `  ( f `  z ) )  C_  ( [,] `  c )  ->  ( f `  z )  =  c ) ) )
9190ralbidv 2864 . . . . . . . . . . . . . . . . . . . . . . . . 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 3229 . . . . . . . . . . . . . . . . . . . . . . . 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 465 . . . . . . . . . . . . . . . . . . . . . . 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 5878 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( c  =  ( f `  m )  ->  ( [,] `  c )  =  ( [,] `  (
f `  m )
) )
9594sseq2d 3492 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( c  =  ( f `  m )  ->  (
( [,] `  (
f `  z )
)  C_  ( [,] `  c )  <->  ( [,] `  ( f `  z
) )  C_  ( [,] `  ( f `  m ) ) ) )
96 eqeq2 2437 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( c  =  ( f `  m )  ->  (
( f `  z
)  =  c  <->  ( f `  z )  =  ( f `  m ) ) )
9795, 96imbi12d 321 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( c  =  ( f `  m )  ->  (
( ( [,] `  (
f `  z )
)  C_  ( [,] `  c )  ->  (
f `  z )  =  c )  <->  ( ( [,] `  ( f `  z ) )  C_  ( [,] `  ( f `
 m ) )  ->  ( f `  z )  =  ( f `  m ) ) ) )
9897rspcva 3180 . . . . . . . . . . . . . . . . . . . . . . 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 479 . . . . . . . . . . . . . . . . . . . . . 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 2431 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( f `  z )  =  ( f `  m )  <->  ( f `  m )  =  ( f `  z ) )
10199, 100syl6ib 229 . . . . . . . . . . . . . . . . . . . . 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 381 . . . . . . . . . . . . . . . . . . . 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 479 . . . . . . . . . . . . . . . . . . 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 837 . . . . . . . . . . . . . . . . . 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 473 . . . . . . . . . . . . . . . . 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 5827 . . . . . . . . . . . . . . . . . 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 6173 . . . . . . . . . . . . . . . . . 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 473 . . . . . . . . . . . . . . . . 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 45 . . . . . . . . . . . . . . . 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 847 . . . . . . . . . . . . . . 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 2846 . . . . . . . . . . . . 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 2426 . . . . . . . . . . . . . . . . 17  |-  ( m  =  z  ->  (
m  =  p  <->  z  =  p ) )
114 fveq2 5878 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  =  z  ->  (
f `  m )  =  ( f `  z ) )
115114fveq2d 5882 . . . . . . . . . . . . . . . . . . 19  |-  ( m  =  z  ->  ( (,) `  ( f `  m ) )  =  ( (,) `  (
f `  z )
) )
116115ineq1d 3663 . . . . . . . . . . . . . . . . . 18  |-  ( m  =  z  ->  (
( (,) `  (
f `  m )
)  i^i  ( (,) `  ( f `  p
) ) )  =  ( ( (,) `  (
f `  z )
)  i^i  ( (,) `  ( f `  p
) ) ) )
117116eqeq1d 2424 . . . . . . . . . . . . . . . . 17  |-  ( m  =  z  ->  (
( ( (,) `  (
f `  m )
)  i^i  ( (,) `  ( f `  p
) ) )  =  (/) 
<->  ( ( (,) `  (
f `  z )
)  i^i  ( (,) `  ( f `  p
) ) )  =  (/) ) )
118113, 117orbi12d 714 . . . . . . . . . . . . . . . 16  |-  ( m  =  z  ->  (
( m  =  p  \/  ( ( (,) `  ( f `  m
) )  i^i  ( (,) `  ( f `  p ) ) )  =  (/) )  <->  ( z  =  p  \/  (
( (,) `  (
f `  z )
)  i^i  ( (,) `  ( f `  p
) ) )  =  (/) ) ) )
119118ralbidv 2864 . . . . . . . . . . . . . . 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 3055 . . . . . . . . . . . . . 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 2437 . . . . . . . . . . . . . . . . 17  |-  ( z  =  p  ->  (
m  =  z  <->  m  =  p ) )
122 fveq2 5878 . . . . . . . . . . . . . . . . . . . 20  |-  ( z  =  p  ->  (
f `  z )  =  ( f `  p ) )
123122fveq2d 5882 . . . . . . . . . . . . . . . . . . 19  |-  ( z  =  p  ->  ( (,) `  ( f `  z ) )  =  ( (,) `  (
f `  p )
) )
124123ineq2d 3664 . . . . . . . . . . . . . . . . . 18  |-  ( z  =  p  ->  (
( (,) `  (
f `  m )
)  i^i  ( (,) `  ( f `  z
) ) )  =  ( ( (,) `  (
f `  m )
)  i^i  ( (,) `  ( f `  p
) ) ) )
125124eqeq1d 2424 . . . . . . . . . . . . . . . . 17  |-  ( z  =  p  ->  (
( ( (,) `  (
f `  m )
)  i^i  ( (,) `  ( f `  z
) ) )  =  (/) 
<->  ( ( (,) `  (
f `  m )
)  i^i  ( (,) `  ( f `  p
) ) )  =  (/) ) )
126121, 125orbi12d 714 . . . . . . . . . . . . . . . 16  |-  ( z  =  p  ->  (
( m  =  z  \/  ( ( (,) `  ( f `  m
) )  i^i  ( (,) `  ( f `  z ) ) )  =  (/) )  <->  ( m  =  p  \/  (
( (,) `  (
f `  m )
)  i^i  ( (,) `  ( f `  p
) ) )  =  (/) ) ) )
127126cbvralv 3055 . . . . . . . . . . . . . . 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 2856 . . . . . . . . . . . . . 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 4405 . . . . . . . . . . . . . 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 281 . . . . . . . . . . . . 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 215 . . . . . . . . . . . 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 2422 . . . . . . . . . . . 12  |-  seq 1
(  +  ,  ( ( abs  o.  -  )  o.  f )
)  =  seq 1
(  +  ,  ( ( abs  o.  -  )  o.  f )
)
13359, 131, 132uniiccvol 22524 . . . . . . . . . . 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 467 . . . . . . . . . 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 2465 . . . . . . . . 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 4445 . . . . . . . 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 13389 . . . . . . . . . . . 12  |-  abs : CC
--> RR
138 subf 9878 . . . . . . . . . . . 12  |-  -  :
( CC  X.  CC )
--> CC
139 fco 5753 . . . . . . . . . . . 12  |-  ( ( abs : CC --> RR  /\  -  : ( CC  X.  CC ) --> CC )  -> 
( abs  o.  -  ) : ( CC  X.  CC ) --> RR )
140137, 138, 139mp2an 676 . . . . . . . . . . 11  |-  ( abs 
o.  -  ) :
( CC  X.  CC )
--> RR
141 zre 10942 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  ZZ  ->  x  e.  RR )
142 2re 10680 . . . . . . . . . . . . . . . . . . . . 21  |-  2  e.  RR
143 reexpcl 12289 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 2  e.  RR  /\  y  e.  NN0 )  -> 
( 2 ^ y
)  e.  RR )
144142, 143mpan 674 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  NN0  ->  ( 2 ^ y )  e.  RR )
145 nn0z 10961 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  NN0  ->  y  e.  ZZ )
146 2cn 10681 . . . . . . . . . . . . . . . . . . . . . 22  |-  2  e.  CC
147 2ne0 10703 . . . . . . . . . . . . . . . . . . . . . 22  |-  2  =/=  0
148 expne0i 12304 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( 2  e.  CC  /\  2  =/=  0  /\  y  e.  ZZ )  ->  (
2 ^ y )  =/=  0 )
149146, 147, 148mp3an12 1350 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  ZZ  ->  (
2 ^ y )  =/=  0 )
150145, 149syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  NN0  ->  ( 2 ^ y )  =/=  0 )
151144, 150jca 534 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  NN0  ->  ( ( 2 ^ y )  e.  RR  /\  (
2 ^ y )  =/=  0 ) )
152 redivcl 10327 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  e.  RR  /\  ( 2 ^ y
)  e.  RR  /\  ( 2 ^ y
)  =/=  0 )  ->  ( x  / 
( 2 ^ y
) )  e.  RR )
153 peano2re 9807 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  RR  ->  (
x  +  1 )  e.  RR )
154 redivcl 10327 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( x  +  1 )  e.  RR  /\  ( 2 ^ y
)  e.  RR  /\  ( 2 ^ y
)  =/=  0 )  ->  ( ( x  +  1 )  / 
( 2 ^ y
) )  e.  RR )
155153, 154syl3an1 1297 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  e.  RR  /\  ( 2 ^ y
)  e.  RR  /\  ( 2 ^ y
)  =/=  0 )  ->  ( ( x  +  1 )  / 
( 2 ^ y
) )  e.  RR )
156 opelxpi 4882 . . . . . . . . . . . . . . . . . . . . 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 665 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( x  e.  RR  /\  ( 2 ^ y
)  e.  RR  /\  ( 2 ^ y
)  =/=  0 )  ->  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>.  e.  ( RR  X.  RR ) )
1581573expb 1206 . . . . . . . . . . . . . . . . . . 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 479 . . . . . . . . . . . . . . . . . 18  |-  ( ( x  e.  ZZ  /\  y  e.  NN0 )  ->  <. ( x  /  (
2 ^ y ) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) ) >.  e.  ( RR  X.  RR ) )
160159rgen2 2850 . . . . . . . . . . . . . . . . 17  |-  A. x  e.  ZZ  A. y  e. 
NN0  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>.  e.  ( RR  X.  RR )
161 eqid 2422 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  ZZ ,  y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  =  ( x  e.