Metamath Proof Explorer

Theorem mblfinlem1

Description: Lemma for ismblfin , 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)

Ref Expression
Assertion 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 ) } )

Proof

Step Hyp Ref Expression
1 peano2re 
 |-  ( n e. RR -> ( n + 1 ) e. RR )
2 ltp1 
 |-  ( n e. RR -> n < ( n + 1 ) )
3 breq2 
 |-  ( z = ( n + 1 ) -> ( n < z <-> n < ( n + 1 ) ) )
4 3 rspcev 
 |-  ( ( ( n + 1 ) e. RR /\ n < ( n + 1 ) ) -> E. z e. RR n < z )
5 1 2 4 syl2anc 
 |-  ( n e. RR -> E. z e. RR n < z )
6 5 rgen 
 |-  A. n e. RR E. z e. RR n < z
7 ltnle 
 |-  ( ( n e. RR /\ z e. RR ) -> ( n < z <-> -. z <_ n ) )
8 7 rexbidva 
 |-  ( n e. RR -> ( E. z e. RR n < z <-> E. z e. RR -. z <_ n ) )
9 rexnal 
 |-  ( E. z e. RR -. z <_ n <-> -. A. z e. RR z <_ n )
10 8 9 bitrdi 
 |-  ( n e. RR -> ( E. z e. RR n < z <-> -. A. z e. RR z <_ n ) )
11 10 ralbiia 
 |-  ( A. n e. RR E. z e. RR n < z <-> A. n e. RR -. A. z e. RR z <_ n )
12 ralnex 
 |-  ( A. n e. RR -. A. z e. RR z <_ n <-> -. E. n e. RR A. z e. RR z <_ n )
13 11 12 bitri 
 |-  ( A. n e. RR E. z e. RR n < z <-> -. E. n e. RR A. z e. RR z <_ n )
14 6 13 mpbi 
 |-  -. E. n e. RR A. z e. RR z <_ n
15 raleq 
 |-  ( A = RR -> ( A. z e. A z <_ n <-> A. z e. RR z <_ n ) )
16 15 rexbidv 
 |-  ( A = RR -> ( E. n e. RR A. z e. A z <_ n <-> E. n e. RR A. z e. RR z <_ n ) )
17 14 16 mtbiri 
 |-  ( A = RR -> -. E. n e. RR A. z e. A z <_ n )
18 ssrab2 
 |-  { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { 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 
 |-  { 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 
 |-  ( x e. ZZ -> x e. RR )
21 2re 
 |-  2 e. RR
22 reexpcl 
 |-  ( ( 2 e. RR /\ y e. NN0 ) -> ( 2 ^ y ) e. RR )
23 21 22 mpan 
 |-  ( y e. NN0 -> ( 2 ^ y ) e. RR )
24 nn0z 
 |-  ( y e. NN0 -> y e. ZZ )
25 2cn 
 |-  2 e. CC
26 2ne0 
 |-  2 =/= 0
27 expne0i 
 |-  ( ( 2 e. CC /\ 2 =/= 0 /\ y e. ZZ ) -> ( 2 ^ y ) =/= 0 )
28 25 26 27 mp3an12 
 |-  ( y e. ZZ -> ( 2 ^ y ) =/= 0 )
29 24 28 syl 
 |-  ( y e. NN0 -> ( 2 ^ y ) =/= 0 )
30 23 29 jca 
 |-  ( y e. NN0 -> ( ( 2 ^ y ) e. RR /\ ( 2 ^ y ) =/= 0 ) )
31 redivcl 
 |-  ( ( x e. RR /\ ( 2 ^ y ) e. RR /\ ( 2 ^ y ) =/= 0 ) -> ( x / ( 2 ^ y ) ) e. RR )
32 peano2re 
 |-  ( x e. RR -> ( x + 1 ) e. RR )
33 redivcl 
 |-  ( ( ( x + 1 ) e. RR /\ ( 2 ^ y ) e. RR /\ ( 2 ^ y ) =/= 0 ) -> ( ( x + 1 ) / ( 2 ^ y ) ) e. RR )
34 32 33 syl3an1 
 |-  ( ( x e. RR /\ ( 2 ^ y ) e. RR /\ ( 2 ^ y ) =/= 0 ) -> ( ( x + 1 ) / ( 2 ^ y ) ) e. RR )
35 opelxpi 
 |-  ( ( ( x / ( 2 ^ y ) ) e. RR /\ ( ( x + 1 ) / ( 2 ^ y ) ) e. RR ) -> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. e. ( RR X. RR ) )
36 31 34 35 syl2anc 
 |-  ( ( x e. RR /\ ( 2 ^ y ) e. RR /\ ( 2 ^ y ) =/= 0 ) -> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. e. ( RR X. RR ) )
37 36 3expb 
 |-  ( ( x e. RR /\ ( ( 2 ^ y ) e. RR /\ ( 2 ^ y ) =/= 0 ) ) -> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. e. ( RR X. RR ) )
38 20 30 37 syl2an 
 |-  ( ( x e. ZZ /\ y e. NN0 ) -> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. e. ( RR X. RR ) )
39 38 rgen2 
 |-  A. x e. ZZ A. y e. NN0 <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. e. ( RR X. RR )
40 eqid 
 |-  ( 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 ) ) >. )
41 40 fmpo 
 |-  ( 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 ) )
