Metamath Proof Explorer

Theorem dya2iocct

Description: The dyadic rectangle set is countable. (Contributed by Thierry Arnoux, 18-Sep-2017) (Revised by Thierry Arnoux, 11-Oct-2017)

Ref Expression
Hypotheses sxbrsiga.0 
|- J = ( topGen ` ran (,) )
dya2ioc.1 
|- I = ( x e. ZZ , n e. ZZ |-> ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) )
dya2ioc.2 
|- R = ( u e. ran I , v e. ran I |-> ( u X. v ) )
Assertion dya2iocct 
|- ran R ~<_ _om

Proof

Step Hyp Ref Expression
1 sxbrsiga.0 
 |-  J = ( topGen ` ran (,) )
2 dya2ioc.1 
 |-  I = ( x e. ZZ , n e. ZZ |-> ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) )
3 dya2ioc.2 
 |-  R = ( u e. ran I , v e. ran I |-> ( u X. v ) )
4 znnen 
 |-  ZZ ~~ NN
5 nnct 
 |-  NN ~<_ _om
6 endomtr 
 |-  ( ( ZZ ~~ NN /\ NN ~<_ _om ) -> ZZ ~<_ _om )
7 4 5 6 mp2an 
 |-  ZZ ~<_ _om
8 ovex 
 |-  ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) e. _V
9 8 rgen2w 
 |-  A. x e. ZZ A. n e. ZZ ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) e. _V
10 9 mpocti 
 |-  ( ( ZZ ~<_ _om /\ ZZ ~<_ _om ) -> ( x e. ZZ , n e. ZZ |-> ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) ) ~<_ _om )
11 7 7 10 mp2an 
 |-  ( x e. ZZ , n e. ZZ |-> ( ( x / ( 2 ^ n ) ) [,) ( ( x + 1 ) / ( 2 ^ n ) ) ) ) ~<_ _om
12 2 11 eqbrtri 
 |-  I ~<_ _om
13 rnct 
 |-  ( I ~<_ _om -> ran I ~<_ _om )
14 12 13 ax-mp 
 |-  ran I ~<_ _om
15 vex 
 |-  u e. _V
16 vex 
 |-  v e. _V
17 15 16 xpex 
 |-  ( u X. v ) e. _V
18 17 rgen2w 
 |-  A. u e. ran I A. v e. ran I ( u X. v ) e. _V
19 18 mpocti 
 |-  ( ( ran I ~<_ _om /\ ran I ~<_ _om ) -> ( u e. ran I , v e. ran I |-> ( u X. v ) ) ~<_ _om )
20 3 breq1i 
 |-  ( R ~<_ _om <-> ( u e. ran I , v e. ran I |-> ( u X. v ) ) ~<_ _om )
21 20 biimpri 
 |-  ( ( u e. ran I , v e. ran I |-> ( u X. v ) ) ~<_ _om -> R ~<_ _om )
22 rnct 
 |-  ( R ~<_ _om -> ran R ~<_ _om )
23 19 21 22 3syl 
 |-  ( ( ran I ~<_ _om /\ ran I ~<_ _om ) -> ran R ~<_ _om )
24 14 14 23 mp2an 
 |-  ran R ~<_ _om