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

Theorem mblfinlem 26151
Description: Lemma for ismblfin 26154, 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.)
Assertion
Ref Expression
mblfinlem  |-  ( ( 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 mblfinlem
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 18756 . . . 4  |-  ( topGen ` 
ran  (,) )  e.  Top
2 0cld 17065 . . . 4  |-  ( (
topGen `  ran  (,) )  e.  Top  ->  (/)  e.  (
Clsd `  ( topGen ` 
ran  (,) ) ) )
31, 2ax-mp 8 . . 3  |-  (/)  e.  (
Clsd `  ( topGen ` 
ran  (,) ) )
4 simpl3 962 . . . . 5  |-  ( ( ( A  e.  (
topGen `  ran  (,) )  /\  M  e.  RR  /\  M  <  ( vol
* `  A )
)  /\  A  =  (/) )  ->  M  <  ( vol * `  A
) )
5 fveq2 5695 . . . . . 6  |-  ( A  =  (/)  ->  ( vol
* `  A )  =  ( vol * `  (/) ) )
65adantl 453 . . . . 5  |-  ( ( ( A  e.  (
topGen `  ran  (,) )  /\  M  e.  RR  /\  M  <  ( vol
* `  A )
)  /\  A  =  (/) )  ->  ( vol * `
 A )  =  ( vol * `  (/) ) )
74, 6breqtrd 4204 . . . 4  |-  ( ( ( A  e.  (
topGen `  ran  (,) )  /\  M  e.  RR  /\  M  <  ( vol
* `  A )
)  /\  A  =  (/) )  ->  M  <  ( vol * `  (/) ) )
8 0ss 3624 . . . 4  |-  (/)  C_  A
97, 8jctil 524 . . 3  |-  ( ( ( A  e.  (
topGen `  ran  (,) )  /\  M  e.  RR  /\  M  <  ( vol
* `  A )
)  /\  A  =  (/) )  ->  ( (/)  C_  A  /\  M  <  ( vol
* `  (/) ) ) )
10 sseq1 3337 . . . . 5  |-  ( s  =  (/)  ->  ( s 
C_  A  <->  (/)  C_  A
) )
11 fveq2 5695 . . . . . 6  |-  ( s  =  (/)  ->  ( vol
* `  s )  =  ( vol * `  (/) ) )
1211breq2d 4192 . . . . 5  |-  ( s  =  (/)  ->  ( M  <  ( vol * `  s )  <->  M  <  ( vol * `  (/) ) ) )
1310, 12anbi12d 692 . . . 4  |-  ( s  =  (/)  ->  ( ( s  C_  A  /\  M  <  ( vol * `  s ) )  <->  ( (/)  C_  A  /\  M  <  ( vol
* `  (/) ) ) ) )
1413rspcev 3020 . . 3  |-  ( (
(/)  e.  ( Clsd `  ( topGen `  ran  (,) )
)  /\  ( (/)  C_  A  /\  M  <  ( vol
* `  (/) ) ) )  ->  E. s  e.  ( Clsd `  ( topGen `
 ran  (,) )
) ( s  C_  A  /\  M  <  ( vol * `  s ) ) )
153, 9, 14sylancr 645 . 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 peano2re 9203 . . . . . . . . . . . . . . . 16  |-  ( n  e.  RR  ->  (
n  +  1 )  e.  RR )
17 ltp1 9812 . . . . . . . . . . . . . . . 16  |-  ( n  e.  RR  ->  n  <  ( n  +  1 ) )
18 breq2 4184 . . . . . . . . . . . . . . . . 17  |-  ( z  =  ( n  + 
1 )  ->  (
n  <  z  <->  n  <  ( n  +  1 ) ) )
1918rspcev 3020 . . . . . . . . . . . . . . . 16  |-  ( ( ( n  +  1 )  e.  RR  /\  n  <  ( n  + 
1 ) )  ->  E. z  e.  RR  n  <  z )
2016, 17, 19syl2anc 643 . . . . . . . . . . . . . . 15  |-  ( n  e.  RR  ->  E. z  e.  RR  n  <  z
)
2120rgen 2739 . . . . . . . . . . . . . 14  |-  A. n  e.  RR  E. z  e.  RR  n  <  z
22 ltnle 9119 . . . . . . . . . . . . . . . . . 18  |-  ( ( n  e.  RR  /\  z  e.  RR )  ->  ( n  <  z  <->  -.  z  <_  n )
)
2322rexbidva 2691 . . . . . . . . . . . . . . . . 17  |-  ( n  e.  RR  ->  ( E. z  e.  RR  n  <  z  <->  E. z  e.  RR  -.  z  <_  n ) )
24 rexnal 2685 . . . . . . . . . . . . . . . . 17  |-  ( E. z  e.  RR  -.  z  <_  n  <->  -.  A. z  e.  RR  z  <_  n
)
2523, 24syl6bb 253 . . . . . . . . . . . . . . . 16  |-  ( n  e.  RR  ->  ( E. z  e.  RR  n  <  z  <->  -.  A. z  e.  RR  z  <_  n
) )
2625ralbiia 2706 . . . . . . . . . . . . . . 15  |-  ( A. n  e.  RR  E. z  e.  RR  n  <  z  <->  A. n  e.  RR  -.  A. z  e.  RR  z  <_  n )
27 ralnex 2684 . . . . . . . . . . . . . . 15  |-  ( A. n  e.  RR  -.  A. z  e.  RR  z  <_  n  <->  -.  E. n  e.  RR  A. z  e.  RR  z  <_  n
)
2826, 27bitri 241 . . . . . . . . . . . . . 14  |-  ( A. n  e.  RR  E. z  e.  RR  n  <  z  <->  -. 
E. n  e.  RR  A. z  e.  RR  z  <_  n )
2921, 28mpbi 200 . . . . . . . . . . . . 13  |-  -.  E. n  e.  RR  A. z  e.  RR  z  <_  n
30 raleq 2872 . . . . . . . . . . . . . 14  |-  ( A  =  RR  ->  ( A. z  e.  A  z  <_  n  <->  A. z  e.  RR  z  <_  n
) )
3130rexbidv 2695 . . . . . . . . . . . . 13  |-  ( A  =  RR  ->  ( E. n  e.  RR  A. z  e.  A  z  <_  n  <->  E. n  e.  RR  A. z  e.  RR  z  <_  n
) )
3229, 31mtbiri 295 . . . . . . . . . . . 12  |-  ( A  =  RR  ->  -.  E. n  e.  RR  A. z  e.  A  z  <_  n )
33 ssrab2 3396 . . . . . . . . . . . . . . . . 17  |-  { 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 }
34 ssrab2 3396 . . . . . . . . . . . . . . . . . 18  |-  { 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 ) )
>. )
35 zre 10250 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  ZZ  ->  x  e.  RR )
36 2re 10033 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  2  e.  RR
37 reexpcl 11361 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( 2  e.  RR  /\  y  e.  NN0 )  -> 
( 2 ^ y
)  e.  RR )
3836, 37mpan 652 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  e.  NN0  ->  ( 2 ^ y )  e.  RR )
39 nn0z 10268 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  e.  NN0  ->  y  e.  ZZ )
40 2cn 10034 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  2  e.  CC
41 2ne0 10047 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  2  =/=  0
42 expne0i 11375 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( 2  e.  CC  /\  2  =/=  0  /\  y  e.  ZZ )  ->  (
2 ^ y )  =/=  0 )
4340, 41, 42mp3an12 1269 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  e.  ZZ  ->  (
2 ^ y )  =/=  0 )
4439, 43syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  e.  NN0  ->  ( 2 ^ y )  =/=  0 )
4538, 44jca 519 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  e.  NN0  ->  ( ( 2 ^ y )  e.  RR  /\  (
2 ^ y )  =/=  0 ) )
46 redivcl 9697 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( x  e.  RR  /\  ( 2 ^ y
)  e.  RR  /\  ( 2 ^ y
)  =/=  0 )  ->  ( x  / 
( 2 ^ y
) )  e.  RR )
47 peano2re 9203 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  e.  RR  ->  (
x  +  1 )  e.  RR )
48 redivcl 9697 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( x  +  1 )  e.  RR  /\  ( 2 ^ y
)  e.  RR  /\  ( 2 ^ y
)  =/=  0 )  ->  ( ( x  +  1 )  / 
( 2 ^ y
) )  e.  RR )
4947, 48syl3an1 1217 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( x  e.  RR  /\  ( 2 ^ y
)  e.  RR  /\  ( 2 ^ y
)  =/=  0 )  ->  ( ( x  +  1 )  / 
( 2 ^ y
) )  e.  RR )
50 opelxpi 4877 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( x  /  (
2 ^ y ) )  e.  RR  /\  ( ( x  + 
1 )  /  (
2 ^ y ) )  e.  RR )  ->  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>.  e.  ( RR  X.  RR ) )
5146, 49, 50syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( x  e.  RR  /\  ( 2 ^ y
)  e.  RR  /\  ( 2 ^ y
)  =/=  0 )  ->  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>.  e.  ( RR  X.  RR ) )
52513expb 1154 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( x  e.  RR  /\  ( ( 2 ^ y )  e.  RR  /\  ( 2 ^ y
)  =/=  0 ) )  ->  <. ( x  /  ( 2 ^ y ) ) ,  ( ( x  + 
1 )  /  (
2 ^ y ) ) >.  e.  ( RR  X.  RR ) )
5335, 45, 52syl2an 464 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  e.  ZZ  /\  y  e.  NN0 )  ->  <. ( x  /  (
2 ^ y ) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) ) >.  e.  ( RR  X.  RR ) )
5453rgen2 2770 . . . . . . . . . . . . . . . . . . . 20  |-  A. x  e.  ZZ  A. y  e. 
NN0  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>.  e.  ( RR  X.  RR )
55 eqid 2412 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  e.  ZZ ,  y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  =  ( x  e.  ZZ ,  y  e. 
NN0  |->  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>. )
5655fmpt2 6385 . . . . . . . . . . . . . . . . . . . 20  |-  ( A. x  e.  ZZ  A. y  e.  NN0  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>.  e.  ( RR  X.  RR )  <->  ( x  e.  ZZ ,  y  e. 
NN0  |->  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>. ) : ( ZZ 
X.  NN0 ) --> ( RR 
X.  RR ) )
5754, 56mpbi 200 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  ZZ ,  y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. ) : ( ZZ  X.  NN0 ) --> ( RR  X.  RR )
58 frn 5564 . . . . . . . . . . . . . . . . . . 19  |-  ( ( x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. ) : ( ZZ  X.  NN0 ) --> ( RR  X.  RR )  ->  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  C_  ( RR  X.  RR ) )
5957, 58ax-mp 8 . . . . . . . . . . . . . . . . . 18  |-  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  C_  ( RR  X.  RR )
6034, 59sstri 3325 . . . . . . . . . . . . . . . . 17  |-  { b  e.  ran  ( x  e.  ZZ ,  y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A }  C_  ( RR  X.  RR )
6133, 60sstri 3325 . . . . . . . . . . . . . . . 16  |-  { 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_  ( RR  X.  RR )
62 rnss 5065 . . . . . . . . . . . . . . . . 17  |-  ( { 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_  ( RR  X.  RR )  ->  ran  {
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  ( RR  X.  RR ) )
63 rnxpid 5269 . . . . . . . . . . . . . . . . 17  |-  ran  ( RR  X.  RR )  =  RR
6462, 63syl6sseq 3362 . . . . . . . . . . . . . . . 16  |-  ( { 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_  ( RR  X.  RR )  ->  ran  {
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_  RR )
6561, 64ax-mp 8 . . . . . . . . . . . . . . 15  |-  ran  {
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_  RR
66 rnfi 7358 . . . . . . . . . . . . . . 15  |-  ( { 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 ) }  e.  Fin  ->  ran  { 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 ) }  e.  Fin )
67 fimaxre2 9920 . . . . . . . . . . . . . . 15  |-  ( ( ran  { 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_  RR  /\  ran  { 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 ) }  e.  Fin )  ->  E. n  e.  RR  A. u  e.  ran  {
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  <_  n )
6865, 66, 67sylancr 645 . . . . . . . . . . . . . 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 ) }  e.  Fin  ->  E. n  e.  RR  A. u  e. 
ran  { 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  <_  n )
6968adantl 453 . . . . . . . . . . . . 13  |-  ( ( 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 ) } )  =  A  /\  { 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 ) }  e.  Fin )  ->  E. n  e.  RR  A. u  e.  ran  {
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  <_  n )
70 eluni2 3987 . . . . . . . . . . . . . . . . . . . 20  |-  ( z  e.  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 ) } )  <->  E. u  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 ) } ) z  e.  u )
71 iccf 10967 . . . . . . . . . . . . . . . . . . . . . 22  |-  [,] :
( RR*  X.  RR* ) --> ~P RR*
72 ffn 5558 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( [,]
: ( RR*  X.  RR* )
--> ~P RR*  ->  [,]  Fn  ( RR*  X.  RR* )
)
7371, 72ax-mp 8 . . . . . . . . . . . . . . . . . . . . 21  |-  [,]  Fn  ( RR*  X.  RR* )
74 ressxr 9093 . . . . . . . . . . . . . . . . . . . . . . 23  |-  RR  C_  RR*
75 xpss12 4948 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( RR  C_  RR*  /\  RR  C_ 
RR* )  ->  ( RR  X.  RR )  C_  ( RR*  X.  RR* )
)
7674, 74, 75mp2an 654 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( RR 
X.  RR )  C_  ( RR*  X.  RR* )
7761, 76sstri 3325 . . . . . . . . . . . . . . . . . . . . 21  |-  { 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_  ( RR*  X.  RR* )
78 eleq2 2473 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( u  =  ( [,] `  v
)  ->  ( z  e.  u  <->  z  e.  ( [,] `  v ) ) )
7978rexima 5944 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( [,]  Fn  ( RR*  X. 
RR* )  /\  {
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_  ( RR*  X.  RR* ) )  ->  ( E. u  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 ) } ) z  e.  u  <->  E. v  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 ) } z  e.  ( [,] `  v ) ) )
8073, 77, 79mp2an 654 . . . . . . . . . . . . . . . . . . . 20  |-  ( E. u  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 ) } ) z  e.  u  <->  E. v  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 ) } z  e.  ( [,] `  v
) )
8170, 80bitri 241 . . . . . . . . . . . . . . . . . . 19  |-  ( z  e.  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 ) } )  <->  E. v  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 ) } z  e.  ( [,] `  v ) )
8261sseli 3312 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( v  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 ) }  ->  v  e.  ( RR  X.  RR ) )
83 1st2nd2 6353 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( v  e.  ( RR  X.  RR )  ->  v  = 
<. ( 1st `  v
) ,  ( 2nd `  v ) >. )
8483fveq2d 5699 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( v  e.  ( RR  X.  RR )  ->  ( [,] `  v )  =  ( [,] `  <. ( 1st `  v ) ,  ( 2nd `  v
) >. ) )
85 df-ov 6051 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( 1st `  v ) [,] ( 2nd `  v
) )  =  ( [,] `  <. ( 1st `  v ) ,  ( 2nd `  v
) >. )
8684, 85syl6eqr 2462 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( v  e.  ( RR  X.  RR )  ->  ( [,] `  v )  =  ( ( 1st `  v
) [,] ( 2nd `  v ) ) )
8786eleq2d 2479 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( v  e.  ( RR  X.  RR )  ->  ( z  e.  ( [,] `  v
)  <->  z  e.  ( ( 1st `  v
) [,] ( 2nd `  v ) ) ) )
8882, 87syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( v  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 ) }  ->  ( z  e.  ( [,] `  v
)  <->  z  e.  ( ( 1st `  v
) [,] ( 2nd `  v ) ) ) )
8988biimpd 199 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( v  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 ) }  ->  ( z  e.  ( [,] `  v
)  ->  z  e.  ( ( 1st `  v
) [,] ( 2nd `  v ) ) ) )
9089imdistani 672 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( v  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 ) }  /\  z  e.  ( [,] `  v
) )  ->  (
v  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 ) }  /\  z  e.  ( ( 1st `  v
) [,] ( 2nd `  v ) ) ) )
91 iccssxr 10957 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( 1st `  v ) [,] ( 2nd `  v
) )  C_  RR*
9291sseli 3312 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( z  e.  ( ( 1st `  v ) [,] ( 2nd `  v ) )  ->  z  e.  RR* )
9392ad2antll 710 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( 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 ) } )  =  A  /\  n  e.  RR )  /\  A. u  e. 
ran  { 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  <_  n )  /\  ( v  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 ) }  /\  z  e.  ( ( 1st `  v
) [,] ( 2nd `  v ) ) ) )  ->  z  e.  RR* )
94 xp2nd 6344 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( v  e.  ( RR  X.  RR )  ->  ( 2nd `  v )  e.  RR )
9594rexrd 9098 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( v  e.  ( RR  X.  RR )  ->  ( 2nd `  v )  e.  RR* )
9682, 95syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( v  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 ) }  ->  ( 2nd `  v )  e.  RR* )
9796ad2antrl 709 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( 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 ) } )  =  A  /\  n  e.  RR )  /\  A. u  e. 
ran  { 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  <_  n )  /\  ( v  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 ) }  /\  z  e.  ( ( 1st `  v
) [,] ( 2nd `  v ) ) ) )  ->  ( 2nd `  v )  e.  RR* )
98 simpllr 736 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( 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 ) } )  =  A  /\  n  e.  RR )  /\  A. u  e. 
ran  { 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  <_  n )  /\  ( v  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 ) }  /\  z  e.  ( ( 1st `  v
) [,] ( 2nd `  v ) ) ) )  ->  n  e.  RR )
9998rexrd 9098 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( 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 ) } )  =  A  /\  n  e.  RR )  /\  A. u  e. 
ran  { 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  <_  n )  /\  ( v  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 ) }  /\  z  e.  ( ( 1st `  v
) [,] ( 2nd `  v ) ) ) )  ->  n  e.  RR* )
100 xp1st 6343 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( v  e.  ( RR  X.  RR )  ->  ( 1st `  v )  e.  RR )
101100rexrd 9098 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( v  e.  ( RR  X.  RR )  ->  ( 1st `  v )  e.  RR* )
102101, 95jca 519 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( v  e.  ( RR  X.  RR )  ->  ( ( 1st `  v )  e.  RR*  /\  ( 2nd `  v )  e. 
RR* ) )
10382, 102syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( v  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 ) }  ->  ( ( 1st `  v )  e. 
RR*  /\  ( 2nd `  v )  e.  RR* ) )
104 iccleub 10931 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( 1st `  v
)  e.  RR*  /\  ( 2nd `  v )  e. 
RR*  /\  z  e.  ( ( 1st `  v
) [,] ( 2nd `  v ) ) )  ->  z  <_  ( 2nd `  v ) )
1051043expa 1153 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( 1st `  v
)  e.  RR*  /\  ( 2nd `  v )  e. 
RR* )  /\  z  e.  ( ( 1st `  v
) [,] ( 2nd `  v ) ) )  ->  z  <_  ( 2nd `  v ) )
106103, 105sylan 458 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( v  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 ) }  /\  z  e.  ( ( 1st `  v
) [,] ( 2nd `  v ) ) )  ->  z  <_  ( 2nd `  v ) )
107106adantl 453 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( 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 ) } )  =  A  /\  n  e.  RR )  /\  A. u  e. 
ran  { 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  <_  n )  /\  ( v  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 ) }  /\  z  e.  ( ( 1st `  v
) [,] ( 2nd `  v ) ) ) )  ->  z  <_  ( 2nd `  v ) )
108 xpss 4949 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( RR 
X.  RR )  C_  ( _V  X.  _V )
10961, 108sstri 3325 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  { 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_  ( _V  X.  _V )
110 df-rel 4852 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( Rel 
{ 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_  ( _V  X.  _V ) )
111109, 110mpbir 201 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  Rel  {
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 ) }
112 2ndrn 6362 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( Rel  { 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 ) }  /\  v  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 ) } )  ->  ( 2nd `  v )  e.  ran  { 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 ) } )
113111, 112mpan 652 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( v  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 ) }  ->  ( 2nd `  v )  e.  ran  { 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 ) } )
114 breq1 4183 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( u  =  ( 2nd `  v
)  ->  ( u  <_  n  <->  ( 2nd `  v
)  <_  n )
)
115114rspccva 3019 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( A. u  e.  ran  { 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  <_  n  /\  ( 2nd `  v )  e.  ran  { 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 ) } )  -> 
( 2nd `  v
)  <_  n )
116113, 115sylan2 461 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( A. u  e.  ran  { 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  <_  n  /\  v  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 ) } )  ->  ( 2nd `  v )  <_  n )
117116ad2ant2lr 729 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( 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 ) } )  =  A  /\  n  e.  RR )  /\  A. u  e. 
ran  { 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  <_  n )  /\  ( v  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 ) }  /\  z  e.  ( ( 1st `  v
) [,] ( 2nd `  v ) ) ) )  ->  ( 2nd `  v )  <_  n
)
11893, 97, 99, 107, 117xrletrd 10716 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( 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 ) } )  =  A  /\  n  e.  RR )  /\  A. u  e. 
ran  { 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  <_  n )  /\  ( v  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 ) }  /\  z  e.  ( ( 1st `  v
) [,] ( 2nd `  v ) ) ) )  ->  z  <_  n )
11990, 118sylan2 461 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( 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 ) } )  =  A  /\  n  e.  RR )  /\  A. u  e. 
ran  { 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  <_  n )  /\  ( v  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 ) }  /\  z  e.  ( [,] `  v ) ) )  ->  z  <_  n )
120119rexlimdvaa 2799 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( 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 ) } )  =  A  /\  n  e.  RR )  /\  A. u  e.  ran  { 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  <_  n )  ->  ( E. v  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 ) } z  e.  ( [,] `  v )  ->  z  <_  n ) )
12181, 120syl5bi 209 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 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 ) } )  =  A  /\  n  e.  RR )  /\  A. u  e.  ran  { 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  <_  n )  ->  ( z  e.  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 ) } )  -> 
z  <_  n )
)
122121ralrimiv 2756 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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 ) } )  =  A  /\  n  e.  RR )  /\  A. u  e.  ran  { 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  <_  n )  ->  A. z  e.  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 ) } ) z  <_  n )
123 raleq 2872 . . . . . . . . . . . . . . . . . 18  |-  ( 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 ) } )  =  A  ->  ( A. z  e.  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 ) } ) z  <_  n 
<-> 
A. z  e.  A  z  <_  n ) )
124123ad2antrr 707 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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 ) } )  =  A  /\  n  e.  RR )  /\  A. u  e.  ran  { 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  <_  n )  ->  ( A. z  e. 
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 ) } ) z  <_  n  <->  A. z  e.  A  z  <_  n ) )
125122, 124mpbid 202 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 ) } )  =  A  /\  n  e.  RR )  /\  A. u  e.  ran  { 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  <_  n )  ->  A. z  e.  A  z  <_  n )
126125ex 424 . . . . . . . . . . . . . . 15  |-  ( ( 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 ) } )  =  A  /\  n  e.  RR )  ->  ( A. u  e. 
ran  { 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  <_  n  ->  A. z  e.  A  z  <_  n ) )
127126reximdva 2786 . . . . . . . . . . . . . 14  |-  ( 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 ) } )  =  A  ->  ( E. n  e.  RR  A. u  e.  ran  { 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  <_  n  ->  E. n  e.  RR  A. z  e.  A  z  <_  n ) )
128127adantr 452 . . . . . . . . . . . . 13  |-  ( ( 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 ) } )  =  A  /\  { 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 ) }  e.  Fin )  -> 
( E. n  e.  RR  A. u  e. 
ran  { 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  <_  n  ->  E. n  e.  RR  A. z  e.  A  z  <_  n ) )
12969, 128mpd 15 . . . . . . . . . . . 12  |-  ( ( 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 ) } )  =  A  /\  { 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 ) }  e.  Fin )  ->  E. n  e.  RR  A. z  e.  A  z  <_  n )
13032, 129nsyl 115 . . . . . . . . . . 11  |-  ( A  =  RR  ->  -.  ( 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 ) } )  =  A  /\  { 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 ) }  e.  Fin ) )
131130adantl 453 . . . . . . . . . 10  |-  ( ( ( A  e.  (
topGen `  ran  (,) )  /\  A  =/=  (/) )  /\  A  =  RR )  ->  -.  ( 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 ) } )  =  A  /\  { 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 ) }  e.  Fin )
)
132 uniretop 18757 . . . . . . . . . . . . . 14  |-  RR  =  U. ( topGen `  ran  (,) )
133 retopcon 18821 . . . . . . . . . . . . . . 15  |-  ( topGen ` 
ran  (,) )  e.  Con
134133a1i 11 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
topGen `  ran  (,) )  /\  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 ) } )  =  A  /\  { 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 ) }  e.  Fin ) )  ->  ( topGen `  ran  (,) )  e.  Con )
135 simpll 731 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
topGen `  ran  (,) )  /\  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 ) } )  =  A  /\  { 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 ) }  e.  Fin ) )  ->  A  e.  (
topGen `  ran  (,) )
)
136 simplr 732 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  (
topGen `  ran  (,) )  /\  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 ) } )  =  A  /\  { 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 ) }  e.  Fin ) )  ->  A  =/=  (/) )
137 simprl 733 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  (
topGen `  ran  (,) )  /\  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