# Metamath Proof Explorer

## Theorem dya2iocucvr

Description: The dyadic rectangular set collection covers ( RR X. RR ) . (Contributed by Thierry Arnoux, 18-Sep-2017)

Ref Expression
Hypotheses sxbrsiga.0 ${⊢}{J}=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
dya2ioc.1 ${⊢}{I}=\left({x}\in ℤ,{n}\in ℤ⟼\left[\frac{{x}}{{2}^{{n}}},\frac{{x}+1}{{2}^{{n}}}\right)\right)$
dya2ioc.2 ${⊢}{R}=\left({u}\in \mathrm{ran}{I},{v}\in \mathrm{ran}{I}⟼{u}×{v}\right)$
Assertion dya2iocucvr ${⊢}\bigcup \mathrm{ran}{R}={ℝ}^{2}$

### Proof

Step Hyp Ref Expression
1 sxbrsiga.0 ${⊢}{J}=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
2 dya2ioc.1 ${⊢}{I}=\left({x}\in ℤ,{n}\in ℤ⟼\left[\frac{{x}}{{2}^{{n}}},\frac{{x}+1}{{2}^{{n}}}\right)\right)$
3 dya2ioc.2 ${⊢}{R}=\left({u}\in \mathrm{ran}{I},{v}\in \mathrm{ran}{I}⟼{u}×{v}\right)$
4 unissb ${⊢}\bigcup \mathrm{ran}{R}\subseteq {ℝ}^{2}↔\forall {d}\in \mathrm{ran}{R}\phantom{\rule{.4em}{0ex}}{d}\subseteq {ℝ}^{2}$
5 vex ${⊢}{u}\in \mathrm{V}$
6 vex ${⊢}{v}\in \mathrm{V}$
7 5 6 xpex ${⊢}{u}×{v}\in \mathrm{V}$
8 3 7 elrnmpo ${⊢}{d}\in \mathrm{ran}{R}↔\exists {u}\in \mathrm{ran}{I}\phantom{\rule{.4em}{0ex}}\exists {v}\in \mathrm{ran}{I}\phantom{\rule{.4em}{0ex}}{d}={u}×{v}$
9 simpr ${⊢}\left(\left({u}\in \mathrm{ran}{I}\wedge {v}\in \mathrm{ran}{I}\right)\wedge {d}={u}×{v}\right)\to {d}={u}×{v}$
10 pwssb ${⊢}\mathrm{ran}{I}\subseteq 𝒫ℝ↔\forall {d}\in \mathrm{ran}{I}\phantom{\rule{.4em}{0ex}}{d}\subseteq ℝ$
11 ovex ${⊢}\left[\frac{{x}}{{2}^{{n}}},\frac{{x}+1}{{2}^{{n}}}\right)\in \mathrm{V}$
12 2 11 elrnmpo ${⊢}{d}\in \mathrm{ran}{I}↔\exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {n}\in ℤ\phantom{\rule{.4em}{0ex}}{d}=\left[\frac{{x}}{{2}^{{n}}},\frac{{x}+1}{{2}^{{n}}}\right)$
13 simpr ${⊢}\left(\left({x}\in ℤ\wedge {n}\in ℤ\right)\wedge {d}=\left[\frac{{x}}{{2}^{{n}}},\frac{{x}+1}{{2}^{{n}}}\right)\right)\to {d}=\left[\frac{{x}}{{2}^{{n}}},\frac{{x}+1}{{2}^{{n}}}\right)$
14 simpll ${⊢}\left(\left({x}\in ℤ\wedge {n}\in ℤ\right)\wedge {d}=\left[\frac{{x}}{{2}^{{n}}},\frac{{x}+1}{{2}^{{n}}}\right)\right)\to {x}\in ℤ$
15 14 zred ${⊢}\left(\left({x}\in ℤ\wedge {n}\in ℤ\right)\wedge {d}=\left[\frac{{x}}{{2}^{{n}}},\frac{{x}+1}{{2}^{{n}}}\right)\right)\to {x}\in ℝ$
16 2re ${⊢}2\in ℝ$
17 16 a1i ${⊢}\left(\left({x}\in ℤ\wedge {n}\in ℤ\right)\wedge {d}=\left[\frac{{x}}{{2}^{{n}}},\frac{{x}+1}{{2}^{{n}}}\right)\right)\to 2\in ℝ$
18 2ne0 ${⊢}2\ne 0$
19 18 a1i ${⊢}\left(\left({x}\in ℤ\wedge {n}\in ℤ\right)\wedge {d}=\left[\frac{{x}}{{2}^{{n}}},\frac{{x}+1}{{2}^{{n}}}\right)\right)\to 2\ne 0$
20 simplr ${⊢}\left(\left({x}\in ℤ\wedge {n}\in ℤ\right)\wedge {d}=\left[\frac{{x}}{{2}^{{n}}},\frac{{x}+1}{{2}^{{n}}}\right)\right)\to {n}\in ℤ$
21 17 19 20 reexpclzd ${⊢}\left(\left({x}\in ℤ\wedge {n}\in ℤ\right)\wedge {d}=\left[\frac{{x}}{{2}^{{n}}},\frac{{x}+1}{{2}^{{n}}}\right)\right)\to {2}^{{n}}\in ℝ$
22 2cnd ${⊢}\left(\left({x}\in ℤ\wedge {n}\in ℤ\right)\wedge {d}=\left[\frac{{x}}{{2}^{{n}}},\frac{{x}+1}{{2}^{{n}}}\right)\right)\to 2\in ℂ$
23 22 19 20 expne0d ${⊢}\left(\left({x}\in ℤ\wedge {n}\in ℤ\right)\wedge {d}=\left[\frac{{x}}{{2}^{{n}}},\frac{{x}+1}{{2}^{{n}}}\right)\right)\to {2}^{{n}}\ne 0$
24 15 21 23 redivcld ${⊢}\left(\left({x}\in ℤ\wedge {n}\in ℤ\right)\wedge {d}=\left[\frac{{x}}{{2}^{{n}}},\frac{{x}+1}{{2}^{{n}}}\right)\right)\to \frac{{x}}{{2}^{{n}}}\in ℝ$
25 1red ${⊢}\left(\left({x}\in ℤ\wedge {n}\in ℤ\right)\wedge {d}=\left[\frac{{x}}{{2}^{{n}}},\frac{{x}+1}{{2}^{{n}}}\right)\right)\to 1\in ℝ$
26 15 25 readdcld ${⊢}\left(\left({x}\in ℤ\wedge {n}\in ℤ\right)\wedge {d}=\left[\frac{{x}}{{2}^{{n}}},\frac{{x}+1}{{2}^{{n}}}\right)\right)\to {x}+1\in ℝ$
27 26 21 23 redivcld ${⊢}\left(\left({x}\in ℤ\wedge {n}\in ℤ\right)\wedge {d}=\left[\frac{{x}}{{2}^{{n}}},\frac{{x}+1}{{2}^{{n}}}\right)\right)\to \frac{{x}+1}{{2}^{{n}}}\in ℝ$
28 27 rexrd ${⊢}\left(\left({x}\in ℤ\wedge {n}\in ℤ\right)\wedge {d}=\left[\frac{{x}}{{2}^{{n}}},\frac{{x}+1}{{2}^{{n}}}\right)\right)\to \frac{{x}+1}{{2}^{{n}}}\in {ℝ}^{*}$
29 icossre ${⊢}\left(\frac{{x}}{{2}^{{n}}}\in ℝ\wedge \frac{{x}+1}{{2}^{{n}}}\in {ℝ}^{*}\right)\to \left[\frac{{x}}{{2}^{{n}}},\frac{{x}+1}{{2}^{{n}}}\right)\subseteq ℝ$
30 24 28 29 syl2anc ${⊢}\left(\left({x}\in ℤ\wedge {n}\in ℤ\right)\wedge {d}=\left[\frac{{x}}{{2}^{{n}}},\frac{{x}+1}{{2}^{{n}}}\right)\right)\to \left[\frac{{x}}{{2}^{{n}}},\frac{{x}+1}{{2}^{{n}}}\right)\subseteq ℝ$
31 13 30 eqsstrd ${⊢}\left(\left({x}\in ℤ\wedge {n}\in ℤ\right)\wedge {d}=\left[\frac{{x}}{{2}^{{n}}},\frac{{x}+1}{{2}^{{n}}}\right)\right)\to {d}\subseteq ℝ$
32 31 ex ${⊢}\left({x}\in ℤ\wedge {n}\in ℤ\right)\to \left({d}=\left[\frac{{x}}{{2}^{{n}}},\frac{{x}+1}{{2}^{{n}}}\right)\to {d}\subseteq ℝ\right)$
33 32 rexlimivv ${⊢}\exists {x}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {n}\in ℤ\phantom{\rule{.4em}{0ex}}{d}=\left[\frac{{x}}{{2}^{{n}}},\frac{{x}+1}{{2}^{{n}}}\right)\to {d}\subseteq ℝ$
34 12 33 sylbi ${⊢}{d}\in \mathrm{ran}{I}\to {d}\subseteq ℝ$
35 10 34 mprgbir ${⊢}\mathrm{ran}{I}\subseteq 𝒫ℝ$
36 35 sseli ${⊢}{u}\in \mathrm{ran}{I}\to {u}\in 𝒫ℝ$
37 36 elpwid ${⊢}{u}\in \mathrm{ran}{I}\to {u}\subseteq ℝ$
38 35 sseli ${⊢}{v}\in \mathrm{ran}{I}\to {v}\in 𝒫ℝ$
39 38 elpwid ${⊢}{v}\in \mathrm{ran}{I}\to {v}\subseteq ℝ$
40 xpss12 ${⊢}\left({u}\subseteq ℝ\wedge {v}\subseteq ℝ\right)\to {u}×{v}\subseteq {ℝ}^{2}$
41 37 39 40 syl2an ${⊢}\left({u}\in \mathrm{ran}{I}\wedge {v}\in \mathrm{ran}{I}\right)\to {u}×{v}\subseteq {ℝ}^{2}$
42 41 adantr ${⊢}\left(\left({u}\in \mathrm{ran}{I}\wedge {v}\in \mathrm{ran}{I}\right)\wedge {d}={u}×{v}\right)\to {u}×{v}\subseteq {ℝ}^{2}$
43 9 42 eqsstrd ${⊢}\left(\left({u}\in \mathrm{ran}{I}\wedge {v}\in \mathrm{ran}{I}\right)\wedge {d}={u}×{v}\right)\to {d}\subseteq {ℝ}^{2}$
44 43 ex ${⊢}\left({u}\in \mathrm{ran}{I}\wedge {v}\in \mathrm{ran}{I}\right)\to \left({d}={u}×{v}\to {d}\subseteq {ℝ}^{2}\right)$
45 44 rexlimivv ${⊢}\exists {u}\in \mathrm{ran}{I}\phantom{\rule{.4em}{0ex}}\exists {v}\in \mathrm{ran}{I}\phantom{\rule{.4em}{0ex}}{d}={u}×{v}\to {d}\subseteq {ℝ}^{2}$
46 8 45 sylbi ${⊢}{d}\in \mathrm{ran}{R}\to {d}\subseteq {ℝ}^{2}$
47 4 46 mprgbir ${⊢}\bigcup \mathrm{ran}{R}\subseteq {ℝ}^{2}$
48 retop ${⊢}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Top}$
49 1 48 eqeltri ${⊢}{J}\in \mathrm{Top}$
50 49 49 txtopi ${⊢}{J}{×}_{t}{J}\in \mathrm{Top}$
51 uniretop ${⊢}ℝ=\bigcup \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
52 1 unieqi ${⊢}\bigcup {J}=\bigcup \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
53 51 52 eqtr4i ${⊢}ℝ=\bigcup {J}$
54 49 49 53 53 txunii ${⊢}{ℝ}^{2}=\bigcup \left({J}{×}_{t}{J}\right)$
55 54 topopn ${⊢}{J}{×}_{t}{J}\in \mathrm{Top}\to {ℝ}^{2}\in \left({J}{×}_{t}{J}\right)$
56 1 2 3 dya2iocuni ${⊢}{ℝ}^{2}\in \left({J}{×}_{t}{J}\right)\to \exists {c}\in 𝒫\mathrm{ran}{R}\phantom{\rule{.4em}{0ex}}\bigcup {c}={ℝ}^{2}$
57 50 55 56 mp2b ${⊢}\exists {c}\in 𝒫\mathrm{ran}{R}\phantom{\rule{.4em}{0ex}}\bigcup {c}={ℝ}^{2}$
58 simpr ${⊢}\left({c}\in 𝒫\mathrm{ran}{R}\wedge \bigcup {c}={ℝ}^{2}\right)\to \bigcup {c}={ℝ}^{2}$
59 elpwi ${⊢}{c}\in 𝒫\mathrm{ran}{R}\to {c}\subseteq \mathrm{ran}{R}$
60 59 adantr ${⊢}\left({c}\in 𝒫\mathrm{ran}{R}\wedge \bigcup {c}={ℝ}^{2}\right)\to {c}\subseteq \mathrm{ran}{R}$
61 60 unissd ${⊢}\left({c}\in 𝒫\mathrm{ran}{R}\wedge \bigcup {c}={ℝ}^{2}\right)\to \bigcup {c}\subseteq \bigcup \mathrm{ran}{R}$
62 58 61 eqsstrrd ${⊢}\left({c}\in 𝒫\mathrm{ran}{R}\wedge \bigcup {c}={ℝ}^{2}\right)\to {ℝ}^{2}\subseteq \bigcup \mathrm{ran}{R}$
63 62 rexlimiva ${⊢}\exists {c}\in 𝒫\mathrm{ran}{R}\phantom{\rule{.4em}{0ex}}\bigcup {c}={ℝ}^{2}\to {ℝ}^{2}\subseteq \bigcup \mathrm{ran}{R}$
64 57 63 ax-mp ${⊢}{ℝ}^{2}\subseteq \bigcup \mathrm{ran}{R}$
65 47 64 eqssi ${⊢}\bigcup \mathrm{ran}{R}={ℝ}^{2}$