42 39 41 mpbi 
 |-  ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) : ( ZZ X. NN0 ) --> ( RR X. RR )
43 frn 
 |-  ( ( 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 ) )
44 42 43 ax-mp 
 |-  ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) C_ ( RR X. RR )
45 19 44 sstri 
 |-  { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } C_ ( RR X. RR )
46 18 45 sstri 
 |-  { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { 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 
 |-  ( { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { 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 
 |-  ran ( RR X. RR ) = RR
49 47 48 sseqtrdi 
 |-  ( { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { 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 )
50 46 49 ax-mp 
 |-  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 
 |-  ( { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { 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 
 |-  ( ( 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 )
53 50 51 52 sylancr 
 |-  ( { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { 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 )
54 53 adantl 
 |-  ( ( 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 
 |-  ( 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 
 |-  [,] : ( RR* X. RR* ) --> ~P RR*
57 ffn 
 |-  ( [,] : ( RR* X. RR* ) --> ~P RR* -> [,] Fn ( RR* X. RR* ) )
58 56 57 ax-mp 
 |-  [,] Fn ( RR* X. RR* )
59 rexpssxrxp 
 |-  ( RR X. RR ) C_ ( RR* X. RR* )
60 46 59 sstri 
 |-  { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { 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 
 |-  ( u = ( [,] ` v ) -> ( z e. u <-> z e. ( [,] ` v ) ) )
62 61 rexima 
 |-  ( ( [,] 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 ) ) )
63 58 60 62 mp2an 
 |-  ( 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 ) )
64 55 63 bitri 
 |-  ( 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 ) )
65 46 sseli 
 |-  ( 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 
 |-  ( v e. ( RR X. RR ) -> v = <. ( 1st ` v ) , ( 2nd ` v ) >. )
67 66 fveq2d 
 |-  ( v e. ( RR X. RR ) -> ( [,] ` v ) = ( [,] ` <. ( 1st ` v ) , ( 2nd ` v ) >. ) )
68 df-ov 
 |-  ( ( 1st ` v ) [,] ( 2nd ` v ) ) = ( [,] ` <. ( 1st ` v ) , ( 2nd ` v ) >. )
69 67 68 eqtr4di 
 |-  ( v e. ( RR X. RR ) -> ( [,] ` v ) = ( ( 1st ` v ) [,] ( 2nd ` v ) ) )
70 69 eleq2d 
 |-  ( v e. ( RR X. RR ) -> ( z e. ( [,] ` v ) <-> z e. ( ( 1st ` v ) [,] ( 2nd ` v ) ) ) )
71 65 70 syl 
 |-  ( 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 ) ) ) )
72 71 biimpd 
 |-  ( 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 ) ) ) )
73 72 imdistani 
 |-  ( ( 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 eliccxr 
 |-  ( z e. ( ( 1st ` v ) [,] ( 2nd ` v ) ) -> z e. RR* )
75 74 ad2antll 
 |-  ( ( ( ( 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* )
76 xp2nd 
 |-  ( v e. ( RR X. RR ) -> ( 2nd ` v ) e. RR )
77 76 rexrd 
 |-  ( v e. ( RR X. RR ) -> ( 2nd ` v ) e. RR* )
78 65 77 syl 
 |-  ( 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* )
79 78 ad2antrl 
 |-  ( ( ( ( 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* )
80 simpllr 
 |-  ( ( ( ( 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 )
81 80 rexrd 
 |-  ( ( ( ( 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* )
82 xp1st 
 |-  ( v e. ( RR X. RR ) -> ( 1st ` v ) e. RR )
83 82 rexrd 
 |-  ( v e. ( RR X. RR ) -> ( 1st ` v ) e. RR* )
84 83 77 jca 
 |-  ( v e. ( RR X. RR ) -> ( ( 1st ` v ) e. RR* /\ ( 2nd ` v ) e. RR* ) )
85 65 84 syl 
 |-  ( 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* ) )
86 iccleub 
 |-  ( ( ( 1st ` v ) e. RR* /\ ( 2nd ` v ) e. RR* /\ z e. ( ( 1st ` v ) [,] ( 2nd ` v ) ) ) -> z <_ ( 2nd ` v ) )
87 86 3expa 
 |-  ( ( ( ( 1st ` v ) e. RR* /\ ( 2nd ` v ) e. RR* ) /\ z e. ( ( 1st ` v ) [,] ( 2nd ` v ) ) ) -> z <_ ( 2nd ` v ) )
88 85 87 sylan 
 |-  ( ( 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 ) )
89 88 adantl 
 |-  ( ( ( ( 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 ) )
90 xpss 
 |-  ( RR X. RR ) C_ ( _V X. _V )
91 46 90 sstri 
 |-  { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { 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 )
92 df-rel 
 |-  ( 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 ) )
93 91 92 mpbir 
 |-  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 ) }
94 2ndrn 
 |-  ( ( 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 ) } )
95 93 94 mpan 
 |-  ( 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 ) } )
96 breq1 
 |-  ( u = ( 2nd ` v ) -> ( u <_ n <-> ( 2nd ` v ) <_ n ) )
97 96 rspccva 
 |-  ( ( 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 )
98 95 97 sylan2 
 |-  ( ( 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 )
99 98 ad2ant2lr 
 |-  ( ( ( ( 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 )
100 75 79 81 89 99 xrletrd 
 |-  ( ( ( ( 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 )
101 73 100 sylan2 
 |-  ( ( ( ( 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 )
102 101 rexlimdvaa 
 |-  ( ( ( 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 ) )
103 64 102 syl5bi 
 |-  ( ( ( 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 ) )
104 103 ralrimiv 
 |-  ( ( ( 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 )
105 raleq 
 |-  ( 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 ) )
106 105 ad2antrr 
 |-  ( ( ( 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 ) )
107 104 106 mpbid 
 |-  ( ( ( 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 )
108 107 ex 
 |-  ( ( 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 ) )
109 108 reximdva 
 |-  ( 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 ) )
110 109 adantr 
 |-  ( ( 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 ) )
111 54 110 mpd 
 |-  ( ( 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 )
112 17 111 nsyl 
 |-  ( 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 ) )
113 112 adantl 
 |-  ( ( ( 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 ) )
114 uniretop 
 |-  RR = U. ( topGen ` ran (,) )
115 retopconn 
 |-  ( topGen ` ran (,) ) e. Conn
116 115 a1i 
 |-  ( ( ( 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. Conn )
117 simpll 
 |-  ( ( ( 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 (,) ) )
118 simplr 
 |-  ( ( ( 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 =/= (/) )
119 simprl 
 |-  ( ( ( 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 )
120 ffun 
 |-  ( [,] : ( RR* X. RR* ) --> ~P RR* -> Fun [,] )
121 funiunfv 
 |-  ( 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 ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } ) )
122 56 120 121 mp2b 
 |-  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 ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } )
123 retop 
 |-  ( topGen ` ran (,) ) e. Top
124 46 sseli 
 |-  ( 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 e. ( RR X. RR ) )
125 1st2nd2 
 |-  ( z e. ( RR X. RR ) -> z = <. ( 1st ` z ) , ( 2nd ` z ) >. )
126 125 fveq2d 
 |-  ( z e. ( RR X. RR ) -> ( [,] ` z ) = ( [,] ` <. ( 1st ` z ) , ( 2nd ` z ) >. ) )
127 df-ov 
 |-  ( ( 1st ` z ) [,] ( 2nd ` z ) ) = ( [,] ` <. ( 1st ` z ) , ( 2nd ` z ) >. )
128 126 127 eqtr4di 
 |-  ( z e. ( RR X. RR ) -> ( [,] ` z ) = ( ( 1st ` z ) [,] ( 2nd ` z ) ) )
129 xp1st 
 |-  ( z e. ( RR X. RR ) -> ( 1st ` z ) e. RR )
130 xp2nd 
 |-  ( z e. ( RR X. RR ) -> ( 2nd ` z ) e. RR )
131 icccld 
 |-  ( ( ( 1st ` z ) e. RR /\ ( 2nd ` z ) e. RR ) -> ( ( 1st ` z ) [,] ( 2nd ` z ) ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
132 129 130 131 syl2anc 
 |-  ( z e. ( RR X. RR ) -> ( ( 1st ` z ) [,] ( 2nd ` z ) ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
133 128 132 eqeltrd 
 |-  ( z e. ( RR X. RR ) -> ( [,] ` z ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
134 124 133 syl 
 |-  ( 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 ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
135 134 rgen 
 |-  A. 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 ) e. ( Clsd ` ( topGen ` ran (,) ) )
136 114 iuncld 
 |-  ( ( ( topGen ` ran (,) ) e. Top /\ { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { 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. 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 ) e. ( Clsd ` ( topGen ` ran (,) ) ) ) -> 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 ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
137 123 135 136 mp3an13 
 |-  ( { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { 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_ 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 ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
138 122 137 eqeltrrid 
 |-  ( { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { 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 ) } ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
139 138 ad2antll 
 |-  ( ( ( 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 ) } ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
140 119 139 eqeltrrd 
 |-  ( ( ( 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. ( Clsd ` ( topGen ` ran (,) ) ) )
141 114 116 117 118 140 connclo 
 |-  ( ( ( 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 = RR )
142 141 ex 
 |-  ( ( 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 = RR ) )
143 142 necon3ad 
 |-  ( ( 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 ) ) )
144 143 imp 
 |-  ( ( ( 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 ) )
145 113 144 pm2.61dane 
 |-  ( ( 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 ) )
146 oveq1 
 |-  ( x = u -> ( x / ( 2 ^ y ) ) = ( u / ( 2 ^ y ) ) )
147 oveq1 
 |-  ( x = u -> ( x + 1 ) = ( u + 1 ) )
148 147 oveq1d 
 |-  ( x = u -> ( ( x + 1 ) / ( 2 ^ y ) ) = ( ( u + 1 ) / ( 2 ^ y ) ) )
149 146 148 opeq12d 
 |-  ( x = u -> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. = <. ( u / ( 2 ^ y ) ) , ( ( u + 1 ) / ( 2 ^ y ) ) >. )
150 oveq2 
 |-  ( y = v -> ( 2 ^ y ) = ( 2 ^ v ) )
151 150 oveq2d 
 |-  ( y = v -> ( u / ( 2 ^ y ) ) = ( u / ( 2 ^ v ) ) )
152 150 oveq2d 
 |-  ( y = v -> ( ( u + 1 ) / ( 2 ^ y ) ) = ( ( u + 1 ) / ( 2 ^ v ) ) )
153 151 152 opeq12d 
 |-  ( y = v -> <. ( u / ( 2 ^ y ) ) , ( ( u + 1 ) / ( 2 ^ y ) ) >. = <. ( u / ( 2 ^ v ) ) , ( ( u + 1 ) / ( 2 ^ v ) ) >. )
154 149 153 cbvmpov 
 |-  ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) = ( u e. ZZ , v e. NN0 |-> <. ( u / ( 2 ^ v ) ) , ( ( u + 1 ) / ( 2 ^ v ) ) >. )
155 fveq2 
 |-  ( a = z -> ( [,] ` a ) = ( [,] ` z ) )
156 155 sseq1d 
 |-  ( a = z -> ( ( [,] ` a ) C_ ( [,] ` c ) <-> ( [,] ` z ) C_ ( [,] ` c ) ) )
157 equequ1 
 |-  ( a = z -> ( a = c <-> z = c ) )
158 156 157 imbi12d 
 |-  ( a = z -> ( ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) <-> ( ( [,] ` z ) C_ ( [,] ` c ) -> z = c ) ) )
159 158 ralbidv 
 |-  ( a = z -> ( A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) <-> A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` z ) C_ ( [,] ` c ) -> z = c ) ) )
160 159 cbvrabv 
 |-  { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } = { z e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` z ) C_ ( [,] ` c ) -> z = c ) }
161 19 a1i 
 |-  ( A e. ( topGen ` ran (,) ) -> { 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 ) ) >. ) )
162 154 160 161 dyadmbllem 
 |-  ( A e. ( topGen ` ran (,) ) -> U. ( [,] " { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ) = U. ( [,] " { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } ) )
163 opnmbllem0 
 |-  ( A e. ( topGen ` ran (,) ) -> U. ( [,] " { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ) = A )
164 162 163 eqtr3d 
 |-  ( A e. ( topGen ` ran (,) ) -> 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 )
165 164 adantr 
 |-  ( ( 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 )
166 nnenom 
 |-  NN ~~ _om
167 sdomentr 
 |-  ( ( { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } ~< NN /\ NN ~~ _om ) -> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } ~< _om )
168 166 167 mpan2 
 |-  ( { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } ~< NN -> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } ~< _om )
169 isfinite 
 |-  ( { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { 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. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } ~< _om )
170 168 169 sylibr 
 |-  ( { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } ~< NN -> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } e. Fin )
171 165 170 anim12i 
 |-  ( ( ( A e. ( topGen ` ran (,) ) /\ 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 ) } ~< NN ) -> ( 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 ) )
172 145 171 mtand 
 |-  ( ( A e. ( topGen ` ran (,) ) /\ 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 ) } ~< NN )
173 qex 
 |-  QQ e. _V
174 173 173 xpex 
 |-  ( QQ X. QQ ) e. _V
175 zq 
 |-  ( x e. ZZ -> x e. QQ )
176 2nn 
 |-  2 e. NN
177 nnq 
 |-  ( 2 e. NN -> 2 e. QQ )
178 176 177 ax-mp 
 |-  2 e. QQ
179 qexpcl 
 |-  ( ( 2 e. QQ /\ y e. NN0 ) -> ( 2 ^ y ) e. QQ )
180 178 179 mpan 
 |-  ( y e. NN0 -> ( 2 ^ y ) e. QQ )
181 180 29 jca 
 |-  ( y e. NN0 -> ( ( 2 ^ y ) e. QQ /\ ( 2 ^ y ) =/= 0 ) )
182 qdivcl 
 |-  ( ( x e. QQ /\ ( 2 ^ y ) e. QQ /\ ( 2 ^ y ) =/= 0 ) -> ( x / ( 2 ^ y ) ) e. QQ )
183 1z 
 |-  1 e. ZZ
184 zq 
 |-  ( 1 e. ZZ -> 1 e. QQ )
185 183 184 ax-mp 
 |-  1 e. QQ
186 qaddcl 
 |-  ( ( x e. QQ /\ 1 e. QQ ) -> ( x + 1 ) e. QQ )
187 185 186 mpan2 
 |-  ( x e. QQ -> ( x + 1 ) e. QQ )
188 qdivcl 
 |-  ( ( ( x + 1 ) e. QQ /\ ( 2 ^ y ) e. QQ /\ ( 2 ^ y ) =/= 0 ) -> ( ( x + 1 ) / ( 2 ^ y ) ) e. QQ )
189 187 188 syl3an1 
 |-  ( ( x e. QQ /\ ( 2 ^ y ) e. QQ /\ ( 2 ^ y ) =/= 0 ) -> ( ( x + 1 ) / ( 2 ^ y ) ) e. QQ )
190 opelxpi 
 |-  ( ( ( x / ( 2 ^ y ) ) e. QQ /\ ( ( x + 1 ) / ( 2 ^ y ) ) e. QQ ) -> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. e. ( QQ X. QQ ) )
191 182 189 190 syl2anc 
 |-  ( ( x e. QQ /\ ( 2 ^ y ) e. QQ /\ ( 2 ^ y ) =/= 0 ) -> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. e. ( QQ X. QQ ) )
192 191 3expb 
 |-  ( ( x e. QQ /\ ( ( 2 ^ y ) e. QQ /\ ( 2 ^ y ) =/= 0 ) ) -> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. e. ( QQ X. QQ ) )
193 175 181 192 syl2an 
 |-  ( ( x e. ZZ /\ y e. NN0 ) -> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. e. ( QQ X. QQ ) )
194 193 rgen2 
 |-  A. x e. ZZ A. y e. NN0 <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. e. ( QQ X. QQ )
195 40 fmpo 
 |-  ( A. x e. ZZ A. y e. NN0 <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. e. ( QQ X. QQ ) <-> ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) : ( ZZ X. NN0 ) --> ( QQ X. QQ ) )
196 194 195 mpbi 
 |-  ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) : ( ZZ X. NN0 ) --> ( QQ X. QQ )
197 frn 
 |-  ( ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) : ( ZZ X. NN0 ) --> ( QQ X. QQ ) -> ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) C_ ( QQ X. QQ ) )
198 196 197 ax-mp 
 |-  ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) C_ ( QQ X. QQ )
199 19 198 sstri 
 |-  { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } C_ ( QQ X. QQ )
200 18 199 sstri 
 |-  { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { 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_ ( QQ X. QQ )
201 ssdomg 
 |-  ( ( QQ X. QQ ) e. _V -> ( { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { 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_ ( QQ X. QQ ) -> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } ~<_ ( QQ X. QQ ) ) )
202 174 200 201 mp2 
 |-  { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } ~<_ ( QQ X. QQ )
203 qnnen 
 |-  QQ ~~ NN
204 xpen 
 |-  ( ( QQ ~~ NN /\ QQ ~~ NN ) -> ( QQ X. QQ ) ~~ ( NN X. NN ) )
205 203 203 204 mp2an 
 |-  ( QQ X. QQ ) ~~ ( NN X. NN )
206 xpnnen 
 |-  ( NN X. NN ) ~~ NN
207 205 206 entri 
 |-  ( QQ X. QQ ) ~~ NN
208 domentr 
 |-  ( ( { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } ~<_ ( QQ X. QQ ) /\ ( QQ X. QQ ) ~~ NN ) -> { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } ~<_ NN )
209 202 207 208 mp2an 
 |-  { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } ~<_ NN
210 172 209 jctil 
 |-  ( ( A e. ( topGen ` ran (,) ) /\ 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 ) } ~<_ NN /\ -. { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } ~< NN ) )
211 bren2 
 |-  ( { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } ~~ NN <-> ( { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } ~<_ NN /\ -. { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } ~< NN ) )
212 210 211 sylibr 
 |-  ( ( A e. ( topGen ` ran (,) ) /\ 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 ) } ~~ NN )
213 212 ensymd 
 |-  ( ( A e. ( topGen ` ran (,) ) /\ A =/= (/) ) -> NN ~~ { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } )
214 bren 
 |-  ( NN ~~ { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } <-> 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 ) } )
215 213 214 sylib 
 |-  ( ( 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 ) } )