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

Theorem mblfinlem1 28371
Description: Lemma for ismblfin 28375, ordering the sets of dyadic intervals that are antichains under subset and whose unions are contained entirely in  A. (Contributed by Brendan Leahy, 13-Jul-2018.)
Assertion
Ref Expression
mblfinlem1  |-  ( ( 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 ) } )
Distinct variable group:    a, b, c, f, x, y, A

Proof of Theorem mblfinlem1
Dummy variables  n  u  v  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 peano2re 9534 . . . . . . . . . . . . 13  |-  ( n  e.  RR  ->  (
n  +  1 )  e.  RR )
2 ltp1 10159 . . . . . . . . . . . . 13  |-  ( n  e.  RR  ->  n  <  ( n  +  1 ) )
3 breq2 4289 . . . . . . . . . . . . . 14  |-  ( z  =  ( n  + 
1 )  ->  (
n  <  z  <->  n  <  ( n  +  1 ) ) )
43rspcev 3066 . . . . . . . . . . . . 13  |-  ( ( ( n  +  1 )  e.  RR  /\  n  <  ( n  + 
1 ) )  ->  E. z  e.  RR  n  <  z )
51, 2, 4syl2anc 661 . . . . . . . . . . . 12  |-  ( n  e.  RR  ->  E. z  e.  RR  n  <  z
)
65rgen 2775 . . . . . . . . . . 11  |-  A. n  e.  RR  E. z  e.  RR  n  <  z
7 ltnle 9446 . . . . . . . . . . . . . . 15  |-  ( ( n  e.  RR  /\  z  e.  RR )  ->  ( n  <  z  <->  -.  z  <_  n )
)
87rexbidva 2726 . . . . . . . . . . . . . 14  |-  ( n  e.  RR  ->  ( E. z  e.  RR  n  <  z  <->  E. z  e.  RR  -.  z  <_  n ) )
9 rexnal 2720 . . . . . . . . . . . . . 14  |-  ( E. z  e.  RR  -.  z  <_  n  <->  -.  A. z  e.  RR  z  <_  n
)
108, 9syl6bb 261 . . . . . . . . . . . . 13  |-  ( n  e.  RR  ->  ( E. z  e.  RR  n  <  z  <->  -.  A. z  e.  RR  z  <_  n
) )
1110ralbiia 2741 . . . . . . . . . . . 12  |-  ( A. n  e.  RR  E. z  e.  RR  n  <  z  <->  A. n  e.  RR  -.  A. z  e.  RR  z  <_  n )
12 ralnex 2719 . . . . . . . . . . . 12  |-  ( A. n  e.  RR  -.  A. z  e.  RR  z  <_  n  <->  -.  E. n  e.  RR  A. z  e.  RR  z  <_  n
)
1311, 12bitri 249 . . . . . . . . . . 11  |-  ( A. n  e.  RR  E. z  e.  RR  n  <  z  <->  -. 
E. n  e.  RR  A. z  e.  RR  z  <_  n )
146, 13mpbi 208 . . . . . . . . . 10  |-  -.  E. n  e.  RR  A. z  e.  RR  z  <_  n
15 raleq 2911 . . . . . . . . . . 11  |-  ( A  =  RR  ->  ( A. z  e.  A  z  <_  n  <->  A. z  e.  RR  z  <_  n
) )
1615rexbidv 2730 . . . . . . . . . 10  |-  ( A  =  RR  ->  ( E. n  e.  RR  A. z  e.  A  z  <_  n  <->  E. n  e.  RR  A. z  e.  RR  z  <_  n
) )
1714, 16mtbiri 303 . . . . . . . . 9  |-  ( A  =  RR  ->  -.  E. n  e.  RR  A. z  e.  A  z  <_  n )
18 ssrab2 3430 . . . . . . . . . . . . . 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 }
19 ssrab2 3430 . . . . . . . . . . . . . . 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 ) )
>. )
20 zre 10642 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  ZZ  ->  x  e.  RR )
21 2re 10383 . . . . . . . . . . . . . . . . . . . . 21  |-  2  e.  RR
22 reexpcl 11874 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 2  e.  RR  /\  y  e.  NN0 )  -> 
( 2 ^ y
)  e.  RR )
2321, 22mpan 670 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  NN0  ->  ( 2 ^ y )  e.  RR )
24 nn0z 10661 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  NN0  ->  y  e.  ZZ )
25 2cn 10384 . . . . . . . . . . . . . . . . . . . . . 22  |-  2  e.  CC
26 2ne0 10406 . . . . . . . . . . . . . . . . . . . . . 22  |-  2  =/=  0
27 expne0i 11888 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( 2  e.  CC  /\  2  =/=  0  /\  y  e.  ZZ )  ->  (
2 ^ y )  =/=  0 )
2825, 26, 27mp3an12 1304 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  ZZ  ->  (
2 ^ y )  =/=  0 )
2924, 28syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  NN0  ->  ( 2 ^ y )  =/=  0 )
3023, 29jca 532 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  NN0  ->  ( ( 2 ^ y )  e.  RR  /\  (
2 ^ y )  =/=  0 ) )
31 redivcl 10042 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  e.  RR  /\  ( 2 ^ y
)  e.  RR  /\  ( 2 ^ y
)  =/=  0 )  ->  ( x  / 
( 2 ^ y
) )  e.  RR )
32 peano2re 9534 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  RR  ->  (
x  +  1 )  e.  RR )
33 redivcl 10042 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( x  +  1 )  e.  RR  /\  ( 2 ^ y
)  e.  RR  /\  ( 2 ^ y
)  =/=  0 )  ->  ( ( x  +  1 )  / 
( 2 ^ y
) )  e.  RR )
3432, 33syl3an1 1251 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  e.  RR  /\  ( 2 ^ y
)  e.  RR  /\  ( 2 ^ y
)  =/=  0 )  ->  ( ( x  +  1 )  / 
( 2 ^ y
) )  e.  RR )
35 opelxpi 4863 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( x  /  (
2 ^ y ) )  e.  RR  /\  ( ( x  + 
1 )  /  (
2 ^ y ) )  e.  RR )  ->  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>.  e.  ( RR  X.  RR ) )
3631, 34, 35syl2anc 661 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( x  e.  RR  /\  ( 2 ^ y
)  e.  RR  /\  ( 2 ^ y
)  =/=  0 )  ->  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>.  e.  ( RR  X.  RR ) )
37363expb 1188 . . . . . . . . . . . . . . . . . . 19  |-  ( ( x  e.  RR  /\  ( ( 2 ^ y )  e.  RR  /\  ( 2 ^ y
)  =/=  0 ) )  ->  <. ( x  /  ( 2 ^ y ) ) ,  ( ( x  + 
1 )  /  (
2 ^ y ) ) >.  e.  ( RR  X.  RR ) )
3820, 30, 37syl2an 477 . . . . . . . . . . . . . . . . . 18  |-  ( ( x  e.  ZZ  /\  y  e.  NN0 )  ->  <. ( x  /  (
2 ^ y ) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) ) >.  e.  ( RR  X.  RR ) )
3938rgen2 2806 . . . . . . . . . . . . . . . . 17  |-  A. x  e.  ZZ  A. y  e. 
NN0  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>.  e.  ( RR  X.  RR )
40 eqid 2437 . . . . . . . . . . . . . . . . . 18  |-  ( 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 ) )
>. )
4140fmpt2 6636 . . . . . . . . . . . . . . . . 17  |-  ( 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 ) )
4239, 41mpbi 208 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ZZ ,  y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. ) : ( ZZ  X.  NN0 ) --> ( RR  X.  RR )
43 frn 5558 . . . . . . . . . . . . . . . 16  |-  ( ( 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 ) )
4442, 43ax-mp 5 . . . . . . . . . . . . . . 15  |-  ran  (
x  e.  ZZ , 
y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  C_  ( RR  X.  RR )
4519, 44sstri 3358 . . . . . . . . . . . . . 14  |-  { b  e.  ran  ( x  e.  ZZ ,  y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. )  |  ( [,] `  b
)  C_  A }  C_  ( RR  X.  RR )
4618, 45sstri 3358 . . . . . . . . . . . . 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_  ( RR  X.  RR )
47 rnss 5060 . . . . . . . . . . . . . 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_  ( 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 ) )
48 rnxpid 5264 . . . . . . . . . . . . . 14  |-  ran  ( RR  X.  RR )  =  RR
4947, 48syl6sseq 3395 . . . . . . . . . . . . 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_  ( 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 )
5046, 49ax-mp 5 . . . . . . . . . . . 12  |-  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
51 rnfi 7588 . . . . . . . . . . . 12  |-  ( { 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 )
52 fimaxre2 10270 . . . . . . . . . . . 12  |-  ( ( 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 )
5350, 51, 52sylancr 663 . . . . . . . . . . 11  |-  ( { 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 )
5453adantl 466 . . . . . . . . . 10  |-  ( ( 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 )
55 eluni2 4088 . . . . . . . . . . . . . . . . 17  |-  ( 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 )
56 iccf 11380 . . . . . . . . . . . . . . . . . . 19  |-  [,] :
( RR*  X.  RR* ) --> ~P RR*
57 ffn 5552 . . . . . . . . . . . . . . . . . . 19  |-  ( [,]
: ( RR*  X.  RR* )
--> ~P RR*  ->  [,]  Fn  ( RR*  X.  RR* )
)
5856, 57ax-mp 5 . . . . . . . . . . . . . . . . . 18  |-  [,]  Fn  ( RR*  X.  RR* )
59 rexpssxrxp 9420 . . . . . . . . . . . . . . . . . . 19  |-  ( RR 
X.  RR )  C_  ( RR*  X.  RR* )
6046, 59sstri 3358 . . . . . . . . . . . . . . . . . 18  |-  { 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* )
61 eleq2 2498 . . . . . . . . . . . . . . . . . . 19  |-  ( u  =  ( [,] `  v
)  ->  ( z  e.  u  <->  z  e.  ( [,] `  v ) ) )
6261rexima 5949 . . . . . . . . . . . . . . . . . 18  |-  ( ( [,]  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 ) ) )
6358, 60, 62mp2an 672 . . . . . . . . . . . . . . . . 17  |-  ( 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
) )
6455, 63bitri 249 . . . . . . . . . . . . . . . 16  |-  ( 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 ) )
6546sseli 3345 . . . . . . . . . . . . . . . . . . . . 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 ) }  ->  v  e.  ( RR  X.  RR ) )
66 1st2nd2 6608 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( v  e.  ( RR  X.  RR )  ->  v  = 
<. ( 1st `  v
) ,  ( 2nd `  v ) >. )
6766fveq2d 5688 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( v  e.  ( RR  X.  RR )  ->  ( [,] `  v )  =  ( [,] `  <. ( 1st `  v ) ,  ( 2nd `  v
) >. ) )
68 df-ov 6089 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 1st `  v ) [,] ( 2nd `  v
) )  =  ( [,] `  <. ( 1st `  v ) ,  ( 2nd `  v
) >. )
6967, 68syl6eqr 2487 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( v  e.  ( RR  X.  RR )  ->  ( [,] `  v )  =  ( ( 1st `  v
) [,] ( 2nd `  v ) ) )
7069eleq2d 2504 . . . . . . . . . . . . . . . . . . . . 21  |-  ( v  e.  ( RR  X.  RR )  ->  ( z  e.  ( [,] `  v
)  <->  z  e.  ( ( 1st `  v
) [,] ( 2nd `  v ) ) ) )
7165, 70syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( 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 ) ) ) )
7271biimpd 207 . . . . . . . . . . . . . . . . . . 19  |-  ( 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 ) ) ) )
7372imdistani 690 . . . . . . . . . . . . . . . . . 18  |-  ( ( 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 ) ) ) )
74 iccssxr 11370 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 1st `  v ) [,] ( 2nd `  v
) )  C_  RR*
7574sseli 3345 . . . . . . . . . . . . . . . . . . . 20  |-  ( z  e.  ( ( 1st `  v ) [,] ( 2nd `  v ) )  ->  z  e.  RR* )
7675ad2antll 728 . . . . . . . . . . . . . . . . . . 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 )  /\  ( 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* )
77 xp2nd 6602 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( v  e.  ( RR  X.  RR )  ->  ( 2nd `  v )  e.  RR )
7877rexrd 9425 . . . . . . . . . . . . . . . . . . . . 21  |-  ( v  e.  ( RR  X.  RR )  ->  ( 2nd `  v )  e.  RR* )
7965, 78syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( 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* )
8079ad2antrl 727 . . . . . . . . . . . . . . . . . . 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 )  /\  ( 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* )
81 simpllr 758 . . . . . . . . . . . . . . . . . . . 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.  ( ( 1st `  v
) [,] ( 2nd `  v ) ) ) )  ->  n  e.  RR )
8281rexrd 9425 . . . . . . . . . . . . . . . . . . 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 )  /\  ( 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* )
83 xp1st 6601 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( v  e.  ( RR  X.  RR )  ->  ( 1st `  v )  e.  RR )
8483rexrd 9425 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( v  e.  ( RR  X.  RR )  ->  ( 1st `  v )  e.  RR* )
8584, 78jca 532 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( v  e.  ( RR  X.  RR )  ->  ( ( 1st `  v )  e.  RR*  /\  ( 2nd `  v )  e. 
RR* ) )
8665, 85syl 16 . . . . . . . . . . . . . . . . . . . . 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 ) }  ->  ( ( 1st `  v )  e. 
RR*  /\  ( 2nd `  v )  e.  RR* ) )
87 iccleub 11343 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( 1st `  v
)  e.  RR*  /\  ( 2nd `  v )  e. 
RR*  /\  z  e.  ( ( 1st `  v
) [,] ( 2nd `  v ) ) )  ->  z  <_  ( 2nd `  v ) )
88873expa 1187 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( 1st `  v
)  e.  RR*  /\  ( 2nd `  v )  e. 
RR* )  /\  z  e.  ( ( 1st `  v
) [,] ( 2nd `  v ) ) )  ->  z  <_  ( 2nd `  v ) )
8986, 88sylan 471 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 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 ) )
9089adantl 466 . . . . . . . . . . . . . . . . . . 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 )  /\  ( 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 ) )
91 xpss 4938 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( RR 
X.  RR )  C_  ( _V  X.  _V )
9246, 91sstri 3358 . . . . . . . . . . . . . . . . . . . . . . 23  |-  { 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 )
93 df-rel 4839 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 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 ) )
9492, 93mpbir 209 . . . . . . . . . . . . . . . . . . . . . 22  |-  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 ) }
95 2ndrn 6617 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( 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 ) } )
9694, 95mpan 670 . . . . . . . . . . . . . . . . . . . . 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 ) }  ->  ( 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 ) } )
97 breq1 4288 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( u  =  ( 2nd `  v
)  ->  ( u  <_  n  <->  ( 2nd `  v
)  <_  n )
)
9897rspccva 3065 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 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 )
9996, 98sylan2 474 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 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 )
10099ad2ant2lr 747 . . . . . . . . . . . . . . . . . . 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 )  /\  ( 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
)
10176, 80, 82, 90, 100xrletrd 11128 . . . . . . . . . . . . . . . . . 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 )  /\  ( 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 )
10273, 101sylan2 474 . . . . . . . . . . . . . . . . 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 )  /\  ( 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 )
103102rexlimdvaa 2836 . . . . . . . . . . . . . . . 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 )  ->  ( 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 ) )
10464, 103syl5bi 217 . . . . . . . . . . . . . . 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 )  ->  ( 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 )
)
105104ralrimiv 2792 . . . . . . . . . . . . . 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  /\  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 )
106 raleq 2911 . . . . . . . . . . . . . . 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  ->  ( 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 ) )
107106ad2antrr 725 . . . . . . . . . . . . . 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  /\  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 ) )
108105, 107mpbid 210 . . . . . . . . . . . . 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  /\  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 )
109108ex 434 . . . . . . . . . . . 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  /\  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 ) )
110109reximdva 2822 . . . . . . . . . . 11  |-  ( 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 ) )
111110adantr 465 . . . . . . . . . 10  |-  ( ( 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 ) )
11254, 111mpd 15 . . . . . . . . 9  |-  ( ( 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 )
11317, 112nsyl 121 . . . . . . . 8  |-  ( 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 ) )
114113adantl 466 . . . . . . 7  |-  ( ( ( 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 )
)
115 uniretop 20310 . . . . . . . . . . 11  |-  RR  =  U. ( topGen `  ran  (,) )
116 retopcon 20375 . . . . . . . . . . . 12  |-  ( topGen ` 
ran  (,) )  e.  Con
117116a1i 11 . . . . . . . . . . 11  |-  ( ( ( 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 )
118 simpll 753 . . . . . . . . . . 11  |-  ( ( ( 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  (,) )
)
119 simplr 754 . . . . . . . . . . 11  |-  ( ( ( 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  =/=  (/) )
120 simprl 755 . . . . . . . . . . . 12  |-  ( ( ( 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 ) )  ->  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 )
121 ffun 5554 . . . . . . . . . . . . . . . 16  |-  ( [,]
: ( RR*  X.  RR* )
--> ~P RR*  ->  Fun  [,] )
12256, 121ax-mp 5 . . . . . . . . . . . . . . 15  |-  Fun  [,]
123 funiunfv 5958 . . . . . . . . . . . . . . 15  |-  ( Fun 
[,]  ->  U_ 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 ) }  ( [,] `  z
)  =  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