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 33446
Description: Lemma for ismblfin 33450, 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 10209 . . . . . . . . . . . . 13 |- ( n e. RR -> ( n + 1 ) e. RR )
2 ltp1 10861 . . . . . . . . . . . . 13 |- ( n e. RR -> n < ( n + 1 ) )
3 breq2 4657 . . . . . . . . . . . . . 14 |- ( z = ( n + 1 ) -> ( n < z <-> n < ( n + 1 ) ) )
43rspcev 3309 . . . . . . . . . . . . 13 |- ( ( ( n + 1 ) e. RR /\ n < ( n + 1 ) ) -> E. z e. RR n < z )
51, 2, 4syl2anc 693 . . . . . . . . . . . 12 |- ( n e. RR -> E. z e. RR n < z )
65rgen 2922 . . . . . . . . . . 11 |- A. n e. RR E. z e. RR n < z
7 ltnle 10117 . . . . . . . . . . . . . . 15 |- ( ( n e. RR /\ z e. RR ) -> ( n < z <-> -. z <_ n ) )
87rexbidva 3049 . . . . . . . . . . . . . 14 |- ( n e. RR -> ( E. z e. RR n < z <-> E. z e. RR -. z <_ n ) )
9 rexnal 2995 . . . . . . . . . . . . . 14 |- ( E. z e. RR -. z <_ n <-> -. A. z e. RR z <_ n )
108, 9syl6bb 276 . . . . . . . . . . . . 13 |- ( n e. RR -> ( E. z e. RR n < z <-> -. A. z e. RR z <_ n ) )
1110ralbiia 2979 . . . . . . . . . . . 12 |- ( A. n e. RR E. z e. RR n < z <-> A. n e. RR -. A. z e. RR z <_ n )
12 ralnex 2992 . . . . . . . . . . . 12 |- ( A. n e. RR -. A. z e. RR z <_ n <-> -. E. n e. RR A. z e. RR z <_ n )
1311, 12bitri 264 . . . . . . . . . . 11 |- ( A. n e. RR E. z e. RR n < z <-> -. E. n e. RR A. z e. RR z <_ n )
146, 13mpbi 220 . . . . . . . . . 10 |- -. E. n e. RR A. z e. RR z <_ n
15 raleq 3138 . . . . . . . . . . 11 |- ( A = RR -> ( A. z e. A z <_ n <-> A. z e. RR z <_ n ) )
1615rexbidv 3052 . . . . . . . . . 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 317 . . . . . . . . 9 |- ( A = RR -> -. E. n e. RR A. z e. A z <_ n )
18 ssrab2 3687 . . . . . . . . . . . . . 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 3687 . . . . . . . . . . . . . . 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 11381 . . . . . . . . . . . . . . . . . . 19 |- ( x e. ZZ -> x e. RR )
21 2re 11090 . . . . . . . . . . . . . . . . . . . . 21 |- 2 e. RR
22 reexpcl 12877 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( 2 e. RR /\ y e. NN0 ) -> ( 2 ^ y ) e. RR )
2321, 22mpan 706 . . . . . . . . . . . . . . . . . . . 20 |- ( y e. NN0 -> ( 2 ^ y ) e. RR )
24 nn0z 11400 . . . . . . . . . . . . . . . . . . . . 21 |- ( y e. NN0 -> y e. ZZ )
25 2cn 11091 . . . . . . . . . . . . . . . . . . . . . 22 |- 2 e. CC
26 2ne0 11113 . . . . . . . . . . . . . . . . . . . . . 22 |- 2 =/= 0
27 expne0i 12892 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( 2 e. CC /\ 2 =/= 0 /\ y e. ZZ ) -> ( 2 ^ y ) =/= 0 )
2825, 26, 27mp3an12 1414 . . . . . . . . . . . . . . . . . . . . 21 |- ( y e. ZZ -> ( 2 ^ y ) =/= 0 )
2924, 28syl 17 . . . . . . . . . . . . . . . . . . . 20 |- ( y e. NN0 -> ( 2 ^ y ) =/= 0 )
3023, 29jca 554 . . . . . . . . . . . . . . . . . . 19 |- ( y e. NN0 -> ( ( 2 ^ y ) e. RR /\ ( 2 ^ y ) =/= 0 ) )
31 redivcl 10744 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( x e. RR /\ ( 2 ^ y ) e. RR /\ ( 2 ^ y ) =/= 0 ) -> ( x / ( 2 ^ y ) ) e. RR )
32 peano2re 10209 . . . . . . . . . . . . . . . . . . . . . 22 |- ( x e. RR -> ( x + 1 ) e. RR )
33 redivcl 10744 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( x + 1 ) e. RR /\ ( 2 ^ y ) e. RR /\ ( 2 ^ y ) =/= 0 ) -> ( ( x + 1 ) / ( 2 ^ y ) ) e. RR )
3432, 33syl3an1 1359 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( x e. RR /\ ( 2 ^ y ) e. RR /\ ( 2 ^ y ) =/= 0 ) -> ( ( x + 1 ) / ( 2 ^ y ) ) e. RR )
35 opelxpi 5148 . . . . . . . . . . . . . . . . . . . . 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 693 . . . . . . . . . . . . . . . . . . . 20 |- ( ( x e. RR /\ ( 2 ^ y ) e. RR /\ ( 2 ^ y ) =/= 0 ) -> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. e. ( RR X. RR ) )
37363expb 1266 . . . . . . . . . . . . . . . . . . 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 494 . . . . . . . . . . . . . . . . . 18 |- ( ( x e. ZZ /\ y e. NN0 ) -> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. e. ( RR X. RR ) )
3938rgen2 2975 . . . . . . . . . . . . . . . . 17 |- A. x e. ZZ A. y e. NN0 <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. e. ( RR X. RR )
40 eqid 2622 . . . . . . . . . . . . . . . . . 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 7237 . . . . . . . . . . . . . . . . 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 220 . . . . . . . . . . . . . . . 16 |- ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) : ( ZZ X. NN0 ) --> ( RR X. RR )
43 frn 6053 . . . . . . . . . . . . . . . 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 3612 . . . . . . . . . . . . . 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 3612 . . . . . . . . . . . . 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 5354 . . . . . . . . . . . . . 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 5567 . . . . . . . . . . . . . 14 |- ran ( RR X. RR ) = RR
4947, 48syl6sseq 3651 . . . . . . . . . . . . 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 8249 . . . . . . . . . . . 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 10969 . . . . . . . . . . . 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 695 . . . . . . . . . . 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 482 . . . . . . . . . 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 4440 . . . . . . . . . . . . . . . . 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 12272 . . . . . . . . . . . . . . . . . . 19 |- [,] : ( RR* X. RR* ) --> ~P RR*
57 ffn 6045 . . . . . . . . . . . . . . . . . . 19 |- ( [,] : ( RR* X. RR* ) --> ~P RR* -> [,] Fn ( RR* X. RR* ) )
5856, 57ax-mp 5 . . . . . . . . . . . . . . . . . 18 |- [,] Fn ( RR* X. RR* )
59 rexpssxrxp 10084 . . . . . . . . . . . . . . . . . . 19 |- ( RR X. RR ) C_ ( RR* X. RR* )
6046, 59sstri 3612 . . . . . . . . . . . . . . . . . 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 2690 . . . . . . . . . . . . . . . . . . 19 |- ( u = ( [,] ` v ) -> ( z e. u <-> z e. ( [,] ` v ) ) )
6261rexima 6497 . . . . . . . . . . . . . . . . . 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 708 . . . . . . . . . . . . . . . . 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 264 . . . . . . . . . . . . . . . 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 3599 . . . . . . . . . . . . . . . . . . . . 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 7205 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( v e. ( RR X. RR ) -> v = <. ( 1st ` v ) , ( 2nd ` v ) >. )
6766fveq2d 6195 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( v e. ( RR X. RR ) -> ( [,] ` v ) = ( [,] ` <. ( 1st ` v ) , ( 2nd ` v ) >. ) )
68 df-ov 6653 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( 1st ` v ) [,] ( 2nd ` v ) ) = ( [,] ` <. ( 1st ` v ) , ( 2nd ` v ) >. )
6967, 68syl6eqr 2674 . . . . . . . . . . . . . . . . . . . . . 22 |- ( v e. ( RR X. RR ) -> ( [,] ` v ) = ( ( 1st ` v ) [,] ( 2nd ` v ) ) )
7069eleq2d 2687 . . . . . . . . . . . . . . . . . . . . 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 219 . . . . . . . . . . . . . . . . . . 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 726 . . . . . . . . . . . . . . . . . 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 12256 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( 1st ` v ) [,] ( 2nd ` v ) ) C_ RR*
7574sseli 3599 . . . . . . . . . . . . . . . . . . . 20 |- ( z e. ( ( 1st ` v ) [,] ( 2nd ` v ) ) -> z e. RR* )
7675ad2antll 765 . . . . . . . . . . . . . . . . . . 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 7199 . . . . . . . . . . . . . . . . . . . . . 22 |- ( v e. ( RR X. RR ) -> ( 2nd ` v ) e. RR )
7877rexrd 10089 . . . . . . . . . . . . . . . . . . . . 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 764 . . . . . . . . . . . . . . . . . . 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 799 . . . . . . . . . . . . . . . . . . . 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 10089 . . . . . . . . . . . . . . . . . . 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 7198 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( v e. ( RR X. RR ) -> ( 1st ` v ) e. RR )
8483rexrd 10089 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( v e. ( RR X. RR ) -> ( 1st ` v ) e. RR* )
8584, 78jca 554 . . . . . . . . . . . . . . . . . . . . . 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 12229 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( 1st ` v ) e. RR* /\ ( 2nd ` v ) e. RR* /\ z e. ( ( 1st ` v ) [,] ( 2nd ` v ) ) ) -> z <_ ( 2nd ` v ) )
88873expa 1265 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( 1st ` v ) e. RR* /\ ( 2nd ` v ) e. RR* ) /\ z e. ( ( 1st ` v ) [,] ( 2nd ` v ) ) ) -> z <_ ( 2nd ` v ) )
8986, 88sylan 488 . . . . . . . . . . . . . . . . . . . 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 482 . . . . . . . . . . . . . . . . . . 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 5226 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( RR X. RR ) C_ ( _V X. _V )
9246, 91sstri 3612 . . . . . . . . . . . . . . . . . . . . . . 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 5121 . . . . . . . . . . . . . . . . . . . . . . 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 221 . . . . . . . . . . . . . . . . . . . . . 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 7216 . . . . . . . . . . . . . . . . . . . . . 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 706 . . . . . . . . . . . . . . . . . . . . 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 4656 . . . . . . . . . . . . . . . . . . . . . 22 |- ( u = ( 2nd ` v ) -> ( u <_ n <-> ( 2nd ` v ) <_ n ) )
9897rspccva 3308 . . . . . . . . . . . . . . . . . . . . 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 491 . . . . . . . . . . . . . . . . . . . 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 784 . . . . . . . . . . . . . . . . . . 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 11993 . . . . . . . . . . . . . . . . . 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 491 . . . . . . . . . . . . . . . . 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 3032 . . . . . . . . . . . . . . . 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 232 . . . . . . . . . . . . . . 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 2965 . . . . . . . . . . . . . 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 3138 . . . . . . . . . . . . . . 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 762 . . . . . . . . . . . . . 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 222 . . . . . . . . . . . . 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 450 . . . . . . . . . . . 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 3017 . . . . . . . . . . 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 481 . . . . . . . . . 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 135 . . . . . . . 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 482 . . . . . . 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 22566 . . . . . . . . . . 11 |- RR = U. ( topGen ` ran (,) )
116 retopconn 22632 . . . . . . . . . . . 12 |- ( topGen ` ran (,) ) e. Conn
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. Conn )
118 simpll 790 . . . . . . . . . . 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 792 . . . . . . . . . . 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 794 . . . . . . . . . . . 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 6048 . . . . . . . . . . . . . . 15 |- ( [,] : ( RR* X. RR* ) --> ~P RR* -> Fun [,] )
122 funiunfv 6506 . . . . . . . . . . . . . . 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 ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } ) )
12356, 121, 122mp2b 10 . . . . . . . . . . . . . 14 |- 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 ) } )
124 retop 22565 . . . . . . . . . . . . . . 15 |- ( topGen ` ran (,) ) e. Top
12546sseli 3599 . . . . . . . . . . . . . . . . 17 |- ( 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 ) )
126 1st2nd2 7205 . . . . . . . . . . . . . . . . . . . 20 |- ( z e. ( RR X. RR ) -> z = <. ( 1st ` z ) , ( 2nd ` z ) >. )
127126fveq2d 6195 . . . . . . . . . . . . . . . . . . 19 |- ( z e. ( RR X. RR ) -> ( [,] ` z ) = ( [,] ` <. ( 1st ` z ) , ( 2nd ` z ) >. ) )
128 df-ov 6653 . . . . . . . . . . . . . . . . . . 19 |- ( ( 1st ` z ) [,] ( 2nd ` z ) ) = ( [,] ` <. ( 1st ` z ) , ( 2nd ` z ) >. )
129127, 128syl6eqr 2674 . . . . . . . . . . . . . . . . . 18 |- ( z e. ( RR X. RR ) -> ( [,] ` z ) = ( ( 1st ` z ) [,] ( 2nd ` z ) ) )
130 xp1st 7198 . . . . . . . . . . . . . . . . . . 19 |- ( z e. ( RR X. RR ) -> ( 1st ` z ) e. RR )
131 xp2nd 7199 . . . . . . . . . . . . . . . . . . 19 |- ( z e. ( RR X. RR ) -> ( 2nd ` z ) e. RR )
132 icccld 22570 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( 1st ` z ) e. RR /\ ( 2nd ` z ) e. RR ) -> ( ( 1st ` z ) [,] ( 2nd ` z ) ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
133130, 131, 132syl2anc 693 . . . . . . . . . . . . . . . . . 18 |- ( z e. ( RR X. RR ) -> ( ( 1st ` z ) [,] ( 2nd ` z ) ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
134129, 133eqeltrd 2701 . . . . . . . . . . . . . . . . 17 |- ( z e. ( RR X. RR ) -> ( [,] ` z ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
135125, 134syl 17 . . . . . . . . . . . . . . . 16 |- ( 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 (,) ) ) )
136135rgen 2922 . . . . . . . . . . . . . . 15 |- 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 (,) ) )
137115iuncld 20849 . . . . . . . . . . . . . . 15 |- ( ( ( 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 (,) ) ) )
138124, 136, 137mp3an13 1415 . . . . . . . . . . . . . 14 |- ( { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) } e. Fin -> 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 (,) ) ) )
139123, 138syl5eqelr 2706 . . . . . . . . . . . . 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 ) } 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 (,) ) ) )
140139ad2antll 765 . . . . . . . . . . . 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 ) } ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
141120, 140eqeltrrd 2702 . . . . . . . . . . 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. ( Clsd ` ( topGen ` ran (,) ) ) )
142115, 117, 118, 119, 141connclo 21218 . . . . . . . . . 10 |- ( ( ( 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 )
143142ex 450 . . . . . . . . 9 |- ( ( 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 ) )
144143necon3ad 2807 . . . . . . . 8 |- ( ( 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 ) ) )
145144imp 445 . . . . . . 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 ) )
146114, 145pm2.61dane 2881 . . . . . 6 |- ( ( 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 ) )
147 oveq1 6657 . . . . . . . . . . . 12 |- ( x = u -> ( x / ( 2 ^ y ) ) = ( u / ( 2 ^ y ) ) )
148 oveq1 6657 . . . . . . . . . . . . 13 |- ( x = u -> ( x + 1 ) = ( u + 1 ) )
149148oveq1d 6665 . . . . . . . . . . . 12 |- ( x = u -> ( ( x + 1 ) / ( 2 ^ y ) ) = ( ( u + 1 ) / ( 2 ^ y ) ) )
150147, 149opeq12d 4410 . . . . . . . . . . 11 |- ( x = u -> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. = <. ( u / ( 2 ^ y ) ) , ( ( u + 1 ) / ( 2 ^ y ) ) >. )
151 oveq2 6658 . . . . . . . . . . . . 13 |- ( y = v -> ( 2 ^ y ) = ( 2 ^ v ) )
152151oveq2d 6666 . . . . . . . . . . . 12 |- ( y = v -> ( u / ( 2 ^ y ) ) = ( u / ( 2 ^ v ) ) )
153151oveq2d 6666 . . . . . . . . . . . 12 |- ( y = v -> ( ( u + 1 ) / ( 2 ^ y ) ) = ( ( u + 1 ) / ( 2 ^ v ) ) )
154152, 153opeq12d 4410 . . . . . . . . . . 11 |- ( y = v -> <. ( u / ( 2 ^ y ) ) , ( ( u + 1 ) / ( 2 ^ y ) ) >. = <. ( u / ( 2 ^ v ) ) , ( ( u + 1 ) / ( 2 ^ v ) ) >. )
155150, 154cbvmpt2v 6735 . . . . . . . . . 10 |- ( 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 ) ) >. )
156 fveq2 6191 . . . . . . . . . . . . . 14 |- ( a = z -> ( [,] ` a ) = ( [,] ` z ) )
157156sseq1d 3632 . . . . . . . . . . . . 13 |- ( a = z -> ( ( [,] ` a ) C_ ( [,] ` c ) <-> ( [,] ` z ) C_ ( [,] ` c ) ) )
158 equequ1 1952 . . . . . . . . . . . . 13 |- ( a = z -> ( a = c <-> z = c ) )
159157, 158imbi12d 334 . . . . . . . . . . . 12 |- ( a = z -> ( ( ( [,] ` a ) C_ ( [,] ` c ) -> a = c ) <-> ( ( [,] ` z ) C_ ( [,] ` c ) -> z = c ) ) )
160159ralbidv 2986 . . . . . . . . . . 11 |- ( 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 ) ) )
161160cbvrabv 3199 . . . . . . . . . 10 |- { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { 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 ) }
16219a1i 11 . . . . . . . . . 10 |- ( 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 ) ) >. ) )
163155, 161, 162dyadmbllem 23367 . . . . . . . . 9 |- ( 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 ) } ) )
164 opnmbllem0 33445 . . . . . . . . 9 |- ( 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 )
165163, 164eqtr3d 2658 . . . . . . . 8 |- ( 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 )
166165adantr 481 . . . . . . 7 |- ( ( 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 )
167 nnenom 12779 . . . . . . . . 9 |- NN ~~ om
168 sdomentr 8094 . . . . . . . . 9 |- ( ( { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { 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 )
169167, 168mpan2 707 . . . . . . . 8 |- ( { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { 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 )
170 isfinite 8549 . . . . . . . 8 |- ( { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { 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 )
171169, 170sylibr 224 . . . . . . 7 |- ( { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { 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 )
172166, 171anim12i 590 . . . . . 6 |- ( ( ( 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 ) )
173146, 172mtand 691 . . . . 5 |- ( ( 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 )
174 qex 11800 . . . . . . . 8 |- QQ e. _V
175174, 174xpex 6962 . . . . . . 7 |- ( QQ X. QQ ) e. _V
176 zq 11794 . . . . . . . . . . . . 13 |- ( x e. ZZ -> x e. QQ )
177 2nn 11185 . . . . . . . . . . . . . . . 16 |- 2 e. NN
178 nnq 11801 . . . . . . . . . . . . . . . 16 |- ( 2 e. NN -> 2 e. QQ )
179177, 178ax-mp 5 . . . . . . . . . . . . . . 15 |- 2 e. QQ
180 qexpcl 12876 . . . . . . . . . . . . . . 15 |- ( ( 2 e. QQ /\ y e. NN0 ) -> ( 2 ^ y ) e. QQ )
181179, 180mpan 706 . . . . . . . . . . . . . 14 |- ( y e. NN0 -> ( 2 ^ y ) e. QQ )
182181, 29jca 554 . . . . . . . . . . . . 13 |- ( y e. NN0 -> ( ( 2 ^ y ) e. QQ /\ ( 2 ^ y ) =/= 0 ) )
183 qdivcl 11809 . . . . . . . . . . . . . . 15 |- ( ( x e. QQ /\ ( 2 ^ y ) e. QQ /\ ( 2 ^ y ) =/= 0 ) -> ( x / ( 2 ^ y ) ) e. QQ )
184 1z 11407 . . . . . . . . . . . . . . . . . 18 |- 1 e. ZZ
185 zq 11794 . . . . . . . . . . . . . . . . . 18 |- ( 1 e. ZZ -> 1 e. QQ )
186184, 185ax-mp 5 . . . . . . . . . . . . . . . . 17 |- 1 e. QQ
187 qaddcl 11804 . . . . . . . . . . . . . . . . 17 |- ( ( x e. QQ /\ 1 e. QQ ) -> ( x + 1 ) e. QQ )
188186, 187mpan2 707 . . . . . . . . . . . . . . . 16 |- ( x e. QQ -> ( x + 1 ) e. QQ )
189 qdivcl 11809 . . . . . . . . . . . . . . . 16 |- ( ( ( x + 1 ) e. QQ /\ ( 2 ^ y ) e. QQ /\ ( 2 ^ y ) =/= 0 ) -> ( ( x + 1 ) / ( 2 ^ y ) ) e. QQ )
190188, 189syl3an1 1359 . . . . . . . . . . . . . . 15 |- ( ( x e. QQ /\ ( 2 ^ y ) e. QQ /\ ( 2 ^ y ) =/= 0 ) -> ( ( x + 1 ) / ( 2 ^ y ) ) e. QQ )
191 opelxpi 5148 . . . . . . . . . . . . . . 15 |- ( ( ( x / ( 2 ^ y ) ) e. QQ /\ ( ( x + 1 ) / ( 2 ^ y ) ) e. QQ ) -> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. e. ( QQ X. QQ ) )
192183, 190, 191syl2anc 693 . . . . . . . . . . . . . 14 |- ( ( x e. QQ /\ ( 2 ^ y ) e. QQ /\ ( 2 ^ y ) =/= 0 ) -> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. e. ( QQ X. QQ ) )
1931923expb 1266 . . . . . . . . . . . . 13 |- ( ( x e. QQ /\ ( ( 2 ^ y ) e. QQ /\ ( 2 ^ y ) =/= 0 ) ) -> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. e. ( QQ X. QQ ) )
194176, 182, 193syl2an 494 . . . . . . . . . . . 12 |- ( ( x e. ZZ /\ y e. NN0 ) -> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. e. ( QQ X. QQ ) )
195194rgen2 2975 . . . . . . . . . . 11 |- A. x e. ZZ A. y e. NN0 <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. e. ( QQ X. QQ )
19640fmpt2 7237 . . . . . . . . . . 11 |- ( 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 ) )
197195, 196mpbi 220 . . . . . . . . . 10 |- ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) : ( ZZ X. NN0 ) --> ( QQ X. QQ )
198 frn 6053 . . . . . . . . . 10 |- ( ( 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 ) )
199197, 198ax-mp 5 . . . . . . . . 9 |- ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) C_ ( QQ X. QQ )
20019, 199sstri 3612 . . . . . . . 8 |- { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } C_ ( QQ X. QQ )
20118, 200sstri 3612 . . . . . . 7 |- { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { 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 )
202 ssdomg 8001 . . . . . . 7 |- ( ( 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 ) ) )
203175, 201, 202mp2 9 . . . . . 6 |- { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { 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 )
204 qnnen 14942 . . . . . . . 8 |- QQ ~~ NN
205 xpen 8123 . . . . . . . 8 |- ( ( QQ ~~ NN /\ QQ ~~ NN ) -> ( QQ X. QQ ) ~~ ( NN X. NN ) )
206204, 204, 205mp2an 708 . . . . . . 7 |- ( QQ X. QQ ) ~~ ( NN X. NN )
207 xpnnen 14939 . . . . . . 7 |- ( NN X. NN ) ~~ NN
208206, 207entri 8010 . . . . . 6 |- ( QQ X. QQ ) ~~ NN
209 domentr 8015 . . . . . 6 |- ( ( { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { 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 )
210203, 208, 209mp2an 708 . . . . 5 |- { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { 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
211173, 210jctil 560 . . . 4 |- ( ( 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 ) )
212 bren2 7986 . . . 4 |- ( { a e. { b e. ran ( x e. ZZ , y e. NN0 |-> <. ( x / ( 2 ^ y ) ) , ( ( x + 1 ) / ( 2 ^ y ) ) >. ) | ( [,] ` b ) C_ A } | A. c e. { 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 ) )
213211, 212sylibr 224 . . 3 |- ( ( 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 )
214213ensymd 8007 . 2 |- ( ( 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 ) } )
215 bren 7964 . 2 |- ( 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 ) } )
216214, 215sylib 208 1 |- ( ( 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 ) } )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   E.wex 1704   e. wcel 1990   =/= wne 2794   A.wral 2912   E.wrex 2913   {crab 2916   _Vcvv 3200   C_ wss 3574   (/)c0 3915   ~Pcpw 4158   <.cop 4183   U.cuni 4436   U_ciun 4520   class class class wbr 4653   X. cxp 5112   ran crn 5115   "cima 5117   Rel wrel 5119   Fun wfun 5882   Fn wfn 5883   -->wf 5884   -1-1-onto->wf1o 5887   ` cfv 5888  (class class class)co 6650   |-> cmpt2 6652   omcom 7065   1stc1st 7166   2ndc2nd 7167   ~~ cen 7952   ~<_ cdom 7953   ~< csdm 7954   Fincfn 7955   CCcc 9934   RRcr 9935   0cc0 9936   1c1 9937   + caddc 9939   RR*cxr 10073   < clt 10074   <_ cle 10075   / cdiv 10684   NNcn 11020   2c2 11070   NN0cn0 11292   ZZcz 11377   QQcq 11788   (,)cioo 12175   [,]cicc 12178   ^cexp 12860   topGenctg 16098   Topctop 20698   Clsdccld 20820  Conncconn 21214
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-inf2 8538  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-fal 1489  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-iin 4523  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-se 5074  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-oadd 7564  df-omul 7565  df-er 7742  df-map 7859  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-fi 8317  df-sup 8348  df-inf 8349  df-oi 8415  df-card 8765  df-acn 8768  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-n0 11293  df-z 11378  df-uz 11688  df-q 11789  df-rp 11833  df-xneg 11946  df-xadd 11947  df-xmul 11948  df-ioo 12179  df-ico 12181  df-icc 12182  df-fz 12327  df-fzo 12466  df-fl 12593  df-seq 12802  df-exp 12861  df-hash 13118  df-cj 13839  df-re 13840  df-im 13841  df-sqrt 13975  df-abs 13976  df-clim 14219  df-sum 14417  df-rest 16083  df-topgen 16104  df-psmet 19738  df-xmet 19739  df-met 19740  df-bl 19741  df-mopn 19742  df-top 20699  df-topon 20716  df-bases 20750  df-cld 20823  df-cmp 21190  df-conn 21215  df-ovol 23233
This theorem is referenced by:  mblfinlem2  33447
  Copyright terms: Public domain W3C validator