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

Theorem mblfinlem1 32022
Description: Lemma for ismblfin 32026, 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 9832 . . . . . . . . . . . . 13  |-  ( n  e.  RR  ->  (
n  +  1 )  e.  RR )
2 ltp1 10471 . . . . . . . . . . . . 13  |-  ( n  e.  RR  ->  n  <  ( n  +  1 ) )
3 breq2 4420 . . . . . . . . . . . . . 14  |-  ( z  =  ( n  + 
1 )  ->  (
n  <  z  <->  n  <  ( n  +  1 ) ) )
43rspcev 3162 . . . . . . . . . . . . 13  |-  ( ( ( n  +  1 )  e.  RR  /\  n  <  ( n  + 
1 ) )  ->  E. z  e.  RR  n  <  z )
51, 2, 4syl2anc 671 . . . . . . . . . . . 12  |-  ( n  e.  RR  ->  E. z  e.  RR  n  <  z
)
65rgen 2759 . . . . . . . . . . 11  |-  A. n  e.  RR  E. z  e.  RR  n  <  z
7 ltnle 9739 . . . . . . . . . . . . . . 15  |-  ( ( n  e.  RR  /\  z  e.  RR )  ->  ( n  <  z  <->  -.  z  <_  n )
)
87rexbidva 2910 . . . . . . . . . . . . . 14  |-  ( n  e.  RR  ->  ( E. z  e.  RR  n  <  z  <->  E. z  e.  RR  -.  z  <_  n ) )
9 rexnal 2848 . . . . . . . . . . . . . 14  |-  ( E. z  e.  RR  -.  z  <_  n  <->  -.  A. z  e.  RR  z  <_  n
)
108, 9syl6bb 269 . . . . . . . . . . . . 13  |-  ( n  e.  RR  ->  ( E. z  e.  RR  n  <  z  <->  -.  A. z  e.  RR  z  <_  n
) )
1110ralbiia 2830 . . . . . . . . . . . 12  |-  ( A. n  e.  RR  E. z  e.  RR  n  <  z  <->  A. n  e.  RR  -.  A. z  e.  RR  z  <_  n )
12 ralnex 2846 . . . . . . . . . . . 12  |-  ( A. n  e.  RR  -.  A. z  e.  RR  z  <_  n  <->  -.  E. n  e.  RR  A. z  e.  RR  z  <_  n
)
1311, 12bitri 257 . . . . . . . . . . 11  |-  ( A. n  e.  RR  E. z  e.  RR  n  <  z  <->  -. 
E. n  e.  RR  A. z  e.  RR  z  <_  n )
146, 13mpbi 213 . . . . . . . . . 10  |-  -.  E. n  e.  RR  A. z  e.  RR  z  <_  n
15 raleq 2999 . . . . . . . . . . 11  |-  ( A  =  RR  ->  ( A. z  e.  A  z  <_  n  <->  A. z  e.  RR  z  <_  n
) )
1615rexbidv 2913 . . . . . . . . . 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 309 . . . . . . . . 9  |-  ( A  =  RR  ->  -.  E. n  e.  RR  A. z  e.  A  z  <_  n )
18 ssrab2 3526 . . . . . . . . . . . . . 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 3526 . . . . . . . . . . . . . . 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 10970 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  ZZ  ->  x  e.  RR )
21 2re 10707 . . . . . . . . . . . . . . . . . . . . 21  |-  2  e.  RR
22 reexpcl 12321 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 2  e.  RR  /\  y  e.  NN0 )  -> 
( 2 ^ y
)  e.  RR )
2321, 22mpan 681 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  NN0  ->  ( 2 ^ y )  e.  RR )
24 nn0z 10989 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  NN0  ->  y  e.  ZZ )
25 2cn 10708 . . . . . . . . . . . . . . . . . . . . . 22  |-  2  e.  CC
26 2ne0 10730 . . . . . . . . . . . . . . . . . . . . . 22  |-  2  =/=  0
27 expne0i 12336 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( 2  e.  CC  /\  2  =/=  0  /\  y  e.  ZZ )  ->  (
2 ^ y )  =/=  0 )
2825, 26, 27mp3an12 1363 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  ZZ  ->  (
2 ^ y )  =/=  0 )
2924, 28syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  NN0  ->  ( 2 ^ y )  =/=  0 )
3023, 29jca 539 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  NN0  ->  ( ( 2 ^ y )  e.  RR  /\  (
2 ^ y )  =/=  0 ) )
31 redivcl 10354 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  e.  RR  /\  ( 2 ^ y
)  e.  RR  /\  ( 2 ^ y
)  =/=  0 )  ->  ( x  / 
( 2 ^ y
) )  e.  RR )
32 peano2re 9832 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  e.  RR  ->  (
x  +  1 )  e.  RR )
33 redivcl 10354 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( x  +  1 )  e.  RR  /\  ( 2 ^ y
)  e.  RR  /\  ( 2 ^ y
)  =/=  0 )  ->  ( ( x  +  1 )  / 
( 2 ^ y
) )  e.  RR )
3432, 33syl3an1 1309 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  e.  RR  /\  ( 2 ^ y
)  e.  RR  /\  ( 2 ^ y
)  =/=  0 )  ->  ( ( x  +  1 )  / 
( 2 ^ y
) )  e.  RR )
35 opelxpi 4885 . . . . . . . . . . . . . . . . . . . . 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 671 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( x  e.  RR  /\  ( 2 ^ y
)  e.  RR  /\  ( 2 ^ y
)  =/=  0 )  ->  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>.  e.  ( RR  X.  RR ) )
37363expb 1216 . . . . . . . . . . . . . . . . . . 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 484 . . . . . . . . . . . . . . . . . 18  |-  ( ( x  e.  ZZ  /\  y  e.  NN0 )  ->  <. ( x  /  (
2 ^ y ) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) ) >.  e.  ( RR  X.  RR ) )
3938rgen2 2825 . . . . . . . . . . . . . . . . 17  |-  A. x  e.  ZZ  A. y  e. 
NN0  <. ( x  / 
( 2 ^ y
) ) ,  ( ( x  +  1 )  /  ( 2 ^ y ) )
>.  e.  ( RR  X.  RR )
40 eqid 2462 . . . . . . . . . . . . . . . . . 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 6887 . . . . . . . . . . . . . . . . 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 213 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ZZ ,  y  e.  NN0  |->  <. (
x  /  ( 2 ^ y ) ) ,  ( ( x  +  1 )  / 
( 2 ^ y
) ) >. ) : ( ZZ  X.  NN0 ) --> ( RR  X.  RR )
43 frn 5758 . . . . . . . . . . . . . . . 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 3453 . . . . . . . . . . . . . 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 3453 . . . . . . . . . . . . 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 5082 . . . . . . . . . . . . . 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 5289 . . . . . . . . . . . . . 14  |-  ran  ( RR  X.  RR )  =  RR
4947, 48syl6sseq 3490 . . . . . . . . . . . . 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 7883 . . . . . . . . . . . 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 10580 . . . . . . . . . . . 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 674 . . . . . . . . . . 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 472 . . . . . . . . . 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 4216 . . . . . . . . . . . . . . . . 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 11762 . . . . . . . . . . . . . . . . . . 19  |-  [,] :
( RR*  X.  RR* ) --> ~P RR*
57 ffn 5751 . . . . . . . . . . . . . . . . . . 19  |-  ( [,]
: ( RR*  X.  RR* )
--> ~P RR*  ->  [,]  Fn  ( RR*  X.  RR* )
)
5856, 57ax-mp 5 . . . . . . . . . . . . . . . . . 18  |-  [,]  Fn  ( RR*  X.  RR* )
59 rexpssxrxp 9711 . . . . . . . . . . . . . . . . . . 19  |-  ( RR 
X.  RR )  C_  ( RR*  X.  RR* )
6046, 59sstri 3453 . . . . . . . . . . . . . . . . . 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 2529 . . . . . . . . . . . . . . . . . . 19  |-  ( u  =  ( [,] `  v
)  ->  ( z  e.  u  <->  z  e.  ( [,] `  v ) ) )
6261rexima 6169 . . . . . . . . . . . . . . . . . 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 683 . . . . . . . . . . . . . . . . 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 257 . . . . . . . . . . . . . . . 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 3440 . . . . . . . . . . . . . . . . . . . . 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 6857 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( v  e.  ( RR  X.  RR )  ->  v  = 
<. ( 1st `  v
) ,  ( 2nd `  v ) >. )
6766fveq2d 5892 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( v  e.  ( RR  X.  RR )  ->  ( [,] `  v )  =  ( [,] `  <. ( 1st `  v ) ,  ( 2nd `  v
) >. ) )
68 df-ov 6318 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 1st `  v ) [,] ( 2nd `  v
) )  =  ( [,] `  <. ( 1st `  v ) ,  ( 2nd `  v
) >. )
6967, 68syl6eqr 2514 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( v  e.  ( RR  X.  RR )  ->  ( [,] `  v )  =  ( ( 1st `  v
) [,] ( 2nd `  v ) ) )
7069eleq2d 2525 . . . . . . . . . . . . . . . . . . . . 21  |-  ( v  e.  ( RR  X.  RR )  ->  ( z  e.  ( [,] `  v
)  <->  z  e.  ( ( 1st `  v
) [,] ( 2nd `  v ) ) ) )
7165, 70syl 17 . . . . . . . . . . . . . . . . . . . 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 212 . . . . . . . . . . . . . . . . . . 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 701 . . . . . . . . . . . . . . . . . 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 11746 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 1st `  v ) [,] ( 2nd `  v
) )  C_  RR*
7574sseli 3440 . . . . . . . . . . . . . . . . . . . 20  |-  ( z  e.  ( ( 1st `  v ) [,] ( 2nd `  v ) )  ->  z  e.  RR* )
7675ad2antll 740 . . . . . . . . . . . . . . . . . . 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 6851 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( v  e.  ( RR  X.  RR )  ->  ( 2nd `  v )  e.  RR )
7877rexrd 9716 . . . . . . . . . . . . . . . . . . . . 21  |-  ( v  e.  ( RR  X.  RR )  ->  ( 2nd `  v )  e.  RR* )
7965, 78syl 17 . . . . . . . . . . . . . . . . . . . 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 739 . . . . . . . . . . . . . . . . . . 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 774 . . . . . . . . . . . . . . . . . . . 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 9716 . . . . . . . . . . . . . . . . . . 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 6850 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( v  e.  ( RR  X.  RR )  ->  ( 1st `  v )  e.  RR )
8483rexrd 9716 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( v  e.  ( RR  X.  RR )  ->  ( 1st `  v )  e.  RR* )
8584, 78jca 539 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( v  e.  ( RR  X.  RR )  ->  ( ( 1st `  v )  e.  RR*  /\  ( 2nd `  v )  e. 
RR* ) )
8665, 85syl 17 . . . . . . . . . . . . . . . . . . . . 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 11719 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( 1st `  v
)  e.  RR*  /\  ( 2nd `  v )  e. 
RR*  /\  z  e.  ( ( 1st `  v
) [,] ( 2nd `  v ) ) )  ->  z  <_  ( 2nd `  v ) )
88873expa 1215 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( 1st `  v
)  e.  RR*  /\  ( 2nd `  v )  e. 
RR* )  /\  z  e.  ( ( 1st `  v
) [,] ( 2nd `  v ) ) )  ->  z  <_  ( 2nd `  v ) )
8986, 88sylan 478 . . . . . . . . . . . . . . . . . . . 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 472 . . . . . . . . . . . . . . . . . . 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 4960 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( RR 
X.  RR )  C_  ( _V  X.  _V )
9246, 91sstri 3453 . . . . . . . . . . . . . . . . . . . . . . 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 4860 . . . . . . . . . . . . . . . . . . . . . . 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 214 . . . . . . . . . . . . . . . . . . . . . 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 6868 . . . . . . . . . . . . . . . . . . . . . 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 681 . . . . . . . . . . . . . . . . . . . . 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 4419 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( u  =  ( 2nd `  v
)  ->  ( u  <_  n  <->  ( 2nd `  v
)  <_  n )
)
9897rspccva 3161 . . . . . . . . . . . . . . . . . . . . 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 481 . . . . . . . . . . . . . . . . . . . 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 759 . . . . . . . . . . . . . . . . . . 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 11488 . . . . . . . . . . . . . . . . . 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 481 . . . . . . . . . . . . . . . . 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 2892 . . . . . . . . . . . . . . . 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 225 . . . . . . . . . . . . . . 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 2812 . . . . . . . . . . . . . 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 2999 . . . . . . . . . . . . . . 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 737 . . . . . . . . . . . . . 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 215 . . . . . . . . . . . . 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 440 . . . . . . . . . . . 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 2874 . . . . . . . . . . 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 471 . . . . . . . . . 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 126 . . . . . . . 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 472 . . . . . . 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 21832 . . . . . . . . . . 11  |-  RR  =  U. ( topGen `  ran  (,) )
116 retopcon 21896 . . . . . . . . . . . 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 765 . . . . . . . . . . 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 767 . . . . . . . . . . 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 769 . . . . . . . . . . . 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 5754 . . . . . . . . . . . . . . 15  |-  ( [,]
: ( RR*  X.  RR* )
--> ~P RR*  ->  Fun  [,] )
122 funiunfv 6178 . . . . . . . . . . . . . . 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 ^ y ) ) >.
)  |